基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.     

应用ANTLR实现过程式语言操作语义的动态演示

介绍了一个面向过程语言的文法特点,应用ANTLR实现了该语言操作语义的动态演示,系统可辅助教师进行课堂教学,为学生自主学习提供良好的支撑环境,从而用形象的图形界面为学生搭起通向掌握抽象思维方法的桥梁。     

并发约束程序设计语言COPS及其执行模型

约束程序设计尤其是约束逻辑程序设计与并发约束程序设计在AI程序设计领域占据着越来越重要的位置。传统逻辑程序设计的基“计算即为定理证明”的计算风格虽获得了简洁优美的操作语义特性,但也付出了执行效率低的代价,当应用系统规模增大时,其性能严重下降以致崩溃。针对传统逻辑程序设计的这种可伸缩性问题,设计了一个基于并发约束程序设计概念的说明性语言COPS,旨在从语言设计与执行模型两方面降低说明性程序的不确定性,提高搜索与运行效率。在语言设计方面,通过引入确定性语言成分,避免不确定计算用于确定性目标所浪费的系统开销;在执行模型方面,在目标的并发穿叉执行与数据驱动的并发同步机制的基础上,实现“优先执行确定目标”策略与“最少假定”策略,作为约束传播的延伸,最大幅度地剪枝搜索空间,降低搜索复杂性。COPS提供的知识表示、推理与并发机制使其成为构造agent程序的理想语言。论文给出COPS语言的语法规范与执行模型的操作语义描述。     

AgentSpeak中意图生成过程的可靠性与完整性研究

意图生成是BDI型Agent为实现目标而产生动作序列的过程。验证软件Agent中意图生成的正确性是Agent编程语言中一个重要的研究问题。针对软件Agent中意图执行的正确性,以当前最流行的BDI型Agent编程语言AgentSpeak为例,证明了软件Agent意图执行的有效性。首先根据AgentSpeak的语法构造了一个解释系统,并给出了该解释系统的满足关系,从而得出了AgentSpcak的模型论语义。在该模型论语义的基础上,结合由Moreira和Bordini所给出的操作语义,证明了AgentSpeak的意图生成等价定理:AgentSpeak语言中模型论语义的意图等价于AgentSpeak程序操作语义的意图。由此可得出结论—AgentSpcak中的意图执行是可靠而完整的,从而验证了AgcntSpcak中软件Agent意图完成目标的正确性。     

DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述

Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描述操作的时态驱动、事件驱动、操作补偿等因素,分析和说明了该语言的语法和语义,最后通过对责任授权模型的形式化描述说明了该语言的表达能力和应用。     

基于过程模型的工作流执行语义研究

针对现有工作流建模语言难以兼顾语言的可理解性、执行语义的形式化和描述维度的单一性等问题,提出利用可视化的过程模型作为工作流建模语言。过程模型能从过程、数据、资源、组织等多个角度描述企事业的业务工作流程。根据过程模型的语法和工作流系统的特点,定义形式化执行语义,为过程模型的分析、验证和执行提供理论依据。     

PROMELA语义引擎执行研究

模型检查工具SPIN的核心是PROMELA语言,对PROMELA语言执行方式的理解决定所描述系统模型的行为方式。该文从语义角度研究了PROMELA语义引擎问题。首先给出PROMELA语法的抽象对象模型形式化定义,然后给出一个算法来实现PROMELA语法到抽象对象模型的映射,描述了PROMELA指称语义。     

一种基于组合Monad的纯函数式通道系统操作

Monad作为构造纯函数式语言的工具,能构造出诸如错误处理、状态、IO等非纯函数式语言的特征。该文通过组合状态转换Monad和异常处理Monad来定义纯函数式语言通道系统操作,给出了通道系统操作的操作语义。     

TempDB:时态数据管理系统

为了适应时态数据库发展需求,针对目前时态数据库技术实现则相对滞后现状,设计和实现了时态数据处理原型系统TempDB. TempDB采用中间件的架构实现,使用具有代表性的时态查询语言--ATSQL2,将时态操作语言转换成与之语义等价的、标准的SQL语言,然后在后台DBMS上执行,实现了基本的时态数据管理功能. TempDB总结应用了相关理论知识,同时也为时态数据库系统的产品化积累了经验.     

一种机器人程序设计语言

