从规范到机器代码:通过形式分析构造程序

现代技术将使软件越来越多地固化在硬件之中。有些情况绝对不允许软件中有任何错误,这只是其中一例。因此程序设计必须很快成为一个安全的程序构造过程;也就是说,应把程序设计组织成为进行推理分析的一系列步骤。先用基本谓词逻辑、集合论和代数做工具对问题做细致的形式规范;再以此规范为出发点,应用形式规则导出它的若干算法版本;最后得到面向若干特定具体机器指令系统的程序。真正的程序构造过程自始至终需要严格形式化。包括规范在内的一切版本都可以很方便地用一个程序设计语言表示,该语言包括描述性的以及应用式(applicative)和过程式的各种风格的功能。这样一个语言还要包括非确定性的概念。非确定性使程序开发过程简单明了而且分外灵活,非确定性是由某个做为其基础的抽象数据类型模型解释的。由于使用的是经过形式证明的变换规则,正确性是得到保证的。此外,尽管程序变换方法最初针对的是经典的程序存储式计算机的软件构造,而且现在主要仍用于这类计算机的软件构造,但它可以扩充到其它计算模型,以适应经常提到的硬件体系结构的革新。这些变换规则可以用于任何问题,在这个意义上可以说程序变换是个通用办法。     

C.A.Petri与计算机科学

这篇文章是作者在西德GMD(数学和数据处理协会)为庆祝Carl Adam Petri博士六十岁生日召开的会上所作的报告。对Petri的成就和远见卓识作了高度评价。报告观点较高,内容深刻,富有哲理,值得参考。原文系德文,译文系根据Springer-Verlag 1987年出版的书《Cencurrency and Nets》中的英译文译出的。     

新程序设计

在计算机问世以来的几十年中,程序设计经历了从技巧到科学的曲折历程。虽然作为一门科学它的全貌还不全清楚,但人们毕竟已认识到,程序设计应该有它自己的原理和原则的一门科学。在这个方向上迄今取得的成就中,Dijkstra 的贡献是最基本最重要的。     

Solving Inheritance Anomaly with OMNets

This paper presents a concurrent object-oriented modeling language based on Petri nets:OMNets,which hepls greatly to avoid the inheritance anomaly problem appeared in concurrent OO languages.OMNets separates th functional part and the synchroniztion part of objects and uses Petri nets to describe the synchronization part.Both parts are reusable through inheritance.     

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

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

一种基于Petri网的RFID事件检测的形式化方法

无线射频识别(RFID)采用唯一的电子标签识别物理对象,可高速收集大量目标数据.为向各类应用提供语义信息,RFID系统需从收集的数据中检测用户自定义的复合事件.通过提出一种基于Petri网的RFID事件检测方法,引入形式化的ED-net模型描述复合事件语义,并以此为基础实现一种事件检测方法.ED-net模型是对传统Petri网的一种扩展,提供了描述用户自定义类型、函数及表达式的能力,可精确描述RFID复合事件的属性及时域、非时域、参数化等约束条件.通过对RFID事件形式化描述,各种RFID事件可以统一在ED-net模型,并可自动化进行检测处理,避免了不同复合事件间公共子事件重复检测的问题.最后,经过实验测试和分析,验证了该形式化方法的有效性及其优势.     

基于规则推理的语义检索若干关键技术研究

 针对专业领域复杂的检索需求,目前相关研究采用基于语义的方法来扩展检索范围并提高准确度.在语义推理方面,目前搜索引擎通常直接采用语义网中的推理算法,推理效率不高.在排序方面,基于关键字的搜索引擎的排序算法也不适合对语义检索结果进行排序.针对上述问题,本文给出了基于语义网的语义规则建立方法,并提出了一种基于闭合世界假设的反向链接推理算法,提高推理效率,同时给出了一种基于特征相似性排序算法,使检索结果排序方式更加符合语义检索的特点.基于本文提出的方法,构造了语义搜索引擎MaterialHub,实验表明该搜索引擎提高了检索的准确率和查全率,有较好的查询响应时间,并已经得到实际应用.     

死锁的PETRI NETS模型

本文给出了操作系统(OS)的一种基于Petri网的形式化模型,由此把死锁问题转化为线性代数问题。我们得到了OS中死锁存在的充要条件,以及一种消除系统中所有的死锁、保证系统正常工作的最优化方法。特别是对于分布式OS,我们大大改进了以往的一些处理死锁的方法,最后还通过举例进行了说明。     

关于程序调试的理论和方法

本文以正确性调试为例,介绍了两种主要调试手段:数据调试法和符号运行法。还指出了各自的局限性。     

基于UniNet的对象概念研究

This paper discusses concepts on object from UniNet view and shows that there exists the flow of controlin object system except for exchanging of messages between objects. Meanwhile, the paper presents an independent mechanism of object communication separated from object that will result in a more general reuse of object. With helpof the control flow and the data flow, UniNet can describe not only the static features, but also the dynamic featuresof object system, which naturally solve the inheritance anomaly and the flow of data and control. In addition, based on UniNet specification, the object system can be verified easily and create the program code automatically.