精化演算支撑工具PRT的研究

1 引言精化演算是一种数学表示法和若干规则的集合,用于从程序规约推导出命令式程序。精化是从抽象程序向具体程序转换的过程,其中包含程序的正确性证明。精化的程序开发方法比对已有程序进行验证以保证程序正确性的方法更有效。通过精化演算中的转换规则可以演算出精化的程序。利用精化演算从规约导出程序的过程由大量步骤构成,非常适合利用机器工具进行辅助。本文对精化工具进行了需求分析和功能分析,研究了一个新的精化工具PRT(Program Refinement Tool)并与现有的一些工具进行了比较。     

基于程序窗口推理的精化演算

由于数据精化需要针对更大的程序块, 所以,它比一般的算法精化更加复杂.在精化演算中过程如何有效地进行数据精化是形式化 方法研究中的一个重要内容.该文介绍了相关的基本概念.在精化演算的基础上,构造了一种 数据精化算子,并提出一种基于数据精化演算和程序窗口推理的数据精化的方法.     

一种从Z到精化演算的软件开发方法

一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于形式规约语言。通过语法和语义有严格数学定义的形式规约语言对系统及其各方面性能的描述,产生系统的形式规约,可以帮助开发者获得对所描述系统的深刻理解,并通     

一种从面向对象Z规约到代码的精化演算方法

COOZ(complete object-oriented Z)的优势在于精确描述大型程序的规约.COOZ本身的结构 不支持精化演算,这限制了COOZ的应用能力,使COOZ难以作为完整的方法应用于软件的开发. 将精化演算引入COOZ,弥补了COOZ在设计和实现阶段的不足,同时也消除了规约与实现之间在 结构和表示方法上的完全分离,使程序开发在一个完整的框架下平滑进行.该文提出了基于CO OZ和精化演算的软件开发模型,通过实例讨论了数据精化和操作精化问题.在精化演算实现技 术方面构造了一种数据精化算子,提出一     

一种基于Z和精化演算的形式化开发方法

通过分析Z和精化演算各自的特点,本文提出了一种使两者无缝集成的形式化开发方法。该方法利用Z良好的描述特性和扩充的类机制,将系统规约直妆定义成精化演算中的抽象程序,然后用精化规则对抽象程序逐步精化,直到可执行程序。最后给出了一个简单例子。     

一种将设计模式用于程序精化演算的并行程序设计方法研究

并行程序设计是并行计算的难点之一。提出了一种将设计模式用于程序精化演算的并行程序设计方法。它通过在Z语言的Schema演算体系中扩充并行的概念和表示,使用设计模式,将问题求解和并行开发的知识进行形式化的定义与描述,通过扩充的Schema演算将其与模型规范进行复合,逐步精化得到抽象并行程序。通过实例对这一方法进行了详细的描述。     

基于时序约束建模的自动精化和组合工具

为提供更优质的使用Event-B形式化方法建模混合系统的工具,根据混合系统的时序约束建模方法,其能够很好刻画混合系统建模中的时间相关性质并且支持精化和组合,提出基于它的自动筛选、精化和组合的方法.开发对应的自动精化和组合的工具链,工具链包含模型检测、自动精化和组合、模型证明等一系列功能并拥有用户友好的界面.给出一个使用...     

对象演算Ⅱ

文章应用Goguen等人的结论证明并得到了几个结构化对象演算的基本定理.一方面,这些定理保证了该文可由现有对象的描述构造新对象的描述,并且可以把建立在现有对象上的定理作为整个对象描述和验证的引理.另一方面,文章还讨论了基于封装性的对象精化.于是得到一个结构化的对象演算系统.     

两次数据精化的形式化软件开发方法

提出了一种从数据精化、过程精化、再数据精化的两次数据精化的形式化软件开发方法。传统Z规约数据精化很复杂。该文先采用过程写出初始规范,对模式进行第一次数据精化,然后把它转换为Z模式,再进行过程精化。最后再数据精化到且标代码。以常见动态Web网页脚本语言PHP为例,阐述了该方法。并为此写了一套从过程到Z模式的转化规则,以及精化到PHP的精化规则。     

一种基于构件演算的主动构件精化方法

现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性.     

基于Mealy机精化关系的验证算法

