Termination assertions for recursive programs: Completeness and axiomatic definability

DOI10.1016/S0019-9958(83)80053-9MaRDI QIDQ3323258zbMATH OpenOpenAlexFDO

Authors Albert R. Meyer, John Mitchell

Publication date 1983

Published in Information and Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0019-9958(83)80053-9

zbMATH Keywords

completenessrecursive proceduressoundnessterminationaxiom systemrecursive programglobal procedure calls

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• Reasoning in Dynamic Logic about Program Termination
• scientific article; zbMATH DE number 4005583
• Effective Axiomatizations of Hoare Logics
• Completeness for recursive procedures in separation logic
• Proof rules for recursive procedures

Cited in

(6)

• Inductive completeness of logics of programs
• Termination Proofs for Recursive Functions in FoCaLiZe
• Reasoning in Dynamic Logic about Program Termination
• Execution termination and computation determinacy of data-flow program nets
• Axiomatization of if-then-else over possibly non-halting programs and tests
• Necessary and sufficient conditions for the universality of programming formalisms

This page was built for publication: Termination assertions for recursive programs: Completeness and axiomatic definability

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