### Abstract

The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's Unifying Theories of Programming (UTP). Isabelle/Circus is a formalization of the UTP and the Circus language in Isabelle/HOL. It contains proof rules and tactic support that allows for proofs of refinement for Circus processes (involving both data and behavioral aspects).

The Isabelle/Circus environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus. This article contains an extended version of corresponding VSTTE Paper together with the complete formal development of its underlying commented theories.

### License

BSD License

### History

June 5, 2014
  More polishing, shorter proofs, added Circus syntax, added Makarius Wenzel as contributor.

### Topics

- Computer science/Concurrency/Process calculi
- Computer science/System description languages

### Session Circus

- Var
- Relations
- Designs
- Reactive_Processes
- CSP_Processes
- Circus_Actions
- Var_list
- Denotational_Semantics
- Circus_Syntax
- Refinement
- Refinement_Example

## Cite

×

Circus-AFP

    @article{Circus-AFP,
      author  = {Abderrahmane Feliachi and Burkhart Wolff and Marie-Claude Gaudel},
      title   = {Isabelle/Circus},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Circus.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 29, 2012 : Isabelle2012