Towards reasoning about Hoare relations. (English) Zbl 0858.68057
Summary: A logical framework is presented for defining semantics of programs that satisfy Hoare postulates. The two families of logical systems are given: modal systems and relational systems. In the modal systems semantics of Hoare-style programming languages is provided in terms of relations and sets, and in relational systems in terms of relations only. Proof theory for the given logics is presented.
References:
| [1] | P. Blackburn, Nominal tense logic and other sorted intensional frameworks, Ph.D. Thesis, University of Edinburgh, Edinburgh (1990). |
| [2] | R. Bull and K. Segerberg, Basic modal logic, in: D.M. Gabbay and F. Guenthner (eds.),Handbook of Philosophical Logic, Vol. II, (Reidel, Dordrecht, 1984) pp. 1-88. · Zbl 0875.03045 |
| [3] | R.J.R. Back and J. von Wright, Refinement calculus, Part I: Sequential programs, in:Proc. 1989 REX Workshop for Refinement of Distributed Systems, Lecture Notes in Computer Science 430 (Springer, 1989). |
| [4] | F.B. Chellas,Modal Logic (Cambridge University Press, 1980). · Zbl 0431.03009 |
| [5] | J.W. de Bakker and W.F. de Roever, A calculus for recursive program schemes, in: M. Nivat (ed.),Automata, Languages and Programming (North-Holland, 1973) pp. 167-196. · Zbl 0262.68004 |
| [6] | M. de Rijke, The modal logic of inequality, J. Symbolic Logic 57 (1992) 566-584. · Zbl 0788.03019 · doi:10.2307/2275293 |
| [7] | E.W. Dijkstra and C.S. Scholten,Predicate Calculus and Program Semantics (Springer, New York, 1990). · Zbl 0698.68011 |
| [8] | G. Gargov and V. Goranko, Modal logic with names, J. Philos. Logic 22 (1993) 607-636. · Zbl 0793.03012 · doi:10.1007/BF01054038 |
| [9] | R. Goldblatt,Logics of Time and Computation, CSLI Standford, 2nd ed. (1992). |
| [10] | V. Goranko, Modal definability in enriched languages, Notre Dame J. Formal Logic (1990) 81-105. · Zbl 0706.03016 |
| [11] | G. Gargov, G. Passy and T. Tinchev, Modal environment for boolean speculations, in: D. Skordev (ed.),Mathematical Logic and its Applications (Plenum Press, 1987) pp. 253-263. · Zbl 0701.03008 |
| [12] | P. Guerreiro, A relational model for nondeterministic programs and predicate transformers, in:Proc. 4th Int. Colloq. on Automata, Languages and Programming, Paris, Lecture Notes in Computer Science 83 (Springer, 1980) pp. 136-146. · Zbl 0436.68008 |
| [13] | D. Harel,First-order Dynamic Logic, Lecture Notes in Computer Science 69 (Springer, 1979). · Zbl 0403.03024 |
| [14] | C. Hoare, I.J. Hayes, He Jifeng, C.C. Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sorensen, J.M. Spivey and B.A. Sufrin, Laws of programming, Commun. ACM 30 (1987) 672-686. · Zbl 0629.68006 · doi:10.1145/27651.27653 |
| [15] | C.A.R. Hoare and He Jifeng, The weakest prespecification, Parts I and II, Fundamenta Informaticae 9 (1986) 51-84, 217-262. · Zbl 0603.68009 |
| [16] | C.A.R. Hoare and He Jifeng, The weakest prespecification, Inform. Processing Lett. 24 (1987) 127-132. · Zbl 0622.68025 · doi:10.1016/0020-0190(87)90106-2 |
| [17] | D. Jacobs and D. Gries, General correctness: A unification of partial and total correctness, Acta Informatica 22 (1985) 67-83. · Zbl 0559.68021 · doi:10.1007/BF00290146 |
| [18] | R.D. Maddux, A working relational model: The derivation of the Dijkstra-Scholten predicate transformer semantics from Tarski’s axioms for the Peirce-Schröder calculus of relations, South African Comp. J. 9 (1993) 92-130. |
| [19] | G. Mirkowska and A. Salwicki,Algorithmic Logic (Reidel, Dordrecht, 1987). · Zbl 0648.03018 |
| [20] | G. Nelson, A generalization of Dijkstra’s calculus, ACM Trans. Prog. Languages and Syst. 11 (1989) 517-561. · doi:10.1145/69558.69559 |
| [21] | T. Nguyen, A relational model of demonic nondeterministic programs, Int. J. Found. Comp. Sci. 2 (1991) 101-131. · Zbl 0739.68063 · doi:10.1142/S012905419100008X |
| [22] | E. Orlowska, Relational interpretation of modal logics, in: H. Andreka, D. Monk and I. Nemeti (eds.),Algebraic logic. Colloquia Mathematica Societatis Janos Bolyai 54 (North-Holland, Amsterdam, 1988) pp. 443-471. |
| [23] | E. Orlowska, Dynamic logic with program specifications and its relational proof system, Int. J. Appl. Non-Classical Logics (1992). · Zbl 0802.03025 |
| [24] | G.D. Plotkin, A powerdomain construction, SIAM J. Comput. 5 (1976) 452-487. · Zbl 0355.68015 · doi:10.1137/0205035 |
| [25] | V.R. Pratt, Semantical considerations on Floyd-Hoare logic, in:Proc. 17th IEEE Symp. Foundations of Computer Science (1976) pp. 109-121. |
| [26] | S. Passy and T. Tinchev, PDL with data constants, Inform. Processing Lett. 20 (1985) 35-41 · Zbl 0577.68046 · doi:10.1016/0020-0190(85)90127-9 |
| [27] | H. Rasiowa and R. Sikorski,The Mathematics of Metamathematics (PWN-Polish Sci. Publ. Warsaw, 1963). · Zbl 0122.24311 |
| [28] | K. Segerberg, ?somewhere else? and ?some other time?, in:Wright and Wrong, Mini-essays in honor of Georg Henrik von Wright (1976) 61-69. |
| [29] | K. Segerberg, A note on the logic of elsewhere, Theoria 47 (1981) 183-187. |
| [30] | K. Segerberg, A completeness theorem in the modal logic of programs, in: T. Traczyk (ed.),Universal Algebra and Applications, (Banach Center Publications, Vol. 9 PWN ? Polish Sci. Pub. Warsaw, 1982) pp. 31-46. · Zbl 0546.03011 |
| [31] | J. van Benthem, Correspondence theory, in: D.M. Gabbay and F. Guenthner (eds.),Handbook of Philosophical Logic, Vol. II (Reidel, Dordrecht, 1984) pp. 167-247. · Zbl 0875.03048 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
