由规格说明到排序算法

本文给出由程序的规格说明变换出程序的一种系统化方法的新概念.对规格说明进行不同的变换可得到不同的不变式形式.这些不变式通过计算最弱前置条件给出了多种相应算法的框架。本文以若干著名的排序算法例示了以上的概念和方法。     

面向对象软件的形式规格说明技术

本文介绍四种面向对象形式规格语言。Object-Z是Z语言的一种扩充,可用于面向对象软件需求规格的形式说明。为研究软件维护和逆向工程,提出了Z~(++),是Z的另一种扩充,其中引入了过程式描述机制。COLD-K是基于代数规格说明技术的面向对象软件设计语言,是一种核心语言,可设计面向用户的形式规格语言,JOOSL是基于COLD-K和Z语言的一种面向对象设计语言,可用于软件自动化的研究。     

基于Object—Z的形式化验证方法

定理证明是一种形式化验证技术，也是形式化方法的重要组成部分，它能从形式规格说明中推理出应具备的性质与属性，从而可以对规格说明进行形式验证。Obiect-Z是形式规格说明语言Z的面向对象扩充，基于集合论与数理逻辑，具有严密的逻辑性，适合精确地描述大型软件系统，并且可以对其形式规格说明进行推理。本文首先给出了基于Object—Z规格说明的定理证明验证方法，接着用Object-Z描述了一个电梯操作系统的实例，在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。     

从集合表达式产生测试数据的方法

软件测试保证和提高了软件质量,因此成为软件界最为关心的问题之一.测试数据的好坏直接影响软件测试的效果.形式规格说明中的前置条件可用来产生测试数据.而前置条件是基于关系操作符的谓词表达式.给出了一个针对集合关系表达式的测试准则和产生符合测试准则的测试数据的算法,根据该测试准则产生的测试数据对于集合条件表达式有比较好的错误检测能力.从给出的数据库查询的例子说明了该方法对于检测代码错误的有效性.     

基于解释的算法构架的学习

本文提出了将解释学习方法用于学习算法构架的思想，以提高软件自动化系统从功能规格说明转换到设计规格说明的能力．文中给出了算法构架的表示，操作性的定义及其处理方法．系统从用户给出的一个问题的解中学习算法构架，用于解决一类问题，系统的学习效果表现为通过学习能够解决原来不能解的问题．     

空间完备性理论及其测试

证明和测试是验证规格说明是否正确的2种方法，两者互为补充。针对软件规格说明难以证明的问题，提出对状态空间进行完备性测试的理论。采用构造函数和受限状态空间的概念，讨论用于测试Z规格说明语言初始状态存在性的方法，通过实例证明该方法的可行性。     

Object—Z规格说明的SQL动画模拟

软件规格说明的确认在软件开发阶段占有举足轻重的地位。形式规格说明的动画模拟技术是一种规格说明的确认方法。本文研究了Obiect-Z规格说明的SQL动画模拟方法，设计了从Object-Z到SQL的转换规则，并提出了模块封装的思想，即用存储过程表示类、对象和模式等模块，用户通过调用执行存储过程确认规格说明是否满足其需求。     

两种形式语言:RSL与Z的分析比较

RSL(RAISE规格说明语言)和Z是目前广泛应用的软件规格说明语言,本文从软件开发生命周期的角度对两种语言进行了比较,提出了将不同规格说明语言结合形式地描述系统的设想。     

基于问题模式的形式化软件规格说明生成方法

精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明.     

Z的面向对象扩充COOZ的设计

为了使Z规格说明与面向对象开发方法相结合，本文在Z中扩充了对象类型和模块描述机制，使之成为面向对象的形式化规格说明语言COOZ（completeobject－orientedZ）．内容包括COOZ的设计思想、语法定义及说明、形式化语义、实例以及与相关研究工作的比较．     

ZRC – A Refinement Calculus for Z

The fact that Z is a specification language only, with no associated program development method, is a widely recognised problem. As an answer to that, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows its style and conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly in that ZRC is completely formalised. In this paper, we explain how programs can be derived from Z specifications using ZRC. We present ZRC-L, the language of our calculus, and its conversion laws, which are concerned with the transformation of Z schemas into programs of this language. Moreover, we present the weakest precondition semantics of ZRC-L, which is the basis for the derivation of the laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement for Z. Received July 1997 / Accepted in revised form October 1998     

从类树形流程图到Z语言的形式化规格

在软件工程中,使用Z语言形式化规格可以大大提高软件开发质量,提高稳定性,降低开发成本,但要开发出高质量的形式化规格并通过验证,却需要损耗较多的时间和精力.为使软件开发人员能够较快地并且高质量地开发出基于Z语言的形式化规格,提出一种简明的类树形流程图,并以电信服务系统中的呼叫转移功能模块为例子,详细描述如何把类树形流程图应用到Z语言的形式化规格开发当中,以期为开发人员带来便利,节省开发时间,提高形式化规格的质量.     

Managing complex documents over the WWW: a case study for XML

