A Denotational Semantics for Circus

被引：16
作者：
Oliveira, Marcel [1 ]
Cavalcanti, Ana [2 ]
Woodcock, Jim [2 ]
机构：
[1] Univ Fed Rio Grande do Norte, Dept Informat & Matemat Aplicada, Natal, RN, Brazil
[2] Univ York, Dept Comp Sci, York, N Yorkshire, England
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2007年 / 187卷 / 107-123期
基金：
英国工程与自然科学研究理事会;
关键词：
Concurrency; refinement calculus; UTP; theorem proving;
D O I：
10.1016/j.entcs.2006.08.047
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：107 / 123
页数：17
相关论文
共 50 条
[31]   Separation Logic Semantics for Communicating Processes [J].
Hoare, Tony ;
O'Hearn, Peter .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 212 (0C) :3-25
[32]   A semantics of communicating reactive objects with timing [J].
Hooman J. ;
van der Zwaag M.B. .
International Journal on Software Tools for Technology Transfer, 2006, 8 (2) :97-112
[33]   A compositional Petri net semantics for SDL [J].
Fleischhack, H ;
Grahlmann, B .
APPLICATION AND THEORY OF PETRI NETS 1998, 1998, 1420 :144-164
[34]   WEAKEST PRECONDITION SEMANTICS FOR TIME AND CONCURRENCY [J].
SCHOLEFIELD, D ;
ZEDAN, HSM .
INFORMATION PROCESSING LETTERS, 1992, 43 (06) :301-308
[35]   UTP Semantics of Reactive Processes with Continuations [J].
Ngondi, Gerard Ekembe ;
Woodcock, Jim .
UNIFYING THEORIES OF PROGRAMMING, UTP 2016, 2017, 10134 :114-133
[36]   A GRAINLESS SEMANTICS FOR THE HARPO/L LANGUAGE [J].
Norvell, Theodore S. .
2009 IEEE 22ND CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1 AND 2, 2009, :742-746
[37]   PVS Verification of cCSP Synchronous Semantics [J].
Ripon, Shamim H. .
ENGINEERING LETTERS, 2010, 18 (03)
[38]   Semantics and logic Efor security protocols [J].
Jacobs, Bart ;
Hasuo, Ichiro .
JOURNAL OF COMPUTER SECURITY, 2009, 17 (06) :909-944
[39]   A Contextual Semantics for Concurrent Haskell with Futures [J].
Sabel, David ;
Schmidt-Schauss, Manfred .
PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING, 2011, :101-112
[40]   Concurrent Separation Logic and Operational Semantics [J].
Vafeiadis, Viktor .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 276 :335-351
12345