Advertisement

Algebra of Monotonic Boolean Transformers

  • Viorel Preoteasa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)

Abstract

Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We introduce here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of our algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).

Keywords

Boolean Algebra Sequential Composition Dual Operator Total Correctness Monotonic Transformer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Back, R.-J.: On the correctness of refinement in program development. PhD thesis, Department of Computer Science, University of Helsinki (1978)Google Scholar
  2. 2.
    Back, R.-J.: Correctness preserving program refinements: proof theory and applications. Mathematical Centre Tracts, vol. 131. Mathematisch Centrum, Amsterdam (1980)zbMATHGoogle Scholar
  3. 3.
    Back, R.-J., Preoteasa, V.: An algebraic treatment of procedure refinement to support mechanical verification. Formal Aspects of Computing 17, 69–90 (2005)CrossRefzbMATHGoogle Scholar
  4. 4.
    Back, R.-J., von Wright, J.: A lattice-theoretical basis for a specification language. In: van de Snepscheut, J.L.A. (ed.) MPC 1989. LNCS, vol. 375, pp. 139–156. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  5. 5.
    Back, R.-J., von Wright, J.: Duality in specification languages: a lattice-theoretical approach. Acta Inf. 27, 583–625 (1990)CrossRefzbMATHGoogle Scholar
  6. 6.
    Back, R.-J., von Wright, J.: Refinement Calculus. A systematic Introduction. Springer, Heidelberg (1998)CrossRefzbMATHGoogle Scholar
  7. 7.
    Dang, H.-H., Höfner, P., Möller, B.: Algebraic separation logic. Journal of Logic and Algebraic Programming 80(6), 221–247 (2011); Relations and Kleene Algebras in Computer ScienceCrossRefzbMATHGoogle Scholar
  8. 8.
    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Logic 7, 798–833 (2006)CrossRefGoogle Scholar
  9. 9.
    Guerreiro, P.: Another characterization of weakest preconditions. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 164–177. Springer, Heidelberg (1982), doi:10.1007/3-540-11494-7_12CrossRefGoogle Scholar
  10. 10.
    Hoare, C.A., Möller, B., Struth, G., Wehrman, I.: Concurrent kleene algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399–414. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)CrossRefzbMATHGoogle Scholar
  12. 12.
    Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19, 427–443 (1997)CrossRefzbMATHGoogle Scholar
  13. 13.
    Martin, C.E., Curtis, S.A., Rewitzky, I.: Modelling angelic and demonic nondeterminism with multirelations. Science of Computer Programming 65(2), 140–158 (2007); Special Issue dedicated to selected papers from the conference of program construction 2004 (MPC 2004)CrossRefzbMATHGoogle Scholar
  14. 14.
    Meinicke, L., Solin, K.: Refinement algebra for probabilistic programs. Formal Aspects of Computing 22, 3–31 (2010), doi:10.1007/s00165-009-0111-1CrossRefzbMATHGoogle Scholar
  15. 15.
    Morgan, C.: Programming from specifications. Prentice-Hall, Inc., Englewood Cliffs (1990)zbMATHGoogle Scholar
  16. 16.
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  17. 17.
    Preoteasa, V.: Program Variables – The Core of Mechanical Reasoning about Imperative Programs. PhD thesis, Turku Centre for Computer Science (November 2006)Google Scholar
  18. 18.
    Preoteasa, V.: Frame rule for mutually recursive procedures manipulating pointers. Theoretical Computer Science 410(42), 4216–4233 (2009)CrossRefzbMATHGoogle Scholar
  19. 19.
    Preoteasa, V., Back, R.-J.: Data refinement of invariant based programs. Electronic Notes in Theoretical Computer Science 259, 143–163 (2009); Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009)CrossRefzbMATHGoogle Scholar
  20. 20.
    Solin, K., von Wright, J.: Enabledness and termination in refinement algebra. Sci. Comput. Program. 74, 654–668 (2009)CrossRefzbMATHGoogle Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    von Wright, J.: Towards a refinement algebra. Sci. Comput. Program. 51, 23–45 (2004)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Viorel Preoteasa
    • 1
  1. 1.Department of Information TechnologiesÅbo Akademi UniversityTurkuFinland

Personalised recommendations

Cite paper

Buy options