Hoare's logic for nondeterministic regular programs: A nonstandard approach

DOI10.1016/0304-3975(89)90165-5zbMath0679.68024OpenAlexW2010093011MaRDI QIDQ1822934

M. Teresa Hortalá-González, Mario Rodríguez Artalejo

Publication date: 1989

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

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90165-5

zbMATH Keywords

Hoare's logiccontinuous semanticsnondeterministic regular programsnonstandard dynamic logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items

Weak second order characterizations of various program verification systems ⋮ Total correctness in nonstandard logics of programs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Total correctness in nonstandard logics of programs
• Proving program inclusion using Hoare's logic
• The axiomatic semantics of programs based on Hoare's logic
• A simple proof for the completeness of Floyd's method
• Ten years of Hoare's logic: A survey. II: Nondeterminism
• Some questions about expressiveness and relative completeness in Hoare's logic
• Non-standard algorithmic and dynamic logic
• A simple dynamic logic
• Some general incompleteness results for partial correctness logics
• A complete logic for reasoning about programs via nonstandard model theory. II
• Programs and program verifications in a general setting
• First-order dynamic logic
• On the notion of expressiveness and the rule of adaptation
• On the strength of “sometimes” and “always” in program verification
• STRUCTURED NONSTANDARD DYNAMIC LOGIC
• A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
• Semantics of looping programs in Propositional Dynamic Logic
• Guarded commands, nondeterminacy and formal derivation of programs
• On the termination of program schemas
• Soundness and Completeness of an Axiom System for Program Verification
• Recursive Programs as Definitions in First-Order Logic
• Flow diagrams, turing machines and languages with only two formation rules
• An axiomatic basis for computer programming

This page was built for publication: Hoare's logic for nondeterministic regular programs: A nonstandard approach