Search

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and post-conditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it to the construction of the classical Deutsch–Schorr–Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover.

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and postconditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it the the construction of the classical Deutsch-Schorr-Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover.

We introduce a new algebraic model for program variables, suitable for reasoning about recursive procedures with parameters and local variables in a mechanical verification setting. We give a predicate transformer semantics to recursive procedures and prove refinement rules for introducing recursive procedure calls, procedure parameters, and local variables. We also prove, based on the refinement rules, Hoare total correctness rules for recursive procedures, and parameters. We introduce a special form of Hoare specification statement which alone is enough to fully specify a procedure. Moreover, we prove that this Hoare specification statement is equivalent to a refinement specification. We implemented this theory in the PVS theorem prover.

We consider the notion of a contract that governs the behavior of a collection of agents. In particular, we study the question of whether a group among these agents can achieve a given goal by following the contract. We show that this can be reduced to studying the existence of winning strategies in a two-person game. A notion of correctness and refinement is introduced for contracts and contracts are shown to form a lattice and a monoid with respect to the refinement ordering. We define a weakest precondition semantics for contracts that permits us to compute the initial states from which a group of agents has a winning strategy to reach their goal. This semantics generalizes the traditional predicate transformer semantics for program statements to contracts and games. Ordinary programs and interactive programs are special kinds of contracts.

In the refinement calculus, program statements are modelled as predicate transformers. A product operator for predicate transformers was introduced by Martin [18] and Naumann [25] using category theoretic considerations. In this paper, we look more closely at the refinement-oriented properties of this operator and at its applications. We also generalise the definition of the product operator to form what we call a fusion operator. Together, the fusion and product operators provide us with algebraic ways of composing program statements in the refinement calculus in order to model effects such as conjunction of specifications, simultaneous execution, and embedding of smaller programs into larger contexts.

An action system is a framework for describing parallel or distributed systems, for which the refinement calculus offers a formalisation of the stepwise development method. Fairness is an important notion in modelling parallel or distributed systems, and this paper investigates a calculus for refinement of fair action systems. Simulations, which are proof techniques for refinement, are extended to verify fair action systems. Our work differs from others' in that the additional condition concerning fairness is expressed through termination of related iteration statements. For this purpose, existing proof rules for termination are extended. In the tradition of the refinement calculus, our approach to fairness is based on techniques developed mainly for sequential programming.

Superposition refinement enhances an algorithm by superposing one computation mechanism onto another mechanism, in a way that preserves the behavior of the original mechanism. Superposition seems to be particularly well suited to the development of parallel and distributed programs: an originally simple sequential algorithm can be extended with mechanisms that distribute control and state information to many processes, thus permitting efficient parallel execution of the algorithm. We will show in this paper how superposition of reactive systems is expressed in the refinement calculus. We illustrate the power of this method by a case study, showing how a distributed broadcasting system is derived through a sequence of superposition refinements.

We describe a foundation for refinement calculus where pro- grams and systems are described as contracts, carried out by a collection of interacting agents. The contract states explicitly what the agents are allowed to do, and who is to blame if things go wrong. A contract can be analyzed from the point of view of any participating agent or coalition of agents, to see what kind of goals the agents can achieve by following the contract. We give an intuitive overview of contracts in this setting, and then continue to describe the mathematical and logical foundations of the calculus. We show how contracts provide a unified framework for a number of seemingly different paradigms in computer science, such as concurrency, interactivity, games, temporal behavior vs input-output computation and high level system design.

The refinement calculus and the action system formalism are combined to provide a uniform method for constructing parallel and distributed algorithms by stepwise refinement. It is shown that the sequencial refinement calculus can be used as such for most of the derivation steps. Parallelism is introduced during the derivation by refinement of atomicity. The approach is applied to the derivation of a parallel version of the Gaussian elimination method for solving simultaneous linear equation systems.

We propose here a mathematical framework for incremental software construction and controlled software evolution. The framework allows incremental changes of a software system to be described on a high architecture level, but still with mathematical precision so that we can reason about the correctness of the changes. The framework introduces refinement diagrams as a visual way of presenting the architecture of large software systems. Refinement diagrams are based on lattice theory and allow reasoning about lattice elements to be carried out directly in terms of diagrams. A refinement diagram proof will be equivalent to a Hilbert like proof in lattice theory. We show how to apply refinement diagrams and refinement calculus to the incremental construction of large software system. We concentrate on three topics: (i) modularization of software systems with component specifications and the role of information hiding in this approach, (ii) layered extension of software by adding new features one-by-one and the role of inheritance and dynamic binding in this approach, and (iii) evolution of software over time and the control of successive versions of software.

