Encoding Circus programs in ProofPower-Z

Frank Zeyda; Ana Cavalcanti

doi:10.1007/978-3-642-14521-6_13

Encoding Circus programs in ProofPower-Z

Frank Zeyda^*, Ana Cavalcanti

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	Unifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers
Pages	218-237
Number of pages	20
DOIs	https://doi.org/10.1007/978-3-642-14521-6_13
Publication status	Published - 26 Aug 2010
Event	2nd International Symposium on Unifying Theories of Programming, UTP 2008 - Dublin, Ireland Duration: 8 Sep 2008 → 10 Sep 2008

Publication series

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

Conference

Conference	2nd International Symposium on Unifying Theories of Programming, UTP 2008
Country/Territory	Ireland
City	Dublin
Period	8/09/08 → 10/09/08

Keywords

refinement
semantics
theorem proving
UTP
Z

Access to Document

10.1007/978-3-642-14521-6_13

Cite this

Zeyda, F., & Cavalcanti, A. (2010). Encoding Circus programs in ProofPower-Z. In Unifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers (pp. 218-237). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5713 LNCS). https://doi.org/10.1007/978-3-642-14521-6_13

@inproceedings{a29e5557135f41f0ab544ea86c9985d4,

title = "Encoding Circus programs in ProofPower-Z",

abstract = "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.",

keywords = "refinement, semantics, theorem proving, UTP, Z",

author = "Frank Zeyda and Ana Cavalcanti",

year = "2010",

month = aug,

day = "26",

doi = "10.1007/978-3-642-14521-6_13",

language = "English",

isbn = "3642145205",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "218--237",

booktitle = "Unifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers",

note = "2nd International Symposium on Unifying Theories of Programming, UTP 2008 ; Conference date: 08-09-2008 Through 10-09-2008",

}

Zeyda, F & Cavalcanti, A 2010, Encoding Circus programs in ProofPower-Z. in Unifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5713 LNCS, pp. 218-237, 2nd International Symposium on Unifying Theories of Programming, UTP 2008, Dublin, Ireland, 8/09/08. https://doi.org/10.1007/978-3-642-14521-6_13

Encoding Circus programs in ProofPower-Z. / Zeyda, Frank ; Cavalcanti, Ana.

Unifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers. 2010. p. 218-237 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5713 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Encoding Circus programs in ProofPower-Z

AU - Zeyda, Frank

AU - Cavalcanti, Ana

PY - 2010/8/26

Y1 - 2010/8/26

N2 - 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.

AB - 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.

KW - refinement

KW - semantics

KW - theorem proving

KW - UTP

KW - Z

UR - http://www.scopus.com/inward/record.url?scp=77955792316&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-14521-6_13

DO - 10.1007/978-3-642-14521-6_13

M3 - Conference contribution

AN - SCOPUS:77955792316

SN - 3642145205

SN - 9783642145209

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 218

EP - 237

BT - Unifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers

T2 - 2nd International Symposium on Unifying Theories of Programming, UTP 2008

Y2 - 8 September 2008 through 10 September 2008

ER -

Encoding Circus programs in ProofPower-Z

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Cite this