Skip to main content

A Weakest Precondition Semantics for Circus

Cavalcanti, Ana L. C., Woodcock, Jim (2002) A Weakest Precondition Semantics for Circus. In: Proceedings of the Communicating Processing Architectures 2002. . IOS Press ISBN 4-274-90539-X. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:13677)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.

Abstract

Circus is a combination of Z and CSP; its chief distinguishing feature is the inclusion of the ideas of the refinement calculus. Our main objective is the definition of refinement methods for concurrent programs. The original semantic model for Circus is Hoare and He's unifying theories of programming. In this paper, we present an equivalent semantics based on predicate transformers. With this new model, we provide a more adequate basis for the formalisation of refinement and verification condition generating rules. Furthermore, this new framework makes it possible to include logical variables and angelic nondeterminism in Circus. The consistency of the relational and predicate transformer models gives us confidence in their accuracy.

Item Type: Conference or workshop item (Paper)
Additional information: To appear
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 17:59 UTC
Last Modified: 12 Jul 2022 10:39 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/13677 (The current URI for this page, for reference purposes)
  • Depositors only (login required):