Mechanical inference of invariants for FOR-loops. (English) Zbl 1208.68147
Summary: In the mechanical verification of programs containing loops it is often necessary to provide loop invariants additionally to the specification in the form of pre and postconditions. In this paper we present a method for the mechanical inference of invariants for a practically relevant class of FOR-loops. The invariant is derived from the specification (pre, post) and the final bound of the loop only. The method is based on the technique “replacing a constant in post by a variable”, which has traditionally been used manually for the development of WHILE-loops. Our method is a complete mechanization of this heuristic for the verification of existing annotated FOR-loops. The range of applicability of the method is further extended by a technique called “bound transformation” and by taking common invariant conjuncts of pre and post into account. As a result, the method is applicable to the majority of FOR-loops occurring in practice.
The incorporation of this method into an automatic program verifier would make the task of the SW engineer easier, because he has only to provide a pre-post-specification for a FOR-loop.
The incorporation of this method into an automatic program verifier would make the task of the SW engineer easier, because he has only to provide a pre-post-specification for a FOR-loop.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Ahrendt, W.; Baar, T.; Beckert, B., The key tool, Software Syst. Model, 4, 32-54 (2005) |
| [2] | Back, R.-J., Invariant based programming, (LNCS, vol. 4024 (2006), Springer: Springer Berlin), 1-18 |
| [4] | Barnes, J., High Integrity Ada-The SPARK Approach- (2000), Addison-Wesley: Addison-Wesley Harlow, etc. · Zbl 0884.68017 |
| [5] | Barnett, M.; Chang, B.-Y. E.; DeLine, R., Boogie: A modular reusable verifier for object-oriented programs, (LNCS, vol. 4111 (2006), Springer: Springer Berlin), 364-387 |
| [6] | Basu, S. K., A note on synthesis of inductive assertions, IEEE TSE, 6, 1, 32-39 (1980) · Zbl 0431.68014 |
| [7] | Caplain, M., Finding invariant assertions for proving programs, SIGPLAN Not., 10, 6, 165-171 (1975) |
| [8] | Collins, W. J., The trouble with FOR-loop invariants, ACM SIGCSE Bull., 20, 1, 1-4 (1988) |
| [9] | Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall Inc: Prentice-Hall Inc Englewood Cliffs · Zbl 0286.00013 |
| [10] | Dijkstra, E. W.; Scholten, C. S., Predicate Calculus and Program Semantics (1990), Springer: Springer New York, etc. · Zbl 0698.68011 |
| [11] | Dunlop, D. D.; Basili, V. R., A heuristic for deriving loop functions, IEEE TSE, 10, 3, 275-285 (1984) · Zbl 0536.68003 |
| [12] | Ellozy, H. A., The determination of loop invariants for programs with arrays, IEEE TSE, 7, 2, 197-206 (1981) · Zbl 0463.68016 |
| [13] | Engeln-Müllges, G.; Reutter, F., (Numerik-Algorithmen mit FORTRAN 77-Programmen. (Numerical Algorithms with Fortran 77 Programs). Numerik-Algorithmen mit FORTRAN 77-Programmen. (Numerical Algorithms with Fortran 77 Programs), Aufl., vol. 7 (1993), BI Wissenschaftsverlag: BI Wissenschaftsverlag Mannheim usw), English edition 1996, ISBN 3-540-60529-0 · Zbl 0787.65001 |
| [17] | Floyd, R. W., Assigning meaning to programs, (Schwartz, J. T., Mathematical Aspects of Computer Science (1967), AMS), 19-32 · Zbl 0189.50204 |
| [18] | Freining, C.; Kauer, S.; Winkler, J. F.H., Ein Vergleich der Programmbeweiser FPP, NPPV und SPARK. (A Comparison of the Program Provers FPP, NPPV and SPARK), (Ada-Deutschland Tagung 2002 (2002), Shaker Verlag: Shaker Verlag Aachen), 127-145 |
| [20] | Golub, G. H.; Loan, C. F.van, Matrix Computations (1990), John Hopkins Univ. Press: John Hopkins Univ. Press Baltimore, etc., second pr |
| [21] | Gonnet, G. H.; Baeza-Yates, R., Handbook of Algorithms and Data Structures (1991), Addison Wesley: Addison Wesley Wokingham · Zbl 0719.68001 |
| [22] | Gries, D., A Note on a Standard Strategy for Developing Loop Invariants and Loops, Sci. Comput. Program., 2, 207-214 (1982) · Zbl 0516.68008 |
| [23] | Gries, D., The Science of Programming (1983), Springer: Springer New York, Second pr |
| [24] | Gumm, H., Generating algebraic laws from imperative programs, Theoret. Comput. Sci., 217, 385-405 (1999) · Zbl 0914.68132 |
| [26] | Hoare, C. A.R., An axiomatic basis of computer programming, CACM, 12, 10, 576-580 (1969), 583 · Zbl 0179.23105 |
| [27] | Hoare, C. A.R., A note on the FOR statement, BIT, 12, 334-341 (1972) · Zbl 0246.68003 |
| [30] | Katz, S.; Manna, Z., Logical analysis of programs, CACM, 19, 4, 188-206 (1976) · Zbl 0353.68016 |
| [40] | Mili, A.; Desharnais, J.; Gagné, J.-R., Strongest invariant functions: Their use in the systematic analysis of while-statements, Acta Inform., 22, 1, 47-66 (1985) · Zbl 0546.68011 |
| [41] | Misra, J., Some aspects of the verification of loop computations, IEEE TSE, 4, 6, 478-486 (1978) · Zbl 0392.68011 |
| [42] | Morris, J. H.; Wegbreit, B., Subgoal induction, CACM, 20, 4, 209-222 (1977) · Zbl 0349.68007 |
| [44] | Paige, R., Programming with invariants, IEEE Software, 3, 1, 56-69 (1986) |
| [45] | Rodríguez-Carbonell, E.; Kapur, D., Automatic generation of polynomial invariants of bounded degree using abstract interpretation, Sci. Comput. Program., 64, 1, 54-75 (2006), Available online 28 Sept 2006 at www.sciencedirect.com/, visited 2007. Jan. 22 · Zbl 1171.68555 |
| [48] | Tamir, M., ADI: Automatic derivation of invariants, IEEE TSE, 6, 1, 40-48 (1980) · Zbl 0431.68015 |
| [49] | Turing, A., Checking a large routine, (Williams, L. R.; Campbell-Kelly, M., The Early British Computer Conferences (1949), MIT Press: MIT Press Cambridge), 70-72, 1989 |
| [50] | Wegbreit, B., The synthesis of loop predicates, CACM, 17, 2, 102-112 (1974) · Zbl 0273.68014 |
| [51] | Winkler, J. F.H., (The Frege Program Prover. 42. The Frege Program Prover. 42, Int. Wiss. Koll., Ilmenau., vol. 1 (1997)), 116-121 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
