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 条
12345