程序：物理对象上的操作表达式

doi:10.3778/j.issn.1673-9418.2009.02.003

计算机科学与探索 ›› 2009, Vol. 3 ›› Issue (2): 144-153.DOI: 10.3778/j.issn.1673-9418.2009.02.003

程序：物理对象上的操作表达式

袁崇义^1,2,黄雨^1,2,3+,赵文^1,2,3

1. 教育部高可信软件技术重点实验室，北京 100871
2. 北京大学信息科学技术学院，北京 100871
3. 北京大学软件工程国家工程研究中心，北京 100871

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2009-03-15 发布日期:2009-03-15
通讯作者: 袁崇义

Program： Expressions of Operations on Physical Objects

YUAN Chongyi^1,2, HUANG Yu^1,2,3+, ZHAO Wen^1,2,3

1. Key Laboratory of High Confidence Software Technologies of Ministry of Education， Peking University， Beijing 100871， China
2. School of Electronics Engineering and Computer Science， Peking University， Beijing 100871， China
3. National Engineering Research Center for Software Engineering， Peking University， Beijing 100871， China

Received:1900-01-01 Revised:1900-01-01 Online:2009-03-15 Published:2009-03-15
Contact: YUAN Chongyi

摘要/Abstract

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

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

Abstract: 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.

Key words: program, physical object, operation on physical object, expression of operations on physical object, semantic axiom

袁崇义1,2 ,黄雨1,2,3+, 赵文1,2,3 . 程序：物理对象上的操作表达式[J]. 计算机科学与探索, 2009, 3(2): 144-153.

YUAN Chongyi^1,2, HUANG Yu^1,2,3+, ZHAO Wen^1,2,3. Program： Expressions of Operations on Physical Objects[J]. Journal of Frontiers of Computer Science and Technology, 2009, 3(2): 144-153.

[1]	史志成, 周宇. 代码特征自动提取方法[J]. 计算机科学与探索, 2021, 15(3): 456-467.
[2]	闫鑫，周宇，黄志球. 基于序列到序列模型的代码片段推荐[J]. 计算机科学与探索, 2020, 14(5): 731-739.
[3]	曾杰，贲可荣，张献，李晓伟，周全. 基于程序向量树的代码克隆检测[J]. 计算机科学与探索, 2020, 14(10): 1656-1669.
[4]	王素琴，吴子锐. 利用LSTM网络和课程关联分类的推荐模型[J]. 计算机科学与探索, 2019, 13(8): 1380-1389.
[5]	任武. 结合动静态分析实现架构恢复的方法[J]. 计算机科学与探索, 2019, 13(4): 563-573.
[6]	杨嘉成，彭鑫，赵文耘. 安卓应用HTTP缓存缺陷的动态检测[J]. 计算机科学与探索, 2018, 12(9): 1397-1406.
[7]	马巧梅. 基于程序特征的线程划分方法的研究[J]. 计算机科学与探索, 2018, 12(6): 872-885.
[8]	陆凯，姜淑娟，王兴亚. 结合图挖掘和支持向量机的错误定位[J]. 计算机科学与探索, 2018, 12(10): 1614-1621.
[9]	吉华斌，尚颖，李征. Web应用程序异步请求时序问题检测[J]. 计算机科学与探索, 2018, 12(1): 101-111.
[10]	柳郁，孙小兵，李斌. 面向Java程序包的代码概要自动生成技术研究[J]. 计算机科学与探索, 2017, 11(2): 212-220.
[11]	梅俊杰，刘蕻，原国伟，王以松. 带函数析取逻辑程序的无基集及其应用[J]. 计算机科学与探索, 2015, 9(6): 747-755.
[12]	车永刚，张理论，王勇献，徐传福，程兴华. Intel 多核与集成众核上CFD程序的OpenMP 性能分析[J]. 计算机科学与探索, 2015, 9(10): 1153-1162.
[13]	江联，黄海亮，周晓聪，王欣明，李文军. 基于变量感染分析的软件错误定位技术[J]. 计算机科学与探索, 2014, 8(8): 966-977.
[14]	王海，林云，彭鑫，赵文耘. 基于分组的代码克隆增量检测方法[J]. 计算机科学与探索, 2014, 8(4): 446-455.
[15]	杨卓群，王以松. 描述逻辑程序系统的设计与实现[J]. 计算机科学与探索, 2014, 8(3): 338-344.

程序：物理对象上的操作表达式

Program： Expressions of Operations on Physical Objects

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics