A complete logic for reasoning about programs via nonstandard model theory. II

DOI10.1016/0304-3975(82)90025-1zbMath0475.68010OpenAlexW4256371891MaRDI QIDQ1159461

Ildikó Sain, Hajnalka Andréka, Istvan Németi

Publication date: 1982

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

Full work available at URL: https://doi.org/10.1016/0304-3975(82)90025-1

zbMATH Keywords

dynamic logicsemanticsexpressive powerFloyd's method

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Nonstandard models (03H99)

Related Items (17)

Non-standard algorithmic and dynamic logic ⋮ A simple dynamic logic ⋮ Recursive programs and denotational semantics in absolute logics of programs ⋮ Some general incompleteness results for partial correctness logics ⋮ Weak second order characterizations of various program verification systems ⋮ Output concepts for accelerated Turing machines ⋮ Temporal logics need their clocks ⋮ Axiomatizing fixpoint logics ⋮ Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics ⋮ On strictly arithmetical completeness in logics of programs ⋮ Total correctness in nonstandard logics of programs ⋮ A unifying theorem for algebraic semantics and dynamic logics ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ A simple proof for the completeness of Floyd's method ⋮ Some questions about expressiveness and relative completeness in Hoare's logic ⋮ On the strength of temporal proofs ⋮ An essay in combinatory dynamic logic

Cites Work

• A theory of interactive programming
• Programs and program verifications in a general setting
• Model theory
• Model theory for tense logics
• On the termination of program schemas
• Soundness and Completeness of an Axiom System for Program Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A complete logic for reasoning about programs via nonstandard model theory. II