Skip to main content
SpringerLink
Log in

Algebra of Monotonic Boolean Transformers

  • Conference paper
Formal Methods, Foundations and Applications (SBMF 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7021))

Included in the following conference series:

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).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. Back, R.-J.: Correctness preserving program refinements: proof theory and applications. Mathematical Centre Tracts, vol. 131. Mathematisch Centrum, Amsterdam (1980)

    MATH  Google Scholar 

  3. Back, R.-J., Preoteasa, V.: An algebraic treatment of procedure refinement to support mechanical verification. Formal Aspects of Computing 17, 69–90 (2005)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  5. Back, R.-J., von Wright, J.: Duality in specification languages: a lattice-theoretical approach. Acta Inf. 27, 583–625 (1990)

    Article  MATH  Google Scholar 

  6. Back, R.-J., von Wright, J.: Refinement Calculus. A systematic Introduction. Springer, Heidelberg (1998)

    Book  MATH  Google Scholar 

  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 Science

    Article  MATH  Google Scholar 

  8. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Logic 7, 798–833 (2006)

    Article  Google Scholar 

  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_12

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  11. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  12. Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst. 19, 427–443 (1997)

    Article  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  14. Meinicke, L., Solin, K.: Refinement algebra for probabilistic programs. Formal Aspects of Computing 22, 3–31 (2010), doi:10.1007/s00165-009-0111-1

    Article  MATH  Google Scholar 

  15. Morgan, C.: Programming from specifications. Prentice-Hall, Inc., Englewood Cliffs (1990)

    MATH  Google Scholar 

  16. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  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. Preoteasa, V.: Frame rule for mutually recursive procedures manipulating pointers. Theoretical Computer Science 410(42), 4216–4233 (2009)

    Article  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  20. Solin, K., von Wright, J.: Enabledness and termination in refinement algebra. Sci. Comput. Program. 74, 654–668 (2009)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  22. von Wright, J.: Towards a refinement algebra. Sci. Comput. Program. 51, 23–45 (2004)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5 A, 20520, Turku, Finland

    Viorel Preoteasa

Authors
  1. Viorel Preoteasa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Mathematics and Computer Science, University of São Paulo, Avenida Trabalhador, são carlense, 400, 13566-590, São Carlos, SP, Brazil

    Adenilso Simao

  2. School of Computer Science and Engineering, University of New South Wales, NSW 2052, Sydney, Australia

    Carroll Morgan

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Preoteasa, V. (2011). Algebra of Monotonic Boolean Transformers. In: Simao, A., Morgan, C. (eds) Formal Methods, Foundations and Applications. SBMF 2011. Lecture Notes in Computer Science, vol 7021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25032-3_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-25032-3_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-25031-6

  • Online ISBN: 978-3-642-25032-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation