The Variety of Variables in Computer-Aided Real-Time Programming

The refinement calculus is a well-established theory for translating specifications to program code. Recent research has extended the calculus to handle real-time requirements and we have developed an interactive support tool based on these extensions. Via a case study, this paper shows how the tool helps the programmer by supporting the many forms of variables used in the theory. These include simple state variables as in the untimed calculus, timed-trace variables that model the evolution of properties over time, and auxiliary variables that exist to support formal reasoning only.     

A formal software development approach using refinement calculus

The advantage of COOZ(Complete Object-Oriented Z) is to specify large scale software,but it does not support refinement calculus.Thus its application is comfined for software development.Including refinement calculus into COOZ overcomes its disadvantage during design and implementation.The separation between the design and implementation for structure and notation is removed as well .Then the software can be developed smoothly in the same frame.The combination of COOZ and refinement calculus can build object-oriented frame,in which the specification in COOZ is refined stepwise to code by calculus.In this paper,the development model is established.which is based on COOZ and refinement calculus.Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement,since data refinement usually has to be done on a large program component at once.As to the implementation technology of refinement calculus,the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.     

The Variety of Variables in Automated Real-Time Refinement

The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.     

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

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

A framework for automated and certified refinement steps

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma.     

A Program Refinement Tool

The refinement calculus for the development of programs from specifications is well suited to mechanised support. We review the requirements for tool support of refinement as gleaned from our experience with existing refinement tools, and report on the design and implementation of a new tool to support refinement based on these requirements. The main features of the new tool are close integration of refinement and proof in a single tool (the same mechanism is used for both), good management of the refinement context, an extensible theory base that allows the tool to be adapted to new application domains, and a flexible user interface. Received June 1997 / Accepted in revised form June 1998     

Mechanizing some advanced refinement concepts

We describe how the HOL theorem prover can be used to check and apply rules of program refinement. The rules are formulated in the refinement calculus, which is a theory of correctness preserving program transformations. We embed a general command notation with a predicate transformer semantics in the logic of the HOL system. Using this embedding, we express and prove rules for data refinement and superposition refinement of initialized loops. Applications of these proof rules to actual program refinements are checked using the HOL system, with the HOL system generating these conditions. We also indicate how the HOL system is used to prove the verification conditions. Thus, the HOL system can provide a complete mechanized environment for proving program refinements.     

A Logic for Schema-Based Program Development

We show how a theory of specification refinement and program development can be constructed as a conservative extension of our existing logic for Z. The resulting system can be set up as a development method for a Z-like specification language, or as a generalisation of a refinement calculus (with a novel semantics). In addition to the technical development we illustrate how the theory can be used in practice.     

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     

A calculus of refinements for program derivations

Summary A calculus of program refinements is described, to be used as a tool for the step-by-step derivation of correct programs. A derivation step is considered correct if the new program preserves the total correctness of the old program. This requirement is expressed as a relation of (correct) refinement between nondeterministic program statements. The properties of this relation are studied in detail. The usual sequential statement constructors are shown to be monotone with respect to this relation and it is shown how refinement between statements can be reduced to a proof of total correctness of the refining statement. A special emphasis is put on the correctness of replacement steps, where some component of a program is replaced by another component. A method by which assertions can be added to statements to justify replacements in specific contexts is developed. The paper extends the weakest precondition technique of Dijkstra to proving correctness of larger program derivation steps, thus providing a unified framework for the axiomatic, the stepwise refinement and the transformational approach to program construction and verification.     

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

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

精化演算支撑工具的分析

利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。     

Real-time refinement in Manna and Pnueli's temporal logic

A refinement calculus for the development of real-time systems is presented. The calculus is based upon a wide-spectrum language called TAM (the Temporal Agent Model), within which both functional and timing properties can be expressed in either abstract or concrete terms. A specification oriented semantics is given for the language. Program development is considered as a refinement process i.e. thecalculation of a structured program from an unstructured specification. An example program is developed.     

