On the status of proving program properties in effective interpretations

DOI10.1016/0304-3975(93)90245-OMaRDI QIDQ689289zbMATH OpenOpenAlexFDO

Authors Michał Grabowski

Publication date 20 March 1995

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(93)90245-o

zbMATH Keywords

program correctnesstheories of interpretations

Mathematics Subject Classification ID

Logic in computer science (03B70) Models of arithmetic and set theory (03C62) Theory of numerations, effectively presented structures (03D45) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The paper is based on the previous published results of the author. Considering dynamic theories, the author tries to give a generalisation of Lipton's theorem (R. Lipton: ``A necessary and sufficient condition for the existence of Hoare logics, Proc. 18th IEEE Symp. FOCS (1977). The idea starts from the fact that every proof system for program correctness yields an enumeration procedure for correctness assertions. The effective interpretations are given by recursive subset of \(\omega\) and recursive functions and relations. The paper presents a sufficient condition for a uniform procedure enumerating dynamic theories of interpretations. If arithmetical notions are first-order-definable by universal or existential formulas within this interpretation, then there exists an appropriate uniform procedure.

Recommendations

• A completeness theorem for dynamic logic
• Effective Axiomatizations of Hoare Logics
• scientific article; zbMATH DE number 4101151
• On relative completeness of Hoare logics
• Dijkstra's interpretation of the approach to solving a problem of program correctness

Cites work

• Effective Axiomatizations of Hoare Logics
• scientific article; zbMATH DE number 4022609 (Why is no real title available?)
• On relative completeness of Hoare logics
• Ten Years of Hoare's Logic: A Survey—Part I

This page was built for publication: On the status of proving program properties in effective interpretations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q689289)