Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B

Héctor Ruíz Barradas, Lilian Burdy, David Déharbe
Digital Printed Abstract View Cite
Type
Short Paper
Publication
7th International Conference on Rigorous State Based Methods (ABZ'20)

Abstract

Proof obligations of the B method and of Event B use predicates in the Constraints, Sets, Properties and Invariant clauses as hypotheses in proof obligations. A contradiction in these predicates results in trivially valid proof obligations and essentially voids the development. A textbook on the B method [3] presents three “existence proof obligations” to show the satisfiability of the Constraints, Properties and Invariant clauses as soon as they are stated in a component. Together with new existence proof obligations for refinement, this prevents the introduction of such contradictions in the refinement chain. This paper presents a detailed formalization of these existence proof obligations, specifying their implementation in Atelier B.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{BarradasBD20,
  author       = {H{\'{e}}ctor Ru{\'{\i}}z Barradas and
                  Lilian Burdy and
                  David D{\'{e}}harbe},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry and
                  Frank Houdek},
  title        = {Existence Proof Obligations for Constraints, Properties and Invariants
                  in Atelier {B}},
  booktitle    = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
                  2020, Ulm, Germany, May 27-29, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12071},
  pages        = {255--259},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-48077-6\_20},
  doi          = {10.1007/978-3-030-48077-6\_20},
  timestamp    = {Mon, 25 May 2020 12:33:39 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BarradasBD20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'20

Related