By the same authors

From the same journal

From the same journal

A UTP semantics for Circus

Research output: Contribution to journalArticle



Publication details

JournalFormal Aspects of Computing
DatePublished - 1 Feb 2009
Issue number1-2
Number of pages30
Pages (from-to)3-32
Original languageEnglish


Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP constructs. Previously, a denotational semantics has been given to Circus; however, a shallow embedding of Circus in Z, in which the mapping from Circus constructs to their semantic representation as a Z specification, with yet another language being used as a meta-language, was not useful for proving properties like the refinement laws that justify the distinguishing development technique associated with Circus. This work presents a final reference for the Circus denotational semantics based on Hoare and He’s Unifying Theories of Programming (UTP); as such, it allows the proof of meta-theorems about Circus including the refinement laws in which we are interested. Its correspondence with the CSP semantics is illustrated with some examples. We also discuss the library of lemmas and theorems used in the proofs of the refinement laws. Finally, we give an account of the mechanisation of the Circus semantics and of the mechanical proofs of the refinement laws.

    Research areas

  • Relational model, Concurrency, Refinement calculus, Theorem proving, UNIFYING THEORIES, CSP


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations