Total correctness in nonstandard logics of programs (Q580955): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(4 intermediate revisions by 4 users not shown) | |||
Property / review text | |||
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. | |||
Property / review text: 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. / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q60 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 4018356 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
termination | |||
Property / zbMATH Keywords: termination / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
Mann-Cooper method for proving total correctness assertions | |||
Property / zbMATH Keywords: Mann-Cooper method for proving total correctness assertions / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
intermittent assertions method | |||
Property / zbMATH Keywords: intermittent assertions method / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
partial correctness | |||
Property / zbMATH Keywords: partial correctness / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0304-3975(87)90118-6 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2015731361 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3309036 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A complete logic for reasoning about programs via nonstandard model theory. II / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3939224 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4054648 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Recursive Programs as Definitions in First-Order Logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5679729 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Programs and program verifications in a general setting / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A completeness theorem for dynamic logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3960106 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Hoare's logic for nondeterministic regular programs: A nonstandard approach / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4726228 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A simple dynamic logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the termination of program schemas / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4124327 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4190096 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Is “sometime” sometimes better than “always”? / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4124795 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3956390 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Non-standard algorithmic and dynamic logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3744163 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3896482 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: STRUCTURED NONSTANDARD DYNAMIC LOGIC / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A simple proof for the completeness of Floyd's method / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3698302 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3956920 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3678651 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 12:27, 18 June 2024
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
0 references