Abstract
Using only a simple transition relation one cannot model commands that may or may not terminate in a given state. In a more general approach commands are relations enriched with termination vectors. We reconstruct this model in modal Kleene algebra. This links the recursive definition of the do od loop with a combination of the Kleene star and a convergence operator. Moreover, the standard wp operator coincides with the wlp operator in the modal Kleene algebra of commands. Therefore our earlier general soundness and relative completeness proof for Hoare logic in modal Kleene algebra can be re-used for wp. Although the definition of the loop semantics is motivated via the standard Egli-Milner ordering, the actual construction does not depend on Egli-Milner-isotony of the constructs involved.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Apt, K.-R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 2nd edn. Springer, Heidelberg (1997)
Backhouse, R.C., van der Woude, J.: Demonic operators and monotype factors. Mathematical Structures in Computer Science 3(4), 417–433 (1993)
Berghammer, R., Zierer, H.: Relational algebraic semantics of deterministic and non-deterministic programs. Theoretical Computer Science 43, 123–147 (1986)
Broy, M., Gnatz, R., Wirsing, M.: Semantics of nondeterministic and non-continuous constructs. In: Gerhart, S.L., Pair, C., Pepper, P.A., Wössner, H., Dijkstra, E.W., Guttag, J.V., Owicki, S.S., Partsch, H., Bauer, F.L., Gries, D., Griffiths, M., Horning, J.J., Wirsing, M. (eds.) Program Construction. LNCS, vol. 69, pp. 553–592. Springer, Heidelberg (1979)
Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)
Conway, J.H.: Regular algebra and finite machines. Chapman and Hall, London (1971)
Desharnais, J., Belkhiter, N., Sghaier, S.B.M., Tchier, F., Jaoua, A., Mili, A., Zaguia, N.: Embedding a demonic semilattice in a relation algebra. Theoretical Computer Science 149, 333–360 (1995)
Desharnais, J., Mili, A., Nguyen, T.T.: Refinement and demonic semantics. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational methods in computer science, ch. 11, pp. 166–183. Springer, Heidelberg (1997)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic (to appear)
Desharnais, J., Möller, B., Struth, G.: Termination in modal Kleene algebra. In: Lévy, J.-J., Mayr, E., Mitchell, J. (eds.) Exploring new frontiers of theoretical informatics. IFIP International Federation for Information Processing Series, vol. 155, pp. 653–666. Kluwer, Dordrecht (2004)
Desharnais, J., Möller, B., Tchier, F.: Kleene under a modal demonic star. Journal on Logic and Algebraic Programming, Special Issue on Relation Algebra and Kleene Algebra (to appear, 2005)
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, Amsterdam (1994)
Ehm, T.: The Kleene algebra of nested pointer structures: theory and applications. Universität Augsburg, Ph.D Thesis (December 2003)
Guttmann, W., Möller, B.: Modal design algebra. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010. Springer, Heidelberg (2006); Preliminary version: Institut für Informatik, Universität Augsburg, Report 2005-15
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Hoare, C.A.R., He, J.: Unifying theories of programming. Prentice Hall, Englewood Cliffs (1998)
Kozen, D.: Kleene algebras with tests. ACM TOPLAS 19, 427–443 (1997)
Möller, B.: Towards pointer algebra. Science of Computer Programming 21, 57–90 (1993)
Möller, B.: Lazy Kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004)
Möller, B., Struth, G.: Modal Kleene algebra and partial correctness. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 379–393. Springer, Heidelberg (2004)
Möller, B., Struth, G.: WP is WLP. Institut für Informatik, Universität Augsburg, Report 2004-14 (2004)
Nelson, G.: A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems 11, 517–561 (1989)
Nguyen, T.T.: A relational model of nondeterministic programs. International J. Foundations Comp. Sci. 2, 101–131 (1991)
Parnas, D.: A generalized control structure and its formal definition. Commun. ACM 26, 572–581 (1983)
Spivey, J.M.: Understanding Z. Cambridge University Press, Cambridge (1988)
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
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Möller, B., Struth, G. (2006). wp Is wlp. In: MacCaull, W., Winter, M., Düntsch, I. (eds) Relational Methods in Computer Science. RelMiCS 2005. Lecture Notes in Computer Science, vol 3929. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11734673_16
Download citation
DOI: https://doi.org/10.1007/11734673_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33339-5
Online ISBN: 978-3-540-33340-1
eBook Packages: Computer ScienceComputer Science (R0)