Maximal and Compositional Pattern-Based Loop Invariants
| Autor: | Yannick Moy, Virginia Aponte, Pierre Courtieu, Marc Sango |
|---|---|
| Přispěvatelé: | CEDRIC, Laboratoire |
| Jazyk: | angličtina |
| Rok vydání: | 2012 |
| Předmět: |
Intermediate language
Pure mathematics Loop invariant Computer science loop invariant proof of programs Hoare logic invariant de boucle Static analysis [INFO] Computer Science [cs] preuve de programmes [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL] Logique de Hoare TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS sémantique Invariant (mathematics) Nested loop join Algorithm semantics |
| Zdroj: | FM 2012: Formal Methods ISBN: 9783642327582 FM |
| Popis: | We present a novel approach for the automatic generation of inductive loop invariants over non nested loops manipulating arrays. Unlike most existing approaches, it generates invariants containing disjunctions and quantifiers, which are rich enough for proving functional properties over programs which manipulate arrays. Our approach does not require the user to provide initial assertions or postconditions. It proceeds first, by translating body loops into an intermediate representation of parallel assignments, and second, by recognizing through static analysis code patterns that respect stability properties on accessed locations. We associate with each pattern a formula that we prove to be a so-called local invariant, and we give conditions for local invariants to compose an inductive invariant of the complete loop. We also give conditions over invariants to be locally maximal, and we show that some of our pattern invariants are indeed maximal. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|