Exits in the refinement calculus

Although many programming languages contain exception handling mechanisms, their formal treatment — necessary for rigorous development — can be complex. Nevertheless, this paper presents a simple incorporation ofexit commands and exception blocks into a rigorous program development method. The refinement calculus, chosen for the exercise, is a method of developing imperative programs. It is based on weakest preconditions, although they are not used explicitly during program construction; they merely justify the general method. In the style of the refinement calculus, program development laws are given that introduce and allow the manipulation ofexits. The soundness of the new laws is shown using weakest preconditions (as for the existing refinement calculus laws). The extension of weakest preconditions needed to handleexits is a variation on earlier work of Cristian; the variation is necessary to handle nondeterminism.     

The Least Conjunctive Refinement and Promotion in the Refinement Calculus

A syntactic calculation of Morgan's least conjunctive refinement operator for predicate transformers is developed. The operator is used to develop a general approach to lifting relational operators to predicate transformer operators. Predicate transformer versions of the relational conjunction and disjunction operators are considered in detail. The Z-based technique of program promotion is considered in a refinement calculus setting. A standard Z promotion example is recast in the refinement calculus. Received August 1997 / Accepted in revised form January 1999     

用Petri网描述程序精化中的循环不变式

形式化方法把程序看成规范,形式化开发方法包括形式规范和规范（程序）的精化。精化演算方法能够通过演算的方式,把规范逐步精化为程序。然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的。形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序。因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索。     

A sequential real-time refinement calculus

We present a comprehensive refinement calculus for the development of sequential, real-time programs from real-time specifications. A specification may include not only execution time limits, but also requirements on the behaviour of outputs over the duration of the execution of the program. The approach allows refinement steps that separate timing constraints and functional requirements. New rules are provided for handling timing constraints, but the refinement of components implementing functional requirements is essentially the same as in the standard refinement calculus. The product of the refinement process is a program in the target programming language extended with timing deadline directives. The extended language is a machine-independent, real-time programming language. To provide valid machine code for a particular model of machine, the machine code produced by a compiler must be analysed to guarantee that it meets the specified timing deadlines. Received: 27 September 1997 / 13 June 2000     

Program families: Program construction by context independent refinements

The concept of program families is a generalisation of the conventional stepwise refinement paradigm. We formalise program families by allowing Hoare-triplets to be parameterized. Next we derive a simple calculus to develop programs which are known a priori to be correct with respect to explicitly formulated pre- and postconditions.

Program families deal with at least two important problems of conventional refinement steps, i.e. program families are not context dependent and they apply just as well to top-down decomposition as to the bottom-up or middle-out approach. It turns out that the meaning of a pseudostatement in the context of program families is quite different from its meaning in the conventional refinement process.

A couple of examples illustrate the technique: the 1000 primes problem, a palindrome filter and a sorting routine.

The discussion relates program families to Morgan's refinement calculus, Knuth' literate programming and Soloway's programming plans.     

Simply-typed Underdeterminism

An extension of the simply-typed lambda calculus with constructs for expressing a notion called underdeterminism is studied.This allows us to interpret notions of stud and skeleton used in top-down program development.We axionatise a simple notion of program refinement,and give a semantics,for which the calculus is proved sound and complete.     

Refinement calculus: A basis for translation validation,debugging and certification

In this paper, we show how refinement calculus provides a basis for translation validation of optimized programs written in high level languages. Towards such a direction, we shall provide a generalized proof rule for establishing refinement of source and target programs for which one need not have to know the underlying program transformations. Our method is supported by a semi-automatic tool that uses a theorem prover for validating the verification conditions. We further show that the translation validation infrastructure provides an effective basis for deriving semantic debuggers and illustrate the development of a simple debugger for optimized programs using this approach using Prolog. A distinct advantage of semantic debugging is that it permits the user to change values at run-time only when the values are consistent with the underlying semantics.