nach oben

2010 | Buch

Kapitel lesen Erstes Kapitel lesen

Unifying Theories of Programming

Second International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected Papers

herausgegeben von: Andrew Butterfield

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Inhaltsverzeichnis

Frontmatter

Refinement Calculus as a Theory of Contracts (Invited Paper)

Abstract

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.

Ralph-Johan Back

Transaction Calculus

(Invited Paper)

Abstract

Transaction-based services are increasingly being applied in solving many universal interoperability problems. Compensation is one typical feature for long-running transactions. This paper presents a design model for specifying the behaviour of compensable programs. The new model for handling exception and compensation is built as conservative extension of the standard relational model. The paper puts forward a mathematical framework for transactions where a transaction is treated as a mapping from its environment to compensable programs. We propose a transaction refinement calculus, and show that every transaction can be converted to a primitive one which simply consists of a forward activity and a compensation module.

He Jifeng

UTP and Temporal Logic Model Checking

Abstract

In this paper we give an additional perspective to the formal verification of programs through temporal logic model checking, which uses Hoare and He Unifying Theories of Programming (UTP). Our perspective emphasizes the use of UTP designs, an alphabetised relational calculus expressed as a pre/post condition pair of relations, to verify state or temporal assertions about programs. The temporal model checking relation is derived from a satisfaction relation between the model and its properties. The contribution of this paper is that it shows a UTP perspective to temporal logic model checking. The approach includes the notion of efficiency found in traditional model checkers, which reduced a state explosion problem through the use of efficient data structures

Hugh Anderson, Gabriel Ciobanu, Leo Freitas

A Note on Traces Refinement and the conf Relation in the Unifying Theories of Programming

Abstract

There is a close relation between the failures-divergences and the UTP models of CSP, but they are not equivalent. For example, miracles are not available in the failures-divergences model; the UTP theory is richer and can be used to give semantics to data-rich process algebras like Circus. Previously, we have defined functions that calculate the failures-divergences model of a CSP process characterised by a UTP relation. In this note, we use these functions to calculate the UTP characterisations of traces refinement and of the conf relation that is widely used in testing. In addition, we prove that the combination of traces refinement and conf corresponds to refinement of processes in Circus. This result is the basis for a formal testing technique based on Circus; as usual in testing, we restrict ourselves to divergence-free processes.

Ana Cavalcanti, Marie-Claude Gaudel

Reasoning about Loops in Total and General Correctness

Abstract

We introduce a calculus for reasoning about programs in total correctness which blends UTP designs with von Wright’s notion of a demonic refinement algebra. We demonstrate its utility in verifying the familiar loop-invariant rule for refining a total-correctness specification by a while loop. Total correctness equates non-termination with completely chaotic behaviour, with the consequence that any situation which admits non-termination must also admit arbitrary terminating behaviour. General correctness is more discriminating in allowing non-termination to be specified together with more particular terminating behaviour. We therefore introduce an analogous calculus for reasoning about programs in general correctness which blends UTP prescriptions with a demonic refinement algebra. We formulate a loop-invariant rule for refining a general-correctness specification by a while loop, and we use our general-correctness calculus to verify the new rule.

Steve E. Dunne, Ian J. Hayes, Andy J. Galloway

Lazy UTP

Abstract

We integrate non-strict computations into the Unifying Theories of Programming. After showing that this is not possible with designs, we develop a new relational model representing undefinedness independently of non-termination. The relations satisfy additional healthiness conditions that model dependence in computations in an elegant algebraic form using partial orders. Programs can be executed according to the principle of lazy evaluation, otherwise known from functional programming languages. We extend the theory to support infinite data structures and give examples to show their use in programs.

Walter Guttmann

Monadic Maps and Folds for Multirelations in an Allegory

Abstract

This paper contributes to the unification of semantic models and program development techniques by making a link from multirelations and predicate transformer semantics to algebraic semantics and the derivation of programs by calculation, as used in functional programming and relational program development. Two common ways to characterise iteration, namely the functional programming operators map and fold, are extended to multirelations, using concepts from category theory, power allegories and monads.

C. E. Martin, S. A. Curtis

Unifying Theories of Interrupts

Abstract

The concept of an interrupt is one that appears across many paradigms, and used in many different areas. It may be used as a device to assist specifications to model failure, or to describe complex interactions between non co-operating components. It is frequently used in hardware to allow complex scheduling patterns. Although interrupts are ubiquitous in usage, the precise behaviour of a system incorporating interrupts can be difficult to reason about and predict. In this paper, a complete theory of the interrupt operator presented by Hoare in his original treatment of CSP is proposed. The semantics are given in the CSP model in Unifying Theories of Programming. New and existing algebraic laws are proposed and justified. The contribution of the paper is therefore a denotational semantics of an interrupt operator, and a collection of algebraic laws that assist in reasoning about systems incorporating interrupts.

