Repeat-until语句的操作语义与指称语义的等价性证明

Equivalence proving of operational and denotational semantics about Repeat-until statement

在计算机科学中,形式语义学以数学为工具,精确地定义和解释计算机程序设计语言的含义或语义.其中操作语义学和指称语义学是形式语义学的两大类别.本文使用简单的命令式语言IMP的语法,首先给出了repeat-until循环语句的操作语义,然后详细推导出了其指称语义,并在此基础上详细证明了它们二者之间的语义等价性.

In computer science field, formal semantics accurately definesand explains the meaning or semantics of computer programming langurage by means of mathematics tool. Operational semantics and denotational semantics are two type of formal semantics. Using syntax of IMP, the operational semantics of repeat-until loop statement is given first, then the denotational semantics of repeat-until loop statement is deduced, and finally the equivalence of them is proved in detail.