Generation of correctness conditions for imperative programs
| Autor: | E. V. Bodin, Nikolay V. Shilov, Igor S. Anureev |
|---|---|
| Rok vydání: | 2008 |
| Předmět: |
Loop invariant
Correctness Theoretical computer science Computer science Programming language Algorithm complexity computer.software_genre Nondeterministic algorithm Program analysis TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Programming Languages A priori and a posteriori Control (linguistics) computer Software |
| Zdroj: | Programming and Computer Software. 34:307-321 |
| ISSN: | 1608-3261 0361-7688 |
| DOI: | 10.1134/s0361768808060029 |
| Popis: | Verification of imperative programs in the sense of Floyd-Hoare is an approach to proving correctness of programs annotated by preconditions, postconditions, and loop invariants. It is based on generation of correctness conditions. In the structured deterministic case, the problem of generation of correctness conditions seems trivial, since it is solved by a syntax-driven algorithm, the complexity of which linearly depends on the number of control constructs. Vice versa, in the unstructured nondeterministic case, it seems a priori clear that the complexity of generation of the correctness conditions exponentially depends on the number of statements in the program. In the paper, an efficient and complete algorithm for the generation of the correctness conditions is presented and justified. It can be used both in the structured deterministic and unstructured nondeterministic cases. The algorithm complexity linearly depends on the number of control constructs and/or program statements. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink