Total correctness in nonstandard logics of programs

DOI10.1016/0304-3975(87)90118-6zbMath0626.68008OpenAlexW2015731361MaRDI QIDQ580955

Ildikó Sain

Publication date: 1987

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

Full work available at URL: https://doi.org/10.1016/0304-3975(87)90118-6

zbMATH Keywords

terminationpartial correctnessintermittent assertions methodMann-Cooper method for proving total correctness assertions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Recursive programs and denotational semantics in absolute logics of programs, Weak second order characterizations of various program verification systems, Temporal logics need their clocks, Algebraization of quantifier logics, an introductory overview, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, Reasoning in Dynamic Logic about Program Termination, Hoare's logic for nondeterministic regular programs: A nonstandard approach, On the strength of temporal proofs

Cites Work

• A completeness theorem for dynamic logic
• A simple proof for the completeness of Floyd's method
• An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic
• Non-standard algorithmic and dynamic logic
• A simple dynamic logic
• A complete logic for reasoning about programs via nonstandard model theory. II
• Programs and program verifications in a general setting
• Hoare's logic for nondeterministic regular programs: A nonstandard approach
• STRUCTURED NONSTANDARD DYNAMIC LOGIC
• On the termination of program schemas
• Is “sometime” sometimes better than “always”?
• Recursive Programs as Definitions in First-Order Logic
• 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
• Unnamed Item