如何证明顺序命令C1；如果我们知道 C1 总是终止，那么 C2 总是可以执行到 C2？

Question

我正在使用定理证明器来演示程序的进度。

程序的语义是使用小步关系定义的，表示为 ctran，程序配置之间。程序配置被定义为(C,s)，其中C是命令并且是状态。因此，有效的执行在 ctran 中被定义为 (C1,s), (C1', s')。我们使用 ctran* 来表示 ctran 的传递自反闭包。然后将程序的终止定义为存在 t，使得 (C1, s), (term, t) \in ctran* 。现在我已经有了 (C1, s), (term, t) \in ctran*, 如何证明 (C1; C2, s), (C2, t) \in ctran*

Answer 1

在编程语言语义课程材料中，

sos_step

的定义表示

skip

（相当于您的

term

）在在序列的第一步执行时被忽略。 然后，您希望获得的语句是

sequence

与定理 sos_sequence_aux 所表达的执行的关联性的结果。