Abstract
We give axioms for an operation that describes iteration in various relational models of computations. The models differ in their treatment of finite, infinite and aborting executions, covering partial, total and general correctness and extensions thereof. Based on the common axioms we derive separation, refinement and program transformation results hitherto known from particular models, henceforth recognised to hold in many different models. We introduce a new model that independently describes the finite, infinite and aborting executions of a computation, and axiomatise an operation that extracts the infinite executions in this model and others. From these unifying axioms we derive explicit representations for recursion and iteration. We show that also the new model is an instance of our general theory of iteration. All results are verified in Isabelle heavily using automated theorem provers.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Aarts C.J., Backhouse R.C., Boiten E.A., Doornbos H., van Gasteren N., van Geldrop R., Hoogendijk P.F., Voermans E., van der Woude J.: Fixed-point calculus. Inf. Process. Lett. 53(3), 131–136 (1995)
Apt K.R., de Boer F.S., Olderog E.-R.: Verification of Sequential and Concurrent Programs. 3rd edn. Springer, London (2009)
Back R.J.R., von Wright J.: Reasoning algebraically about loops. Acta Informatica 36(4), 295–334 (1999)
Berghammer R., Zierer H.: Relational algebraic semantics of deterministic and nondeterministic programs. Theor. Comput. Sci. 43, 123–147 (1986)
Birkhoff G.: Lattice Theory, volume XXV of Colloquium Publications. 3rd edn. American Mathematical Society, Providence, RI (1967)
Blanchette J.C., Böhme S., Paulson L.C.: Extending Sledgehammer with SMT solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction: CADE-23, volume 6803 of Lecture Notes in Computer Science, pp. 116–130. Springer, Berlin (2011)
Blanchette J.C., Nipkow T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pp. 131–146. Springer, Berlin (2010)
Bloom S.L., Ésik Z.: Iteration Theories: The Equational Logic of Iterative Processes. Springer, Berlin (1993)
Broy M., Gnatz R., Wirsing M.: Semantics of nondeterministic and noncontinuous constructs. In: Bauer, F.L., Broy, M. (eds.) Program Construction, volume 69 of Lecture Notes in Computer Science, pp. 553–592. Springer, Berlin (1979)
Cohen E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pp. 45–59. Springer, Berlin (2000)
Conway J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)
de Bakker J.W.: Semantics and termination of nondeterministic recursive programs. In: Michaelson, S., Milner, R. (eds.) Automata, Languages and Programming: Third International Colloquium, pp. 435–477. Edinburgh University Press, Edinburgh (1976)
De Carufel J.-L., Desharnais J.: Demonic algebra with domain. In: Schmidt, R. (ed) Relations and Kleene Algebra in Computer Science, volume 4136 of Lecture Notes in Computer Science, pp. 120–134. Springer, Berlin (2006)
Desharnais J., Möller B., Struth G.: Kleene algebra with domain. ACM Trans. Comput. Log. 7(4), 798–833 (2006)
Desharnais J., Möller B., Struth G.: Algebraic notions of termination. Log. Methods Comput. Sci. 7(1:1), 1–29 (2011)
Desharnais J., Möller B., Tchier F.: Kleene under a modal demonic star. J. Log. Algebr. Program. 66(2), 127–160 (2006)
Desharnais J., Struth G.: Internal axioms for domain semirings. Sci. Comput. Program. 76(3), 181–203 (2011)
Doornbos H.: A relational model of programs without the restriction to Egli-Milner-monotone constructs. In: Olderog, E.-R. (ed.) Programming Concepts, Methods and Calculi, pp. 363–382. North-Holland Publishing Company, Amsterdam (1994)
Dunne, S.: Recasting Hoare and He’s unifying theory of programs in the context of general correctness. In: Butterfield, A., Strong, G., Pahl, C. (eds.) 5th Irish Workshop on Formal Methods, Electronic Workshops in Computing. The British Computer Society (2001)
Guttmann W.: General correctness algebra. In: Berghammer, R., Jaoua, A.M., Möller, B. (eds.) Relations and Kleene Algebra in Computer Science, volume 5827 of Lecture Notes in Computer Science, pp. 150–165. Springer, Berlin (2009)
Guttmann W.: Partial, total and general correctness. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science, pp. 157–177. Springer, Berlin (2010)
Guttmann, W.: Unifying recursion in partial, total and general correctness. In: Qin, S. (eds.) Unifying Theories of Programming, Third International Symposium, UTP 2010, volume 6445 of Lecture Notes in Computer Science, pp. 207–225. Springer, Berlin (2010)
Guttmann W.: Fixpoints for general correctness. J. Log. Algebr. Program. 80(6), 248–265 (2011)
Guttmann W.: Towards a typed omega algebra. In: de Swart, H. (ed.) Relational and Algebraic Methods in Computer Science, volume 6663 of Lecture Notes in Computer Science, pp. 196–211. Springer, Berlin (2011)
Guttmann, W.: Extended designs algebraically. Sci. Comput. Program. (2012) (to appear)
Guttmann W.: Unifying correctness statements. In: Gibbons, J., Nogueira, P. (eds.) Mathematics of Program Construction, volume 7342 of Lecture Notes in Computer Science, pp. 198–219. Springer, Berlin (2012)
Guttmann, W.: Unifying lazy and strict computations. In: Griffin, T.G., Kahl, W. (eds.) Relational and Algebraic Methods in Computer Science, Lecture Notes in Computer Science. Springer, Berlin (2012) (to appear)
Guttmann W., Möller B.: Modal design algebra. In: Dunne, S., Stoddart, W. (eds.) Unifying Theories of Programming, volume 4010 of Lecture Notes in Computer Science, pp. 236–256. Springer, Berlin (2006)
Guttmann W., Möller B.: Normal design algebra. J. Log. Algebr. Program. 79(2), 144–173 (2010)
Guttmann W., Struth G., Weber T.: Automating algebraic methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering, volume 6991 of Lecture Notes in Computer Science, pp. 617–632. Springer, Berlin (2011)
Hayes I.J., Dunne S.E., Meinicke L.: Unifying theories of programming that distinguish nontermination and abort. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science, pp. 178–194. Springer, Berlin (2010)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall Europe (1998)
Höfner P., Möller B., Solin K.: Omega algebra, demonic refinement algebra and commands. In: Schmidt, R. (ed.) Relations and Kleene Algebra in Computer Science, volume 4136 of Lecture Notes in Computer Science, pp. 222–234. Springer, Berlin (2006)
Jacobs D., Gries D.: General correctness: a unification of partial and total correctness. Acta Informatica 22(1), 67–83 (1985)
Kozen D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366–390 (1994)
Kozen D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)
Kozen D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60–76 (2000)
McCune, W.: Mace4 reference manual and guide. Technical Memorandum ANL/MCS-TM-264, Mathematics and Computer Science Division, Argonne National Laboratory, (2003). Mace4 is available at http://www.cs.unm.edu/~mccune/mace4/
Möller B.: The linear algebra of UTP. In: Uustalu, T. (ed.) Mathematics of Program Construction, volume 4014 of Lecture Notes in Computer Science, pp. 338–358. Springer, Berlin (2006)
Möller B.: Kleene getting lazy. Sci. Comput. Program. 65(2), 195–214 (2007)
Möller B., Struth G.: Algebras of modal operators and partial correctness. Theor. Comput. Sci. 351(2), 221–239 (2006)
Möller B., Struth G.: WP is WLP. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) Relational Methods in Computer Science 2005, volume 3929 of Lecture Notes in Computer Science, pp. 200–211. Springer, Berlin (2006)
Nelson G.: A generalization of Dijkstra’s calculus. ACM Trans. Program. Lang. Syst. 11(4), 517–561 (1989)
Parnas D.: A generalized control structure and its formal definition. Commun. ACM 26(8), 572–581 (1983)
Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe G., Ternovska E., Schulz S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 3–13 (2010)
von Wright J.: Towards a refinement algebra. Sci. Comput. Program. 51(1–2), 23–45 (2004)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Guttmann, W. Algebras for iteration and infinite computations. Acta Informatica 49, 343–359 (2012). https://doi.org/10.1007/s00236-012-0162-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00236-012-0162-2