In this paper we extend the model of program variables from the Refinement Calculus [2] in order to be able to reason more algebraically about recursive procedures with parameters and local variables. We extend the meaning of variable substitution or freeness from the syntax to the semantics of program expressions. We give a predicate transformer semantics to recursive procedures with parameters and prove a refinement rule for introduction of recursive procedure calls. We also prove a Hoare total correctness rule for our recursive procedures. These rules have no side conditions and are easier to apply to programs than the ones in the literature. The theory is built having in mind mechanical verification support using theorem provers like PVS [18] or HOL [11].

Continuous action systems (CAS) is a formalism intended for modeling hybrid systems (systems that combine discrete control with continuous behavior), and proving properties about the model within refinement calculus. We use a symbolic manipulation program to build a tool for simulating CAS models by, calculating symbolically the time evolution of the discrete and continuous CAS model functions, as explicit and exact expressions of a continuous time variable. We may then study the time behavior and general properties of the model by plotting these functions with respect to time. For certain models our tool eliminates the need for introducing tolerances into the model structure. The tool is useful for checking that the model behaves correctly, and we can sometimes study the behavior of CAS models with in principle infinite precision.

It is shown how to change the data representation in programs (data refinement) systematically within refinement calculus. Data refinement in the original refinement calculus was only defined for functional data abstractions. It is shown how the method can be extended to nonfunctional data abstraction by adding 'don't know' (or angelic) nondeterminism to the usual 'don't care' (or demonic) nondeterminism. The method is very flexible, permitting different data abstractions to be combined in the same statement, as well as refinements of the data abstractions themselves. The flexibility is illustrated by an example program derivation. >

An overview of the refinement calculus and of the action system paradigm for constructing parallel and reactive systems is given. Superposition is studied in detail, as an example of an important method for refinement of reactive programs. In connection with superposition, fairness of action system execution is considered, and a proof rule for preserving fairness in superposition refinement is given. >

Refinement calculus [1,5] is a formal framework for reasoning about program correctness and correctness preserving program refinements. It serves as the foundation for an object-oriented software architecture and construction method that we refer to as stepwise feature introduction (SFI) [3]. Characteristic for this approach is that each software module is described in terms of thin layers. Each layer extends the software with some new feature, in a way that preserves the features that have been introduced by earlier layers. This amounts to requiring that the new layer is a superposition refinement [4] of the layers below. The modules are interconnected using interface specifications, usually providing a more abstract view of the module state than what will actually be implemented. The implementation is required to be a data refinement [9,6] of the interface specification. SFI is based on structuring software with these two basic mechanisms, modularization and extension, while the refinement calculus provides the formal framework for reasoning about the correctness of software constructed in this way.We use UML [8] to describe the software architecture, with refinement calculus providing a rigorous mathematical semantics for the UML constructs employed. This will also give us a formal framework for reasoning about UML class diagrams, in essence using these as proof schemes when arguing about software properties.

We study a method for software construction that is based on introducing new features to an evolving system one by one. A layered software architecture is proposed to support this method. We show how to describe the software with UML diagrams. We provide an exact semantics for the UML diagrams employed in the software architecture, using refinement calculus as the logical framework and show how to reason about software correctness in terms of these UML diagrams.

We have looked at recursion and iteration in general in the preceding chapters. In this chapter, we will show that the refinement calculus framework is usable beyond its original area of application, by showing how to model and analyze two-person games in the calculus. We show how to use total correctness reasoning to show the existence of winning strategies for such games. Furthermore, we show how one can derive a program that actually plays a game against an opponent. We choose the game of nim as an example and study it within the refinement calculus framework.

The predicate transformers that we use to model contracts are constructed from other predicate transformers or from simpler elements, like state predicates, state transformers, or state relations. The predicate transformer constructors can thus be seen as functions that map elements in one domain to the domain itself or to another domain. The basic question that we investigate in this chapter is to what extent the lattice and category structure is preserved by these constructors, i.e., to what extent the constructors are monotonic and homomorphic.