The use of the World Wide Web as a communication medium for knowledge engineers and software designers is limited by the lack of tools for writing, sharing, and verifying documents written with design notations. For instance, the Z language has a rich set of mathematical characters, and requires graphic-rich boxes and schemas for structuring a specification document. It is difficult to integrate Z specifications and text on WWW pages written with HTML, and traditional tools are not suited for the task. On the other hand, a newly proposed standard for markup languages, namely XML, allows one to define any set of markup elements; hence, it is suitable for describing any kind of notation. Unfortunately, the proposed standard for rendering XML documents, namely XSL, provides for text-only (although sophisticated) rendering of XML documents, and thus it cannot be used for more complex notations. We present a Java-based tool for applying any notation to elements of XML documents. These XML documents can thus be shown on current-generation WWW browsers with Java capabilities. A complete package for displaying Z specifications has been implemented and integrated with standard text parts. Being a complete rendering engine, text parts and Z specifications can be freely intermixed, and all the standard features of XML (including HTML links and form elements) are available outside and inside Z specifications. Furthermore, the extensibility of our engine allows any additional notations to be supported and integrated with the ones we describe     

Using formal specifications to support software testing

Formal specifications become more and more important in the development of software, especially but not only in the area of high integrity system design. In this paper it is demonstrated, how, apart from the specification phase, further benefits may be drawn from formal specifications for checking the implementation against the specification. It is shown how the specification can be used for systematically deriving test input data and for automatically evaluating test results. The approach is illustrated using the specification language Z. The same principles may be applied to other specification languages. The approach allows a high degree of automation, drastically improving productivity and quality of the testing process.     

规格说明语言Z的类型检查

软件规格说明的正确性是软件目标代码正确性的前提。正确性要求这一就是类型正确。本文介绍Ｚ规格说明类型的检查器的实现方法,并对类型检查的环境、一致化方法、替换策略和类型变量的应用等问题进行讨论。     

Synthesizing structured analysis and object‐based formal specifications

Structured Analysis (SA) is a widely‐used software development method. SA specifications are based on Data Flow Diagrams (DFD's), Data Dictionaries (DD's) and Process Specifications (P‐Specs). As used in practice, SA specifications are not formal. Seemingly orthogonal approaches to specifications are those using formal, object‐based, abstract model specification languages, e.g., VDM, Z, Larch/C++ and SPECS. These languages support object‐based software development in that they are designed to specify abstract data types (ADT's). We suggest formalizing SA specifications by: (i) formally specifying flow value types as ADT's in DD's, (ii) formally specifying P‐Specs using both the assertional style of the aforementioned specification languages and ADT operations defined in DD's, and (iii) adopting a formal semantics for DFD “execution steps”. The resulting formalized SA specifications, DFD‐SPECS, are well‐suited to the specification of distributed or concurrent systems. We provide an example DFD‐SPEC for a client‐server system with a replicated server. When synthesized with our recent results in the direct execution of formal, model‐based specifications, DFD‐SPECS will also support the direct execution of specifications of concurrent or distributed systems.     

Experience with logical code analysis in software maintenance

Formal program specification and logical analysis are often used for program derivation and proofs of correctness. The basic tools include the logic of predicate calculus and Dijkstra's weakest precondition calculations. Recent work has shown that these tools are also very useful in the maintenance phase of the software life-cycle. This paper reports experience working with software maintenance teams to apply formal methods. Formal logical analysis is invaluable for isolating defects, determining code corrections, eliminating side-effects, and code re-engineering. Logical analysis works well in software maintenance because many defects can be isolated to small segments of code. These small segments can then be analyzed manually or with code analysis tools. The result is lowered software maintenance costs due to the benefits of defect prevention, reduction of code complexity metrics, productivity improvements, and better specifications and documentation. It would be beneficial to use logical code analysis in the earlier phases of the software life-cycle, such as quality assurance and inspection.     

用UML描述组件规格说明

在基于组件的软件开放方式（CBD）下，软件系统是一些盯互联系的可重用组件的集合，因此需要对系统的每一个组件以及组件之间的相互关系有很好的理解。UML作为一种标准建模语言，不仅可以支持面向对象的分析与设计，而且能够有力地支持从需求分析开始的软件开发全过程。但是UML对组件建模的支持并不理想，这就需要开发一种能很好支持组件建模的方法。本文提出一种用UML描述组件规格说明的方法。将组件规格说明分解成组件接口规格说明。通过对组件的每个接口和组件接口之间的相互关系加以形式描述，从而达到组件规格说明的清晰性和精确性。     

Translation of Z specifications to executable code: Application to the database domain

ContextIt is well-known that the use of formal methods in the software development process results in high-quality software products. Having specified the software requirements in a formal notation, the question is how they can be transformed into an implementation. There is typically a mismatch between the specification and the implementation, known as the specification-implementation gap.ObjectiveThis paper introduces a set of translation functions to fill the specification-implementation gap in the domain of database applications. We only present the formal definition, not the implementation, of the translation functions.MethodWe chose Z, SQL and Delphi languages to illustrate our methodology. Because the mathematical foundation of Z has many properties in common with SQL, the translation functions from Z to SQL are derived easily. For the translation of Z to Delphi, we extend Delphi libraries to support Z mathematical structures such as sets and tuples. Then, based on these libraries, we derive the translation functions from Z to Delphi. Therefore, we establish a formal relationship between Z specifications and Delphi/SQL code. To prove the soundness of the translation from a Z abstract schema to the Delphi/SQL code, we define a Z design-level schema. We investigate the consistency of the Z abstract schema with the Z design-level schema by using Z refinement rules. Then, by the use of the laws of Morgan refinement calculus, we prove that the Delphi/SQL code refines the Z design-level schema.ResultsThe proposed approach can be used to build the correct prototype of a database application from its specification. This prototype can be evolved, or may be used to validate the software requirements specification against user requirements.ConclusionTherefore, the work presented in this paper reduces the overall cost of the development of database applications because early validation reveals requirement errors sooner in the software development cycle.