Encoding Circus programs in ProofPower-Z

Frank Zeyda*, Ana Cavalcanti

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Circus combines elements from sequential and reactive programming, and is especially suited for the development and verification of state-rich, reactive systems. In this paper we illustrate, by example, how a mechanisation of the UTP, and of a Circus theory, more specifically, can be used to encode particular Circus specifications. This complements previous work which focused on using the mechanised UTP semantics to prove general laws. We propose a number of extensions to an existing mechanisation by Oliveira to deal with the problems of type constraints and theory instantiation. We also show what the strategies and practical solutions are for proving refinement conjectures.

Original languageEnglish
Title of host publicationUnifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers
Number of pages20
Publication statusPublished - 26 Aug 2010
Event2nd International Symposium on Unifying Theories of Programming, UTP 2008 - Dublin, Ireland
Duration: 8 Sept 200810 Sept 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5713 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference2nd International Symposium on Unifying Theories of Programming, UTP 2008


  • refinement
  • semantics
  • theorem proving
  • UTP
  • Z

Cite this