We extend the Action-Oberon language for executing action systems with type-bound actions. Type-bound actions combine the concepts of type-bound procedures (methods) and actions, bringing object orientation to action systems. Type-bound actions are created at runtime along with the objects of their bound types. They permit the encapsulation of data and code in objects. Allowing an action to have more than one participant gives us a mechanism for expressing n-ary communication between objects. By showing how type-bound actions can logically be reduced to plain actions, we give our extension a firm foundation in the Refinement Calculus.

We introduce a simple programming language and define its predicate transformer semantics. We motivate the choice of the constructs for the language by algebraic arguments, showing that the constructs are essentially the basic algebraic operations that are available for predicate transformers, when these are viewed as forming a complete lattice enriched category. We then show that the statements in the language can be given a simple operational interpretation, as describing the interaction between a user and a computing system. This gives a general intuitive interpretation of angelic and demonic nondeterminism. We also consider the notion of correctness and refinement of program statements that this intuitive interpretation gives rise to, and show the connection between the user-system interpretation and the interpretation of program execution as a game.

Product and summation operators for predicate transformers were introduced by Naumann and by Martin using category theoretic considerations. In this paper, we formalise these operators in the higher order logic approach to the refinement calculus of Back and von Wright, and examine various algebraic properties of these operators. There are several motivating factors for this analysis. The product operator provides a model of simultaneous execution of statements, while the summation operator provides a simple model of late binding. We also generalise the product operator slightly to form an operator that corresponds to conjunction of specifications. We examine several applications of the these operators showing, for example, how a combination of the product and summation operators could be used to model inheritance in an object-oriented programming language.

Action systems are used to extend program refinement methods for sequential programs, as described in the refinement calculus, to parallel and reactive system refinement. They provide a general description of reactive systems, capable of modeling terminating, possibly aborting and infinitely repeating systems. We show how to extend the action system model to refinement of modular systems. A module may export and import variables, it may provide access procedures for other modules, and it may itself access procedures of other modules. Modules may have autonomous internal activity and may execute in parallel or in sequence. Modules may be nested within each other. They may communicate by shared variables, shared actions, a generalized form of remote procedure calls and by persistent data structures. Both synchronous and asynchronous communication between modules is supported. The paper shows how a single framework can be used for both the specification of large systems, the modular decomposition of the system into smaller units and the refinement of the modules into program modules that can be described in a standard programming language and executed on standard hardware.

We show how to describe refinement calculus in a lattice theoretic framework. The predicate transformer lattice is built by pointwise extensions from the truth value lattice. A simple but very powerful statement language characterizes the monotonic predicate transformer lattice. We show how to formalize the calculus in higher order logic. We also show how to express data refinement in this framework. A theorem of data refinement with stuttering is proved, to illustrate the algebraic nature of reasoning in this framework.

Superposition refinement enhances an algorithm by superposing one computation mechanism onto another mechanism, in a way that preserves the behavior of the original mechanism. Superposition seems to be particularly well suited to the development of parallel and distributed programs. An originally simple sequential algorithm can be extended with mechanisms that distribute control and state information to many processes, thus permitting efficient parallel execution of the algorithm. We will in this paper show how superposition of parallel algorithms is expressed in the refinement calculus. We illustrate the power of this method by a case study, showing how a distributed broadcasting algorithm is derived through a sequence of superposition refinements.

It is shown how to apply the refinement calculus to stepwise refinement of both parallel programs and reactive programs. The approach is based on using the action systems model to describe parallel and reactive systems. Action systems are sequential programs which can be implemented in a parallel fashion. Hence the refinement calculus for sequential programs carries over to the parallel programs expressed in this framework. Refinement of reactive programs can be expressed and proved in the refinement calculus by using the methods of data refinement from the sequential refinement calculus.

The stepwise refinement technique is studied from a mathematical point of view. A relation of correct refinement between programs is defined, based on the principle that refinement steps should be correctness preserving. Refinement between programs will therefore depend on the criterion of program correctness used. The application of the refinement relation in showing the soundness of different techniques for refining programs is discussed. Special attention is given to the use of abstraction in program construction. Refinement with respect to partial and total correctness will be studied in more detail, both for deterministic and nondeterministic programs. The relationship between these refinement relations and the approximation relation of fixpoint semantics will be studied, as well as the connection with the predicate transformers used in program verification.