Journal
FORMAL ASPECTS OF COMPUTING
Volume 21, Issue 1-2, Pages 3-32Publisher
SPRINGER
DOI: 10.1007/s00165-007-0052-5
Keywords
Relational model; Concurrency; Refinement calculus; Theorem proving
Categories
Funding
- Engineering and Physical Sciences Research Council [EP/E025366/1] Funding Source: researchfish
- EPSRC [EP/E025366/1] Funding Source: UKRI
Ask authors/readers for more resources
Circus specifications de. ne 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 Zspecification, 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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available