The semantics of a simple parallel programming language is presented in two ways: deductively, by a set of Hoare-like axioms and inference rules, and operationally, by means of an interpreter. It is shown that the deductive system is consistent with the interpreter. It would be desirable to show that the deductive system is also complete with respect to the interpreter, but this is impossible since the programming language contains the natural numbers. Instead it is proved that the deductive system is complete relative to a complete proof system for the natural numbers; this result is similar to Cook's relative completeness for sequential programs.
The deductive semantics given here is an extension of an incomplete deductive system proposed by Hoare. The key difference is an additional inference rule which provides for the introduction of auxiliary variables in a program to be verified.
简单并行编程语言的语义以两种方式表示:通过一组类似Hoare的公理和推理规则进行演绎,以及在操作上通过解释器进行演绎。结果表明,演绎系统与口译员是一致的。希望证明演绎系统在解释器方面也是完整的,但这是不可能的,因为编程语言包含自然数。相反,证明了相对于自然数的完整证明系统而言,演绎系统是完整的。这个结果类似于库克对顺序程序的相对完整性。 P>
此处给出的演绎语义是Hoare提出的不完整演绎系统的扩展。关键的区别是附加的推理规则,该规则可在要验证的程序中引入辅助变量。 P>
机译:完善而完整的演绎系统,用于ctl *验证*
机译:用于多DSP系统的C程序自动并行化的完整编译器方法
机译:自动化弱存储程序的演绎验证(扩展版)
机译:旨在演绎验证消息传递并行程序
机译:完整的概率逻辑演绎系统,应用于Harsanyi型空间。
机译:基于等式的异构计算系统仿真程序的平行化
机译:一致而完整的演绎程序验证系统
机译:演绎数据库和逻辑编程:演绎数据库和基于知识的系统中的绑定。 ICLp'95联合研讨会的会议记录。 1995年6月17日在日本湘南村中心举行