Advertisement

Reasoning about Multi-process Systems with the Box Calculus

  • Greg Michaelson
  • Gudmund Grov
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7241)

Abstract

The box calculus is a formalism for reasoning about the properties of multi-process systems which enables account to be taken of pragmatic as well as computational concerns. It was developed for the programming language Hume which explicitly distinguishes between coordination, based on concurrent boxes linked by wires, and expressions, based on polymorphic recursive functions. This chapter introduces Hume expressions and surveys classic techniques for reasoning about functional programs. It then explores Hume coordination and the box calculus, and examines how Hume programs may be systematically transformed while maintaining computational and pragmatic correctness.

Keywords

Truth Table Recursive Function Output Link Peano Arithmetic Structural Induction 
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. Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the Association for Computing Machinery 24(1), 44–67 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  2. Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall (1997)Google Scholar
  3. Bird, R.S.: An introduction to the theory of lists. In: Broy, M. (ed.) Logic of Programming and Calculi of Discrete Design, pp. 3–42. Springer, Heidelberg (1987)Google Scholar
  4. Breitinger, S., Loogen, R., Ortega Mallen, Y., Pena, R.: The Eden Coordination Model for Distributed Memory Systems. In: Proceedings of the 1997 Workshop on High-Level Programming Models and Supportive Environments (HIPS 1997), pp. 120–124. IEEE Computer Society, Washington, DC (1997)Google Scholar
  5. Burstall, R.: Proving properties of programs by structural induction. Computer Journal 12(1), 41–48 (1969)CrossRefzbMATHGoogle Scholar
  6. Church, A.: An unsolvable problem of elementary number theory. American Journal of Mathematics 58, 345–363 (1936)MathSciNetCrossRefzbMATHGoogle Scholar
  7. Chapman, B., Jost, G., van der Pas, R.: Using OpenMP: Portable Shared Memory Parallel Programming (Scientific and Engineering Computation). MIT (2007)Google Scholar
  8. Dijkstra, E.W.: Guarded commands, non-determinacy and derivation of programs. Commuications of the ACM 18(8), 453–457 (1975)CrossRefzbMATHGoogle Scholar
  9. Peyton Jones, S.L. (ed.), Augustsson, L., Boutel, B., Burton, F.W., Fasel, J.H., Gordon, A.D., Hammond, K., Hughes, R.J.M., Hudak, P., Johnsson, T., Jones, M.P., Peterson, J.C., Reid, A., Wadler, P.L.: Report on the Non-Strict Functional Language, Haskell (Haskell98). Technical report, Yale University (1999) Google Scholar
  10. Grov, G., Michaelson, G.: Towards a Box Calculus for Hierarchical Hume. In: Morazan, M. (ed.) Trends in Functional Programming, vol. 8, pp. 71–88. Intellect (2008)Google Scholar
  11. Grov, G., Michaelson, G.: Hume box calculus: robust system development through software transformation. In: Higher Order Symbolic Computing (July 2011), doi:10.1007/s10990-011-9067-yGoogle Scholar
  12. Grov, G.: Reasoning about correctness properties of a coordination language. PhD thesis, Heriot-Watt University (2009)Google Scholar
  13. Halmos, P.R.: Naive Set theory. Van Nostrand (1960)Google Scholar
  14. Hammond, K., Michaelson, G.: Hume: A Domain-Specific Language for Real-Time Embedded Systems. In: Pfenning, F., Macko, M. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 37–56. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12, 576–583 (1969)CrossRefzbMATHGoogle Scholar
  16. Hoare, C.A.R.: Communicating Sequential Processes. Communications of the ACM 21(8), 666–677 (1978)CrossRefzbMATHGoogle Scholar
  17. Hodges, W.: Logic. Pelican (1977)Google Scholar
  18. Inmos: Occam Reference Manual. Prentice-Hall (1988)Google Scholar
  19. Kneebone, G.: Mathematical Logic and the Foundations of Mathematics. Van Nostrand (1963)Google Scholar
  20. McCarthy, J.: A basis for a mathematical theory of computation. Technical Report Memo 31. MIT (1962)Google Scholar
  21. MPI-Forum: MPI: A message passing intrface standard. International Journal of Supercomputer Application 8(3-4), 165–414 (1994)Google Scholar
  22. Milner, R.: A Calculus of Communicating Systems. Springer (1982)Google Scholar
  23. Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)Google Scholar
  24. Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press (1997)Google Scholar
  25. Nidditch, P.H.: Propositional Calculus. Routledge and Kegan Paul (1962)Google Scholar
  26. Peter, R.: Recursive Functions. Academic Press (1967)Google Scholar
  27. Quine, W.V.: Word and Object. MIT (1964)Google Scholar
  28. Wegner, P.: Programming Languages, Information Structures, and Machine Organization. McGraw-Hill (1968)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Greg Michaelson
    • 1
  • Gudmund Grov
    • 2
  1. 1.Heriot-Watt UniversityUK
  2. 2.University of EdinburghUK

Personalised recommendations

Cite chapter

Buy options