Summary
Strongest invariant functions, a useful tool in the analysis of while statements, are defined and discussed. Their relationships to loop invariants and to the function computed by the while statement are investigated.
Similar content being viewed by others
References
Amy, B.: Calcul des Invariants Algorithmiques. In: Actes du Congrès Théories et Techniques de l'Informatique, pp.390–399. Gif-Sur-Yvette, France, 1978
Amy, B., Caplain, M.: Invariants Algorithmiques et Recurrences. Rapport de Recherche No 110. ENSIMAG, Université de Grenoble, 1978. Also available in: Proceedings, Third International Symposium on Programming, pp.218–231. Paris, 1978
Basu, S.K., Misra, J.: Proving Loop Programs. IEEE Trans. Software Eng. SE-1, 339–345 1975
Caplain, M.: Finding Invariant Assertions for Proving Programs. Proceedings, International Conference on Reliable Software, pp.165–171. Los Angeles, 1975
Dunlop, D.D., Basili, V.R.: A Comparative Analysis of Functional Correctness. ACM Comput. Surveys 14, 229–244 (1982)
Gries, D.: The Science of Programming. Berlin-Heidelberg-New York: Springer 1981
Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Commun. ACM 12, 576–583 (1969)
Manna, Z.: Mathematical Theory of Computation. New York: McGraw-Hill 1974
Mili, A.: The Bottom Up Analysis of While Statements: Strongest Invariant Functions. Proceedings, Ninth World Computer Congress (IFIP '83), pp.339–343. Paris, France, 1983
Mili, A.: Verifying Programs by Induction on their Data Structure: General Format and Applications. Inf. Process. Lett. 17, 155–160 (1983)
Mili, A.: A Relational Approach to the Design of Deterministic Programs. Acta Inf. 20, 315–328 (1983)
Mili, A., Desharnais, J., Gagné, J.-R.: Strongest Invariant Functions. Rapport de Recherche, DIUL-RR-8412. Département d'Informatique, Université Laval, Québec, PQ, G1K 7P4, 1984
Mills, H.D.: The New Math of Computer Programming. Commun. ACM 18, 43–48 (1975)
Mills, H., Basili, V.R., Gannon, J.D., Hamlet, R.G., Schneiderman, B., Austing, R.H., Kohl, J.E.: The Calculus of Computer Programming. Manuscript (1982) (To be published by Allyn & Bacon, Boston, MA)
Parnas, D.L.: A Generalized Control Structure and Its Formal Definition. Commun. ACM 26, 572–581 (1983)
Sanderson, J.G.: A Relational Theory of Computing. Lect. Notes Comput. Sci. Vol. 82. BerlinHeidelberg-New York: Springer 1980
Author information
Authors and Affiliations
Additional information
This research is partially supported by the National Science and Engineering Research Council of Canada under grant number A2509
Rights and permissions
About this article
Cite this article
Mili, A., Desharnais, J. & Gagné, J.R. Strongest invariant functions: Their use in the systematic analysis of while statements. Acta Informatica 22, 47–66 (1985). https://doi.org/10.1007/BF00290145
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00290145