Abstract
A classical while-program normal-form theorem is derived in demonic refinement algebra. In contrast to Kozen’s partial-correctness proof of the theorem in Kleene algebra with tests, the derivation in demonic refinement algebra provides a proof that the theorem holds in total correctness.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Back, R.J.R., von Wright, J.: Refinement calculus: A systematic introduction. Springer, Heidelberg (1998)
Böhm, C., Jacopini, G.: Flow diagrams, Turing machines and languages with only two formation rules. Commun. ACM 9(5), 366–371 (1966)
Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Log. 7(4), 798–833 (2006)
Dijkstra, E.W.: A discipline of programming. Prentice-Hall International, Englewood Cliffs (1976)
Harel, D.: On folk theorems. Commun. ACM 23(7), 379–389 (1980)
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. Prog. Lang. Syst. 19(3), 427–443 (1997)
Mirkowska, G.: Algorithmic logic and its applications. PhD thesis. Univ. of Warsaw, Warsaw, Poland (1972) (in Polish)
von Wright, J.: From Kleene algebra to refinement algebra. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 233–262. Springer, Heidelberg (2002)
von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51, 23–45 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Solin, K. (2009). A While Program Normal Form Theorem in Total Correctness. In: Berghammer, R., Jaoua, A.M., Möller, B. (eds) Relations and Kleene Algebra in Computer Science. RelMiCS 2009. Lecture Notes in Computer Science, vol 5827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04639-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-04639-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04638-4
Online ISBN: 978-3-642-04639-1
eBook Packages: Computer ScienceComputer Science (R0)