Published in Volume XXVI, Issue 2, 2016, pages 125-156, doi: 10.7561/SACS.2016.2.125

Authors: J.A. Bergstra, C.A. Middelburg

Abstract

We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerned. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.

Full Text (PDF)

References

[1] K. R. Apt. Ten years of Hoare’s logic: A survey – Part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, 1981. doi:10.1145/357146.357150.

[2] J. A. Bergstra and M. E. Loots. Program algebra for sequential code. Journal of Logic and Algebraic Programming, 51(2):125–156, 2002. doi: 10.1016/S1567-8326(02)00018-8.

[3] J. A. Bergstra and C. A. Middelburg. Program algebra with a jump-shift instruction. Journal of Applied Logic, 6(4):553–563, 2008. doi: 10.1016/j.jal.2008.07.001.

[4] J. A. Bergstra and C. A. Middelburg. Instruction sequence processing operators. Acta Informatica, 49(3):139–172, 2012. doi:10.1007/s00236-012-0154-2.

[5] J. A. Bergstra and C. A. Middelburg. Instruction Sequences for Computer Science, volume 2 of Atlantis Studies in Computing. Atlantis Press, Amsterdam, 2012. doi:10.2991/978-94-91216-65-7.

[6] J. A. Bergstra and C. A. Middelburg. Instruction sequence based non-uniform complexity classes. Scientific Annals of Computer Science, 24(1):47–89, 2014. doi:10.7561/SACS.2014.1.47.

[7] J. A. Bergstra and C. A. Middelburg. On instruction sets for Boolean registers in program algebra. Scientific Annals of Computer Science, 26(1):1–26, 2016. doi:10.7561/SACS.2016.1.1.

[8] J. A. Bergstra and J. V. Tucker. Two theorems about the completeness of Hoare’s logic. Information Processing Letters, 15(4):143–149, 1982. doi:10.1016/0020-0190(82)90095-3.

[9] E. M. Clarke. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Journal of the ACM, 26(1):129–147, 1979. doi:10.1145/322108.322121.

[10] M. Clint and C. A. R. Hoare. Program proving: Jumps and functions. Acta Informatica, 1(3):214–224, 1972. doi:10.1007/BF00288686.

[11] S. A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing, 7(1):70–90, 1978. doi:10.1137/0207005.

[12] A. de Bruin. Goto statements: Semantics and deduction systems. Acta Informatica, 15(4):385–424, 1981. doi:10.1007/BF00264536.

[13] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification I: Equations and Initial Semantics, volume 6 of EATCS Monographs. Springer-Verlag, Berlin, 1985. doi:10.1007/978-3-642-69962-7.

[14] R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19–32. American Mathematical Society, 1967.

[15] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 583, 1969. doi:10.1145/363235.363259.

[16] W. A. Hodges. Model Theory, volume 42 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1993.

[17] J. B. Jensen, N. Benton, and A. Kennedy. High-level separation logic for low-level code. In POPL 2013, pages 301–314. ACM Press, 2013. doi:10.1145/2480359.2429105.

[18] C. A. Middelburg. Instruction sequences as a theme in computer science. https://instructionsequence.wordpress.com/, 2015.

[19] M. O. Myreen and M. J. C. Gordon. Hoare logic for realistically modelled machine code. In O. Grumberg and M. Huth, editors, TACAS 2007, volume 4424 of Lecture Notes in Computer Science, pages 568–582. Springer-Verlag, 2007. doi:10.1007/978-3-540-71209-1_44.

[20] J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS 2002, pages 55–74. IEEE Computer Society Press, 2002.

[21] A. Saabas and T. Uustalu. A compositional natural semantics and Hoare logic for low-level languages. Theoretical Computer Science, 373(3):273–302, 2007. doi:10.1016/j.tcs.2006.12.020.

[22] D. Sannella and A. Tarlecki. Algebraic preliminaries. In E. Astesiano, H.-J. Kreowski, and B. Krieg-Brückner, editors, Algebraic Foundations of Systems Specification, pages 13–30. Springer-Verlag, Berlin, 1999. doi:10.1007/978-3-642-59851-7_2.

[23] D. Sannella and A. Tarlecki. Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science, An EATCS Series. Springer-Verlag, Berlin, 2012. doi:10.1007/978-3-642-17336-3.

[24] G. Tan and A. W. Appel. A compositional logic for control flow. In E. A. Emerson and K. S. Namjoshi, editors, VMCAI 2006, volume 3855 of Lecture Notes in Computer Science, pages 80–94. Springer-Verlag, 2006. doi:10.1007/11609773_6.

[25] A. Wang. An axiomatic basis for proving total correctness of goto-programs. BIT Numerical Mathematics, 16(1):88–102, 1976. doi: 10.1007/BF01940782a.

[26] M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 675–788. Elsevier, Amsterdam, 1990.

Bibtex

@article{sacscuza:bergstra2016ahloasis,
  title={A Hoare-Like Logic of  Asserted Single-Pass Instruction Sequences},
  author={J.A. Bergstra and C.A. Middelburg},
  journal={Scientific Annals of Computer Science},
  volume={26},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2016},
  pages={125--156},
  doi={10.7561/SACS.2016.2.125},
  publisher={``A.I. Cuza'' University Press}
}