Alistair A. McEwan, Jim Woodcock

UTP Semantics for Handel-C

Abstract

Only limited progress has been made so far towards an axiomatic semantics or discovering the algebraic rules that characterise Handel-C programs. In this paper we present a UTP semantics together with extensions we needed to include in order to express Handel-C properties that were not addressable with standard UTP. We also show how our extensions can be abstracted to a more general context and prove a set of algebraic rules that hold for them. Finally, we use the semantics to prove some properties about Handel-C constructs.

Juan Ignacio Perna, Jim Woodcock

Unifying Theories of Locations

Abstract

We present a Unifying Theories of Programming (UTP) model of locations, where a location is either shareable or containable depending on whether its value can be dereferenced by a pointer. Our model of locations is similar to previous work on pointers within the UTP; the main difference is that the previous work on pointers only modelled shareable locations. We explain why containable locations (whose values must be copied rather than aliased) are useful, present an outline of our UTP model, and compare it to existing work on UTP. We hope to convince the reader that a general model of pointers within the UTP ought to be able to represent both shareable and containable locations.

Michael Anthony Smith, Jeremy Gibbons

Unifying Input Output Conformance

Abstract

Model-based conformance testing aims to assess the correctness of an implementation with respect to a specification. This raises the question of a proper conformance relation that should be established between implementations and specifications. One commonly used conformance relation is the so-called input output conformance (ioco), which is defined over labeled transition systems. In this paper we investigate a denotational semantics of the input output conformance relation over reactive processes. We formalize the underlying assumptions of the ioco relation in terms of formal healthiness conditions and by adopted choice operators. Finally, we show that our denotational version of ioco can be generalized in the same way as the original relation. Our work aims to provide a unification of input output conformance by lifting the definition from labeled transition systems to reactive processes.

Martin Weiglhofer, Bernhard K. Aichernig

The Miracle of Reactive Programming

Abstract

Reactive miracles are rather unexplored in Unifying Theories of Programming. We present two simple properties: prefixing a miracle with an event, and offering an external choice between a process and a miracle. Both are strange processes, each violating an important axiom of the standard failures-divergences model for CSP.

Jim Woodcock

Encoding Circus Programs in ProofPowerZ

Abstract

Circus combines elements from sequential and reactive programming, and is especially suited for the development and verification of state-rich, reactive systems. In this paper we illustrate, by example, how a mechanisation of the UTP, and of a Circus theory, more specifically, can be used to encode particular Circus specifications. This complements previous work which focused on using the mechanised UTP semantics to prove general laws. We propose a number of extensions to an existing mechanisation by Oliveira to deal with the problems of type constraints and theory instantiation. We also show what the strategies and practical solutions are for proving refinement conjectures.

Frank Zeyda, Ana Cavalcanti

Component Publications and Compositions

Abstract

One of the major issues in component-based design is how to use a component correctly in different applications according to the given interface specification, called the publication, of the component. In this paper we formulate this as the problem of component publication composition and refinement. We define the notion of publications of components that describes how a component can be used by a third party in building their own components or in writing their applications without access to the design or the code of the component. It is desirable that different users of the components can be given different publications according to their need. The first contribution of this paper is to provide a procedure, which calculates a weakest contract of the required interface of a component from the contract of its provided interface and its code. The other contribution, that is more significant from a component-based designer’s point of view, is to define composition on publications so that the publication of a composite component can be calculated from those of its subcomponents. For this we define a set of primitive composition operators over components, including renaming, hiding, internalizing, plugging and feedback. This theory is presented based on the sematic model of rCOS, a refinement calculus of component and object systems.

Naijun Zhan, Eun Young Kang, Zhiming Liu

Denotational Approach to an Event-Driven System-Level Language

Abstract

As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It is challenging to formalise SystemC. In this paper, we study the denotational semantics for SystemC using Unifying Theories of Programming (abbreviated as UTP) [6]. Two trace variables are introduced, one is to record the state behaviours and another is to record the event behaviours. The timed model is formalised in a three-dimensional structure. A set of algebraic laws is explored, which can be proved via the achieved denotational semantics.

Huibiao Zhu, Jifeng He, Xiaoqing Peng, Naiyong Jin

Backmatter

Titel: Unifying Theories of Programming
herausgegeben von: Andrew Butterfield
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-14521-6
Print ISBN: 978-3-642-14520-9
DOI: https://doi.org/10.1007/978-3-642-14521-6