The correctness of event-B inductive convergence.
Saved in:
| Title: | The correctness of event-B inductive convergence. |
|---|---|
| Authors: | Hallerstede, Stefan1 stefan.hallerstede@wanadoo.fr |
| Source: | Science of Computer Programming. Dec2016, Vol. 131, p94-108. 15p. |
| Subjects: | Computer software correctness, B method (Computer science), Computer programming, Proof theory, Stochastic convergence, Mathematical induction |
| Abstract: | Anticipation proof obligations for stated variants need to be proved in Event-B even if the variant has no variable in common with an anticipated event. This often leads to models that are complicated by additional auxiliary variables and variants that need to take into account these variables. Because of such “encodings” of control flow information in the variants the corresponding proof obligations can usually not be discharged automatically. We present a new proof obligation for anticipated events that does not have this defect and prove it correct. The proof is fairly intricate due to the nondeterminism of the simulations that link refinements. An informal soundness argument suggests using a lexicographic product in the soundness proof. However, it turns out that a weaker order is required which we call quasi-lexicographic product. [ABSTRACT FROM AUTHOR] |
| Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 118898534 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: The correctness of event-B inductive convergence. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Hallerstede%2C+Stefan%22">Hallerstede, Stefan</searchLink><relatesTo>1</relatesTo><i> stefan.hallerstede@wanadoo.fr</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Science+of+Computer+Programming%22">Science of Computer Programming</searchLink>. Dec2016, Vol. 131, p94-108. 15p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Computer+software+correctness%22">Computer software correctness</searchLink><br /><searchLink fieldCode="DE" term="%22B+method+%28Computer+science%29%22">B method (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+programming%22">Computer programming</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink><br /><searchLink fieldCode="DE" term="%22Stochastic+convergence%22">Stochastic convergence</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+induction%22">Mathematical induction</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: Anticipation proof obligations for stated variants need to be proved in Event-B even if the variant has no variable in common with an anticipated event. This often leads to models that are complicated by additional auxiliary variables and variants that need to take into account these variables. Because of such “encodings” of control flow information in the variants the corresponding proof obligations can usually not be discharged automatically. We present a new proof obligation for anticipated events that does not have this defect and prove it correct. The proof is fairly intricate due to the nondeterminism of the simulations that link refinements. An informal soundness argument suggests using a lexicographic product in the soundness proof. However, it turns out that a weaker order is required which we call quasi-lexicographic product. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=118898534 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1016/j.scico.2016.04.012 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 15 StartPage: 94 Subjects: – SubjectFull: Computer software correctness Type: general – SubjectFull: B method (Computer science) Type: general – SubjectFull: Computer programming Type: general – SubjectFull: Proof theory Type: general – SubjectFull: Stochastic convergence Type: general – SubjectFull: Mathematical induction Type: general Titles: – TitleFull: The correctness of event-B inductive convergence. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Hallerstede, Stefan IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 12 Text: Dec2016 Type: published Y: 2016 Identifiers: – Type: issn-print Value: 01676423 Numbering: – Type: volume Value: 131 Titles: – TitleFull: Science of Computer Programming Type: main |
| ResultId | 1 |
