程序性质的描述及证明

来源 :计算机科学 | 被引量 : 0次 | 上传用户：huangcheng118

【摘要】

：

<正> XYZ/E是一种基于Manna-Pnueli线性时序逻辑的线性时序逻辑语青(LTLL),其主要特征为它在统一的时序逻辑框架下既能表示程序的静态规范(XYZ/AE)也能表示可执行代码(XYZ/EE

【作者】

：

官荷卿郭亮

【机构】

：

中国科学院软件研究所计算机科学开放研究室

【出处】

：

计算机科学

【发表日期】

：

2003年3期

【关键词】

：

程序性质程序设计 XYZ语言 AE语言时序逻辑语言 Temporal logic language XYZ/E.Dekker algorithm Speci

【基金项目】

：

国家自然科学基金YCK15028

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

<正> XYZ/E是一种基于Manna-Pnueli线性时序逻辑的线性时序逻辑语青(LTLL),其主要特征为它在统一的时序逻辑框架下既能表示程序的静态规范(XYZ/AE)也能表示可执行代码(XYZ/EE),因此程序规范和程序可执行代码的语义一致性也就得以在时序逻辑框架下验证。对于顺序程序,XYZ系统提供了一套基于Hoare逻辑规则的验证工具XYZ/VERI。此工具通过读取程序及其前后断

其他文献

我国道路石油沥青标准的发展历程

通过查阅调研建国以来我国道路石油沥青标准制定与修订情况,对其发展历程进行梳理,为不同行业、不同使用部门合理选择实施道路石油沥青标准提供参考。

期刊

道路石油沥青国家标准行业标准发展历程Petroleum asphalt for road National standard Industrial

水泥、二灰固化剂在黄土改良中的对比研究

对比水泥固化剂与二灰固化剂对黄土不良工程性能的处置效果,通过测量CBR值得出：随着二灰与水泥掺量的增加,土体承载能力上升,膨胀率下降,其中5%掺量水泥膨胀率最低为0.08%,回

期刊

黄土水泥二灰CBR值回弹模量水稳定性无侧限抗压强度Loess Cement Lime fly-ash CBR value Modulus

基于遗传算法的FCM算法在边坡监测中的应用研究

利用模糊聚类分析方法将边坡进行安全等级分类,对于边坡的治理是一种有效的方法。传统的聚类是一种局部搜索方法,易陷入极小值。遗传算法（GA）是一种应用广泛的全局寻优算法,将

期刊

FCM聚类算法遗传算法边坡监测FCM clustering algorithm Genetic algorithm Slope monitoring

预应力损失对连续刚构桥施工中腹板开裂的影响分析

随着近几十年交通运输事业的飞速发展,连续刚构桥凭借其经济实用、行车平顺舒适及不需要转换体系等一系列优点,成为大跨径桥梁选型里极具竞争力的桥型之一。但随着大跨径连续

期刊

连续刚构桥施工中腹板开裂敏感性因素预应力损失Continuous rigid frame bridge Cracking in webs during

基于Agent的自适应性工作流模型的研究与设计

该文在对代理技术和当前工作流技术所面临的问题进行研究的基础上，提出了基于Agent的自适应性工作流模型，研究了其中的一些相关算法和关键技术的实现机制。最后讨论了下一步要

期刊

工作流模型自适应性代理技术工作流技术算法设计实现机制若干问题基础关键技术

基于MPEG－4的视频检索技术研究

There are so many multimedia resources now. But it is difficult to look for any video thing amongthem. MPEG-4 is a major technique used for video coding. In the

期刊

视频检索多媒体文件格式MPEG-4视频压缩图像编码MPEG-4 XML DIVX A/VO OCI XMT

程序性质的描述及证明

其他学术论文