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 条
  • [1] A UTP semantics for Circus
    Oliveira, Marcel
    Cavalcanti, Ana
    Woodcock, Jim
    FORMAL ASPECTS OF COMPUTING, 2009, 21 (1-2) : 3 - 32
  • [2] A Denotational Semantics for SPARC TSO
    Kavanagh, Ryan
    Brookes, Stephen
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2018, 336 (336) : 223 - 239
  • [3] A DENOTATIONAL SEMANTICS FOR SPARC TSO
    Kavanagh, Ryan
    Brookes, Stephen
    LOGICAL METHODS IN COMPUTER SCIENCE, 2019, 15 (02) : 10:1 - 10:23
  • [4] Denotational semantics of channel mobility in UTP-CSP
    Ngondi, Gerard Ekembe
    FORMAL ASPECTS OF COMPUTING, 2021, 33 (4-5) : 803 - 826
  • [5] Verification for ASP denotational semantics: A case study using the PVS theorem prover
    Aguado, F.
    Ascariz, P.
    Cabalar, P.
    Perez, G.
    Vidal, C.
    LOGIC JOURNAL OF THE IGPL, 2017, 25 (02) : 195 - 213
  • [6] ArcAngelC: a Refinement Tactic Language for Circus
    Oliveira, M. V. M.
    Cavalcanti, A. L. C.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 214 (0C) : 203 - 229
  • [7] Encoding Circus Programs in ProofPower-Z
    Zeyda, Frank
    Cavalcanti, Ana
    UNIFYING THEORIES OF PROGRAMMING, 2010, 5713 : 218 - 237
  • [8] A Denotational Approach to Release/Acquire Concurrency
    Dvir, Yotam
    Kammar, Ohad
    Lahav, Ori
    PROGRAMMING LANGUAGES AND SYSTEMS, PT II, ESOP 2024, 2024, 14577 : 121 - 149
  • [9] Prom Circus to JCSP
    Oliveira, M
    Cavalcanti, A
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2004, 3308 : 320 - 340
  • [10] Integrating Time and Resource into Circus
    Geguang Pu
    Qiu Zongyan
    He Jifeng
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 130 : 401 - 418
12345