I present a new method for specifying and verifying the partial correctness of sequential programs. The key observation is that, in Hoare logic, assertions are used as selectors of states, that is, an assertion specifies the set of program states that satisfy the assertion. Hence, the usual meaning of the partial correctness Hoare triple $\{f\}\{P\}\{g\}$: if execution is started in any of the states that satisfy assertion $f$, then, upon termination, the resulting state will be some state that satisfies assertion $g$. There are of course other ways to specify a set of states. I propose to replace assertions by programs: a program $A$ specifies a set of states as follows: we start $A$ in any state whatsoever, and all the states that $A$ may terminate in constitute the specified set. I thus introduce the operational triple $[A]\, P\, [B]$ to mean: if execution of $P$ is started in any post-state of $A$, then upon termination, the resulting state will be some post-state of $B$. Here, $A$ is the pre-program, and plays the role of a pre-condition, and $B$ is the post-program, and plays the role of a post-condition. Finally, I indicate informally how operational annotations can be extended to the verification of concurrent programs.
翻译：关键的意见是,在Haare逻辑中,断言是作为国家选择者使用的,也就是说,断言具体指明了符合这一主张的一套方案。因此,部分正确性的通常含义是Hoare三倍的美元(ff ⁇ P ⁇ g ⁇ $$):如果在满足要求的任何一个州开始执行3倍的处决,那么,在终止时,所产生的状态将是满足1美元主张的某种状态。当然,还有其他方法可以指定一组国家。我提议用方案取代断言:一个方案($A$)具体列出一套国家如下:我们从任何州开始1美元,所有A$可能终止的州构成规定的一套。因此,我引入了3倍的[A]\,P\,[B]美元执行,意思是:如果在任何1美元后状态开始执行1美元,在终止时,那么,由此产生的状态将是一定的1美元后状态。这里,美元是方案前的1个州,在任何州中可以发挥固定的核查作用。
相关内容
微信扫码咨询专知VIP会员