Paper Info
Title
A Denotational Semantics for Circus
Abstract
Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP. Previously, a denotational semantics has been given to Circus; however, as a shallow embedding of Circus in Z, it was not possible to use it to prove 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). Finally, it discusses the library of theorems on the UTP that was created and used in the proofs of the refinement laws.
Year
DOI
Venue
2007
10.1016/j.entcs.2006.08.047
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
distinguishing development technique,refinement law,circus denotational semantics,final reference,utp,theorem proving,circus specification,denotational semantics,refinement calculus,behavioural aspect,concurrency,theorem proving.,shallow embedding
Denotational semantics of the Actor model,Programming language,Embedding,Refinement calculus,Computer science,Concurrency,Denotational semantics,Automated theorem proving,Theoretical computer science,Mathematical proof
Journal
Volume
ISSN
Citations 
187,
Electronic Notes in Theoretical Computer Science
20
PageRank 
References 
Authors
0.94
6
3
Name
Order
Citations
PageRank
Marcel Oliveira117212.57
Ana Cavalcanti266859.95
Jim Woodcock324418.34