计算机科学与探索
計算機科學與探索
계산궤과학여탐색
JOURNAL OF FRONTIERS OF COMPUTER SCIENCE & TECHNOLOGY
2009年
2期
144-153
,共10页
程序%物理对象%物理对象上的操作%物理对象上的操作表达式%语义公理
程序%物理對象%物理對象上的操作%物理對象上的操作錶達式%語義公理
정서%물리대상%물리대상상적조작%물리대상상적조작표체식%어의공리
program%physical object%operation on physical object%expression of operations on physical object%semantic axiom
把赋值语句看作物理对象上的操作时,程序就呈现为物理对象上的操作构成的表达式(简称O表达式).给出了定义O表达式语法的BNF公式,并用公理规定O表达式的语义.主动式的O表达式以计算最终结果为目的,因而相关公理给出的是施行表达式中操作以后的变量与施行之前变量之间的准确依赖关系.反应式O表达式要对外来需求作反应.描述反应的公理规定如何反应.有关通讯的公理要求正确的信息被正确的接受者收到.共享变量公理则给出有关共享变量的性质判断.例子用于说明异步顺序O表达式的性质是如何分析的.
把賦值語句看作物理對象上的操作時,程序就呈現為物理對象上的操作構成的錶達式(簡稱O錶達式).給齣瞭定義O錶達式語法的BNF公式,併用公理規定O錶達式的語義.主動式的O錶達式以計算最終結果為目的,因而相關公理給齣的是施行錶達式中操作以後的變量與施行之前變量之間的準確依賴關繫.反應式O錶達式要對外來需求作反應.描述反應的公理規定如何反應.有關通訊的公理要求正確的信息被正確的接受者收到.共享變量公理則給齣有關共享變量的性質判斷.例子用于說明異步順序O錶達式的性質是如何分析的.
파부치어구간작물리대상상적조작시,정서취정현위물리대상상적조작구성적표체식(간칭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.