The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic

DOI10.1007/s11704-015-4024-2zbMath1404.03028OpenAlexW2303516764MaRDI QIDQ1712495

Zaiyue Zhang, Yuefei Sui, Cun-Gen Cao

Publication date: 22 January 2019

Published in: Frontiers of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11704-015-4024-2

zbMATH Keywords

recursive functionHoare logicnonstandard model of Peano arithmeticcomputable function

Mathematics Subject Classification ID

Logic in computer science (03B70) Nonstandard models of arithmetic (03H15) Recursive functions and relations, subrecursive hierarchies (03D20)

Cites Work

• Unnamed Item
• Unnamed Item
• Expressiveness and the completeness of Hoare's logic
• On the completeness of propositional Hoare logic
• The ``Hoare Logic of CSP, and All That
• Separation and information hiding
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Separation logic and abstraction
• An axiomatic basis for computer programming

This page was built for publication: The \(\mathbf{M}\)-computations induced by accessibility relations in nonstandard models \(\mathbf{M}\) of Hoare logic