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

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

Descripción completa

Detalles Bibliográficos
Autores principales: Ruíz Barradas, Héctor, Burdy, Lilian, Déharbe, David
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7242038/
http://dx.doi.org/10.1007/978-3-030-48077-6_20
_version_ 1783537167784476672
author Ruíz Barradas, Héctor
Burdy, Lilian
Déharbe, David
author_facet Ruíz Barradas, Héctor
Burdy, Lilian
Déharbe, David
author_sort Ruíz Barradas, Héctor
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7242038
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-72420382020-05-22 Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B Ruíz Barradas, Héctor Burdy, Lilian Déharbe, David Rigorous State-Based Methods Article 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. 2020-04-22 /pmc/articles/PMC7242038/ http://dx.doi.org/10.1007/978-3-030-48077-6_20 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Ruíz Barradas, Héctor
Burdy, Lilian
Déharbe, David
Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
title Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
title_full Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
title_fullStr Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
title_full_unstemmed Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
title_short Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
title_sort existence proof obligations for constraints, properties and invariants in atelier b
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7242038/
http://dx.doi.org/10.1007/978-3-030-48077-6_20
work_keys_str_mv AT ruizbarradashector existenceproofobligationsforconstraintspropertiesandinvariantsinatelierb
AT burdylilian existenceproofobligationsforconstraintspropertiesandinvariantsinatelierb
AT deharbedavid existenceproofobligationsforconstraintspropertiesandinvariantsinatelierb

Ejemplares similares