Hoare Logic and Auxiliary Variables

Formal Aspects of Computing - Tập 11 Số 5 - Trang 541-566 - 1999
Thomas Kleymann1
1Laboratory for Foundations of Computer Science, The University of Edinburgh, Scotland, GB

Tóm tắt

Abstract.Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the role of auxiliary variables. We stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions. Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, one can show that Hoare Logic subsumes Vienna Development Method's (VDM) operation decomposition rules in that every derivation in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the presentation for verification calculi dealing with more interesting features such as recursion.

Từ khóa


Tài liệu tham khảo

Aczel P., 1982, January

Aczel P., 1982, Unpublished

America P., 1990, Proving total correctness of recursive procedures, Information and Computation, 84, 129, 10.1016/0890-5401(90)90037-I

Abadi M., Bidoit and Dauchet [BiD97], 682

Apt K. R., 1980, : Completeness with finite systems of intermediate assertions for recursive program schemes, SIAM Journal on Computing, 9, 665, 10.1137/0209050

Apt K. R., 1981, Ten years of Hoare’s logic: A survey - part I, ACM Transactions on Programming Languages and Systems, 3, 431, 10.1145/357146.357150

Bidoit M., 1997, editors, 10.1007/BFb0030581

Burstall R., 1993, Proceedings of MFCS '93, 32

Clarke Jr. E. M., 1979, Programming language constructs for which it is impossible to obtain good Hoare axiom systems, Journal of the ACM, 26, 129, 10.1145/322108.322121

Clint M., 1981, On the use of history variables, Acta Informatica, 16, 15, 10.1007/BF00289587

Cook S. A., 1978, Soundness and completeness of an axiom system for program verification, SIAM Journal on Computing, 7, 70, 10.1137/0207005

Cousot P., 1990, Handbook of Theoretical Computer Science, 841

Dahl O.-J., 1992, Verifiable Programming

de Bakker J., 1980, Mathematical Theory of Program Correctness

Dershowitz N., 1979, Proving termination with multiset orderings, Communications of the ACM, 22, 465, 10.1145/359138.359142

Floyd R. W., 1967, Proc. Symp. in Applied Mathematics, 19, 19

Gries D., 1980, Assignment and procedure call proof rules, ACM Transactions on Programming Languages and Systems, 2, 564, 10.1145/357114.357119

Gries D., 1981, The Science of Computer Programming, 10.1007/978-1-4612-5983-1

Halpern J. Y., 1984, Eleventh Annual Symposium on Principles of Programming Languages (POPL)

Hoare C. A. R., 1989, editors

Homeier P. V., 1996, Automated Deduction - CADE-13, 201, 10.1007/3-540-61511-3_81

Hoare C. A. R., 1969, An axiomatic basis for computer programming, Communications of the ACM, 12, 576, 10.1145/363235.363259

Hoare C. A. R., 1971, Symposium on Semantics of Algorithmic Languages, 102, 10.1007/BFb0059696

Hoare C. A. R., 1975, Parallel programming: An axiomatic approach, Computer Languages, 1, 151, 10.1016/0096-0551(75)90014-4

Hofmann M., 1997, Semantik und Verifikation

Jones C. B., 1986, Software Specification Techniques, 89

Jones C. B., 1990, : Systematic Software Development Using VDM

Jones C. B., 1990, Case Studies in Systematic Software Development

Kleymann T., 1999, Wolfgang Naraschewski

London R. L., 1978, Proof rules for the programming language Euclid, Acta Informatica, 10, 1, 10.1007/BF00260921

Luo Z., 1994, Computation and Reasoning: A Type Theory for Computer Science, 10.1093/oso/9780198538356.001.0001

[Mor] Morris J. H.: Comments on “procedures and parameters”. Undated and unpublished.

Morgan C. C., 1988, Procedures, parameters, and abstraction: separate concerns, Science of Computer Programming, 11, 17, 10.1016/0167-6423(88)90062-7

Morgan C. C., 1990, : Programming from Specifications

Nipkow T., 1998, Winskel is (almost) right: Towards a mechanized semantics textbook, Formal Aspects of Computing, 10, 171, 10.1007/s001650050009

Owicki S., 1976, An axiomatic proof technique for parallel programs, Acta Informatica, 6, 319, 10.1007/BF00268134

Olderog E.-R., 1981, Sound and complete Hoare-like calculi based on copy rules, Acta Informatica, 16, 161

Olderog E.-R., 1983, On the notion of expressiveness and the rule of adaptation, Theoretical Computer Science, 24, 337, 10.1016/0304-3975(83)90009-9

Reynolds J. C., 1982, Tools & Notions for Program Construction

Schreiber T., Bidoit and Dauchet [BiD97], 697

Sokolowski S., 1977, Sixth Mathematical Foundations of Computer Science (Tatranská Lomnica), 475, 10.1007/3-540-08353-7_170

Soundararajan N., 1984, A proof technique for parallel programs, Theoretical Computer Science, 31, 13, 10.1016/0304-3975(84)90122-1

Stirling C., 1988, A generalization of Owicki-Gries’s Hoare Logic for a concurrent while language, Theoretical Computer Science, 58, 347, 10.1016/0304-3975(88)90033-3

Stølen K., 1991, Proceedings of CONCUR '91, 510, 10.1007/3-540-54430-5_110

Tarlecki A., 1985, A language of specified programs, Science of Computer Programming, 5, 59, 10.1016/0167-6423(85)90004-8

Vickers S., 1991, Software engineer’s reference book

von Oheimb D., 1999, Nineteenth Conference on the Foundations of Software Technology and Theoretical Computer Science

Zwiers J., 1989, Compositionality, Concurrency and Partial Correctness

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Tập 11 Số 5

541-566

Thông tin tác giả