Total correctness in nonstandard logics of programs
We show that termination is a first-order notion if approached via nonstandard logics of programs (NLP). We give explicit first-order characterizations of the program-verifying power of the well-known Mann- Cooper method for proving total correctness assertions (tca's). Similar characterization is given to the intermittent assertions method (w.r.t. tca's). A comparison of the tca-proving powers of distinguished methods (or logics of programs) is also attempted. We also show that NLP provided new methods which are strictly stronger than the Mann-Cooper method. In the end we turn to partial correctness issues related to the main body of the paper.
- A complete logic for reasoning about programs via nonstandard model theory. II
- A completeness theorem for dynamic logic
- A simple dynamic logic
- A simple proof for the completeness of Floyd's method
- An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic
- Hoare's logic for nondeterministic regular programs: A nonstandard approach
- scientific article; zbMATH DE number 3839296 (Why is no real title available?)
- scientific article; zbMATH DE number 3900134 (Why is no real title available?)
- scientific article; zbMATH DE number 3924132 (Why is no real title available?)
- scientific article; zbMATH DE number 3979058 (Why is no real title available?)
- scientific article; zbMATH DE number 3703966 (Why is no real title available?)
- scientific article; zbMATH DE number 3755858 (Why is no real title available?)
- scientific article; zbMATH DE number 3776849 (Why is no real title available?)
- scientific article; zbMATH DE number 3777465 (Why is no real title available?)
- scientific article; zbMATH DE number 3782362 (Why is no real title available?)
- scientific article; zbMATH DE number 3469999 (Why is no real title available?)
- scientific article; zbMATH DE number 3550181 (Why is no real title available?)
- scientific article; zbMATH DE number 3550662 (Why is no real title available?)
- scientific article; zbMATH DE number 3628347 (Why is no real title available?)
- scientific article; zbMATH DE number 3999893 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- Is “sometime” sometimes better than “always”?
- Non-standard algorithmic and dynamic logic
- On the termination of program schemas
- Programs and program verifications in a general setting
- Recursive Programs as Definitions in First-Order Logic
- STRUCTURED NONSTANDARD DYNAMIC LOGIC
- Non-standard algorithmic and dynamic logic
- Weak second order characterizations of various program verification systems
- Temporal logics need their clocks
- Algebraization of quantifier logics, an introductory overview
- Hoare's logic for nondeterministic regular programs: A nonstandard approach
- General correctness: A unification of partial and total correctness
- Recursive programs and denotational semantics in absolute logics of programs
- Unifying Recursion in Partial, Total and General Correctness
- Semantical proofs of correctness for programs performing non-deterministic tests on real numbers
- scientific article; zbMATH DE number 3856389 (Why is no real title available?)
- scientific article; zbMATH DE number 3921953 (Why is no real title available?)
- scientific article; zbMATH DE number 4022609 (Why is no real title available?)
- Reasoning in Dynamic Logic about Program Termination
- Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics
- On the strength of temporal proofs
This page was built for publication: Total correctness in nonstandard logics of programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q580955)