本文论述我们自己设计和实现的机器人语言 ZDRL。这是一种面向运动的语言,用户程序采用解释执行的方式。语言系统提供了一个良好的程序开发环境,用户可进行对程序的编辑、调试、执行和存取操作。该系统已在 IBMPC 微机上实现。并已应用到 Rhino 机器人的控制上。     

仿生机器鱼的动力学仿真

仿生机器鱼的研究受到各国越来越多的研究工作者的重视,并取得了一定的成果.本文着重研究了仿生机器鱼的尾鳍的动力学并建立了仿生机器鱼的运动模型,并对该模型进行了计算机仿真,研究探索了仿生机器鱼的前进速度与尾鳍摆角、摆动频率、摆动幅度之间的关系.     

多种燃料锅炉效率曲线的辨识方法

多种燃料锅炉的运行优化是钢铁联合企业节约能源的一个主要方法,但是这种锅炉的效率曲线的辨识却是一个复杂而困难的非线性最小二乘问题。借鉴大系统递阶算法的思想,本文提出了一种新的两级递阶辨识的算法。这种算法通过预估关联量,将非线性最小二乘问题转化为两级线性最小二乘问题。实验的结果证明:这种算法是一种有效的算法。     

多台电轴系统稳定性区域之扩大

刘永清在[1]、[2]中研究了疏松桂提出的多台电轴系统的稳定性,本文应用标量函数分解法,从如何寻求尽可能大的稳定域的观点出发,研究了电力拖动自动控制系统中带平衡机的n台电轴系统的稳定性,扩大了参数稳定性区域,并给出渐近稳定性区域估计式。     

PERCEPTION OF AREA OF INTERPOLATED FIGURES

The area perception of incomplete (interpolated) geometric figures is studied. The obtained data are discussed in order to compare them with the results of our previous experiments where complete figures were studied. The results of the present experiment support the validity of the model of area perception that is based on the concept of image function. The different contributions of the perceptual processes as well as of the cognitive processes to the area estimation are discussed.     

并发代码的继承问题

文献[1]提出了一种新的刻划并发行为的方法.本文继续讨论这种方法在面向对象的程序设计中是如何解决并发代码在继承过程中的冲突问题的.     

智能优化策略的比较

智能优化是从诸多新兴学科衍生出来的前沿科学，本文研究了智能优化的策略，对计算智能策略进行了分析比较，并举出了在工程实践中用这些策略进行智能优化的实例，从中得出有意义的结论。     

溴代胞嘧啶对三螺旋DNA稳定性的影响

研究了三螺旋ＤＮＡ中胞嘧啶被５－溴有包嘧啶取代后的稳定性问题。通过建立ＣＧＣ、ＣＧＢｒＣ,ＢｒＧＣ和ＢｒＣＧＢｒＣ４种模型。并２ＩｎｓｉｇｈｔⅡ软件包中的Ｄｉｓｃｏｖｅｒ程度进行计算模拟,骼５－溴胞嘧啶取代三螺肇ＤＮＡ分子中的胞嘧啶后,整个分子的稳定性与有所降低。同时,当用５－溴胞嘧啶取代三螺旋ＤＮＡ不同链上的胞嘧啶时,被取代链的碱基堆积能显著增高,导致分子人稳定性降低,但被取代链和相邻链同相互和     

人体三围特征计算的研究与实现

文中提出了一个基于多边形逼近和凸包球取的人体三围特征计算方法。首先给出了一个具有确定性的高效的多边形逼年算法，运用该算法对人体横截面边界进行特征化处理，再通过特征识别抽取人体三围的特征多边形，最后通过计算凸包的方法获取人体三围特征值。文中提出的方法已运用于一个综合化的服装ＣＡＤ系统中。     

计算机仿真系统的可信度评估

相似理论是计算机仿真的基础,它在建立仿真模型、仿真可信性评估等方面都有很好的指导作用,在文中分析相似理论中的序结构定律的基础上,将序结构定律运用于计算机仿真系统的相似评定中,并给出了具体的算法。对如何评估仿真系统的相似度问题,在理论上作了一定的研究和探讨。     

表的等价性的NP完全性的讨论

本文给出了表的等价性判定的一些结果：三元可满足性问题，表达式的ＮＰ完全性，表的ＮＰ完全性，还给出了函数依赖对表的影响，强等价性的复杂性的一些讨论。为对表的进一步研究屯指出了方向。