56 research outputs found
Exploring Summation and Product Operators in the Refinement Calculus
No full textProduct 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
A continuous semantics for unbounded nondeterminism
No full textAbstractNondeterminism is introduced into an ordinary iterative programming language by treating procedure calls as nondeterministic assignment statements. The effect of such assignment statements is assumed to be determined solely by the entry-exit specifications of the corresponding procedures. The nondeterminism which this approach yields is not necessarily bounded. The paper discusses the problem of defining a denotational semantic for programming languages with this kind of, possibly unbounded, nondeterminism. As an additional constraint, the semantics is required to be continuous, in the sense that the underlying semantic algebra is continuous. It is shown how such a continuous semantics for unbounded nondeterminism can be derived from a simple operational semantics based on program execution trees
On correct refinement of programs
No full textAbstractThe 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
Proceedings of the Second International Workshop on Computational Models for Cell Processes
No full textA semantic approach to program modularity
No full textModularity in programs is studied from a semantic point of view. A simple model of modular systems and modularization mechanisms is presented, together with correctness criteria for modular systems. A concept of locality is defined for modular systems and modularization mechanisms. In a local modular system the correctness of each module can be established by only looking at the module specifications, i.e., without using any information about how the modules are implemented. Locality is thus a basic property of modular systems and justifies the use of Parnas' information hiding principle in the construction of modular systems. A characterization of locality is given, and the locality of hierarchical and recursive modular systems is studied. Hierarchical modular systems are shown always to be local, while recursive systems need not be local. A sufficient condition for the locality of recursive modular systems is given. Finally, the composition of modular systems to yield higher level modular systems is described and analyzed. It is shown that locality of modular systems is preserved in a hierarchical composition of modular systems. Correctness of hierarchically composed modular systems is analyzed and sufficient conditions for establishing it are given
Stepwise refinement of parallel algorithms
No full textAbstractThe 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
On the suitability of trace semantics for modular proofs of communicating processes
No full textAbstractThe question of whether a semantic model is suitable for the construction of a modular proof system is studied in detail. The notion of one semantic model being a (full) abstraction of another semantic model with respect to a given class of properties is introduced, and is used in analyzing different semantic models for communicating processes. A trace model for communicating processes is described and shown to be suitable for the construction of a modular proof system in which partial correctness assertions about communicating processes can be expressed
- …
