Predicate transformers in the semantics of Circus

Author

Cavalcanti, A.L.C. ; Woodcock, J.C.P.

Author_Institution

Comput. Lab., Kent Univ., Canterbury, UK

Volume

150

Issue

2

fYear

2003

fDate

4/1/2003 12:00:00 AM

Firstpage

85

Lastpage

94

Abstract

Circus is a combination of Z and CSP; its chief distinguishing feature is the inclusion of the ideas of refinement calculus. The main objective is the definition of refinement methods for concurrent programs. The original semantic model for Circus is Hoare and He´s (1998) unifying theories of programming. An equivalent semantics based on predicate transformers is presented. With this model, a more adequate basis for the formalisation of refinement and verification-condition generation rules is provided. Furthermore, this framework makes it possible to include logical variables and angelic nondeterminism in Circus. The consistency of the relational and predicate transformer models gives us confidence in their accuracy.

Keywords

communicating sequential processes; computational linguistics; refinement calculus; specification languages; CSP; Circus; Z; angelic nondeterminism; communicating sequential processes; concurrent programs; logical variables; predicate transformers; refinement calculus; refinement methods; semantics; unifying theories; verification-condition generation rules;

fLanguage

English

Journal_Title

Software, IEE Proceedings -

Publisher

iet

ISSN

1462-5970

Type

jour

DOI

10.1049/ip-sen:20030131

Filename

1199820