论文部分内容阅读
把赋值语句看作物理对象上的操作时，程序就呈现为物理对象上的操作构成的表达式（简称O表达式）。给出了定义O表达式语法的BNF公式，并用公理规定O表达式的语义。主动式的O表达式以计算最终结果为目的，因而相关公理给出的是施行表达式中操作以后的变量与施行之前变量之间的准确依赖关系。反应式O表达式要对外来需求作反应。描述反应的公理规定如何反应。有关通讯的公理要求正确的信息被正确的接受者收到。共享变量公理则给出有关共享变量的性质判断。例子用于说明异步顺序O表达式的性质是如何分析的。