基于归约方法的操作语义的定义过程 ●格局的形式:<comp1,…,comp>,通过模式给出 ●初始格局和终止格局 组归约公理 configure -> configur e2 一组归约规则形: ······n 条件公理 configure1→ confi gure2推导出的公理 其中A1,…,An是关于 configure1中成分的公理,而 configure2中的成分只能从 onfigure1和A1,,An 中的结果格局中得到; 2021/2/52021/2/5 26 基于归约方法的操作语义的定义过程 ⚫ 格局的形式：<comp1,…, compn>，通过模式给出 ⚫ 初始格局和终止格局 ⚫ 一组归约公理： configure1 → configure2 ⚫ 一组归约规则形： A1,……,An 条件公理 configure1 → configure2 推导出的公理 其中A1,……,An是关于configure1中成分的公理，而 configure2中的成分只能从configure1和A1,……,An 中的结果格局中得到；