Total correctness in nonstandard logics of programs (Q580955)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Total correctness in nonstandard logics of programs |
scientific article |
Statements
Total correctness in nonstandard logics of programs (English)
0 references
1987
0 references
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.
0 references
termination
0 references
Mann-Cooper method for proving total correctness assertions
0 references
intermittent assertions method
0 references
partial correctness
0 references