程序:物理对象上的操作表达式(英文)  

Program:Expressions of Operations on Physical Objects

作　　者：袁崇义[1,2] 黄雨[1,2,3] 赵文[1,2,3] 

机构地区：[1]教育部高可信软件技术重点实验室,北京100871 [2]北京大学信息科学技术学院,北京100871 [3]北京大学软件工程国家工程研究中心,北京100871

出　　处：《计算机科学与探索》2009年第2期144-153,共10页Journal of Frontiers of Computer Science and Technology

基　　金：The National Natural Science Foundation of China under Grant No.60803014,60873061;the National High-TechResearch and Development Plan of China under Grant No.2006AA01Z160;the National ResearchFoundation for Doctoral Program of Higher Education of China under Grant No.200800011017.~~

摘　　要：把赋值语句看作物理对象上的操作时,程序就呈现为物理对象上的操作构成的表达式(简称O表达式)。给出了定义O表达式语法的BNF公式,并用公理规定O表达式的语义。主动式的O表达式以计算最终结果为目的,因而相关公理给出的是施行表达式中操作以后的变量与施行之前变量之间的准确依赖关系。反应式O表达式要对外来需求作反应。描述反应的公理规定如何反应。有关通讯的公理要求正确的信息被正确的接受者收到。共享变量公理则给出有关共享变量的性质判断。例子用于说明异步顺序O表达式的性质是如何分析的。A program turns out to be an expression of operations on physical objects （operation expression or O_expression for short） when assignments are treated as operations on physical objects. BNF formulas are given to define O_expression syntax while axioms are proposed as semantics of O_expressions. An active O_expression computes some ultimate results. As such, an axiom for active O_expressions defines how a variable after the application of operations in an O_expression is precisely related to variables before the application. A reactive O_expression responses to requests from outside. An axiom, describing responses to requests, tells how a response should be made. Axioms on communications make sure that the right messages to be received by the right receivers while axioms about shared variables depict properties concerning shared variables. Examples are given to show how to analyze properties of asynchronous sequential O_expressions .

关 键 词：程序 物理对象 物理对象上的操作 物理对象上的操作表达式 语义公理 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]