A Denotational Semantics for Circus

被引：17
作者：
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 条
[41]   Partial order semantics and read arcs [J].
Vogler, W .
THEORETICAL COMPUTER SCIENCE, 2002, 286 (01) :33-63
[42]   Concurrent Separation Logic and Operational Semantics [J].
Vafeiadis, Viktor .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 276 :335-351
[43]   A metric approach to control flow semantics [J].
DeBakker, JW ;
DeVink, EP .
PAPERS ON GENERAL TOPOLOGY AND APPLICATIONS: ELEVENTH SUMMER CONFERENCE AT THE UNIVERSITY OF SOUTHERN MAINE, 1996, 806 :11-27
[44]   A CSP model with flexible parallel termination semantics [J].
Howells, Paul ;
d'Inverno, Mark .
FORMAL ASPECTS OF COMPUTING, 2009, 21 (05) :421-449
[45]   Revisiting Concurrent Separation Logic and Operational Semantics [J].
Soares, Pedro ;
Ravara, Antonio ;
de Sousa, Simao Melo .
23RD EUROMICRO INTERNATIONAL CONFERENCE ON PARALLEL, DISTRIBUTED, AND NETWORK-BASED PROCESSING (PDP 2015), 2015, :484-491
[46]   Abstract interpretation of trace semantics for concurrent calculi [J].
Barbuti, R ;
De Francesco, N ;
Santone, A ;
Vaglini, G .
INFORMATION PROCESSING LETTERS, 1999, 70 (02) :69-78
[47]   Operational Semantics for the Rigorous Analysis of Distributed Systems [J].
Al-Mahfoudh, Mohammed S. ;
Gopalakrishnan, Ganesh ;
Stutsman, Ryan .
QUALITY SOFTWARE THROUGH REUSE AND INTEGRATION, 2018, 561 :209-231
[48]   Ready to preorder: The case of weak process semantics [J].
Chen, Taolue ;
Fokkink, Wan ;
van Glabbeek, Rob .
INFORMATION PROCESSING LETTERS, 2008, 109 (02) :104-111
[49]   Formal Semantics of Orc Based on TLA+ [J].
You, Zhen ;
Xue, Jinyun ;
Hu, Qimin ;
Hong, Yi .
STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, 2015, 8979 :147-163
[50]   INTERLEAVING SEMANTICS AND ACTION REFINEMENT WITH ATOMIC CHOICE [J].
CZAJA, I ;
VANGLABBEEK, RJ ;
GOLTZ, U .
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 609 :89-107
12345