与传统验证方法相比,形式验证技术因其完备性,已在数字电路设计领域中得到越来越多的关注。通过对形式验证技术和状态机的研究,在LTL公式的可实现策略基础上,提出一个基于Mealy机精化关系的验证算法,实现了一个搜索工具原型:支持算术表达式的LTL性质描述,在设计空间中搜索满足给定规范的输入输出信号。该技术可应用于定位电路设计中满足给定功能性质的代码片段。     

基于ORACLE环境的报表生成工具的设计

本文提出了报表信息的本质三个不同层次上的数据约束。一方面通过定义数据约束就可以定报表，另一方面，根据数据约束就能够生成报表数据流。基于这种思想我们在ＯＲＡＣＬＥ环境下开发了一人表生成工具。     

一种Petri网层次模型建模工具的设计与实现

为解决使用Petri网建模遇到的状态空间爆炸问题,提出使用层次模型,采用分层细化逐步求精的方法建立Petri网分层模型.设计并实现基于图形用户界面的普通边界为1的Petri网分层建模工具软件.用户在交互方式下建立Petri网层次模型,并可修改、删除、存储、分层平面化、简单功能模拟、导入和导出可复用Petri子网和将模型翻译为预定义的模型描述语言源程序.     

STEP信息集成软件工具的设计和实现

ＳＴＥＰ是国际标准化组织ＩＳＯ正在组织开发的应用于计算机集成制造系统（ＣＩＭＳ）信息集成的产品数据表达与交换标准，ＳＴＥＰ不仅是一种规范，更是一种信息集成技术，本文以ＣＡＤ／ＣＡＰＰ／ＣＡＭ系统集成为背景，提出了ＳＴＥＰ信息集成支持工具ＥｘＴｒａ的设计和实现技术，该软件工具已成功且有效地应用于ＣＡＤ／ＣＡＰＰ／ＣＡＭ系统集成中。     

A CALCULUS FOR SELF-REFERENCE

An extension of the calculus of indications (of G. Spencer Brown) is presented to encompass all occurrences of self-referential situations. This is done through the introduction of a third state in the form of indication, a state seen to arise autonomously by self-indication. The new extended calculus is fully developed, and some of its consequences for systems, logic and epistemology are discussed     

管理信息系统中自定义报表工具的研究与设计

简述了在一个需求多变的环境下建立一个相对独立的自定义报表工具的必要性及其必须具备的基本功能。在综合分析了当前各类常用报表工具的优缺点之后对它们进行了分类,并选择其一恰当者作为我们开发自定义报表工具的基础。然后详细阐述了一个具体的报表工具的设计方法,数据模型,用户接口及执行流程。最后,阐述了该报表工具在几个不同类型的应用程序中的使用效果,并指出了它的局限性和有效性。     

面向对象的工程设计专家系统开发工具OOESTOOL

本文介绍了一个用C 语言开发的支持面向对象功能的工程设计专家系统开发工具OOESTOOL。我们以面向对象的软件开发方法分析并设计OOESTOOL的组成和结构,初步建立了面向对象的知识表示机制和面向对象推理系统,并讨论了面向对象的工程数据库的设计与实现。     

支持软件详细设计工具JS—PDL／C的设计与实现

ＰＤＬ是在ＣＡＳＥ中使用非常广泛的一种软件详细设计方法和工具。ＪＳ－ＰＤＬ是集成环境ＪＳ－ＳＣＡＳ中基于ＰＤＬ方法的详细设计工具，是支持交互式，多窗口和菜单驱动的工作方式。它把概要设计阶段产生的结构图和模块说明自动转换成最初的详细设计档，通过对最初详细设计文档的编辑、逐步精化以及部分自动转换，从而生成Ｃ语言程序和各种详细设计文档。     

模拟器采样工具设计与实现

采样技术作为一种高效的模拟器加速手段,目前已得到广泛的应用。但采样技术通常需要使用大量的数据分析算法,因此,如何方便快捷地集成采样技术所需的各种算法,不仅可以让采样技术更加简单易用,也能够提高对新采样技术的评估效率。设计并实现了针对采样技术的自动化工具,该工具可以让用户自己设计采样算法,并且能自动且高效地完成采样算法的分析。实验数据表明,该工具能自动且高效地完成采样算法的分析,同时具有运算速度快、可扩展性强等优点。