Total correctness in nonstandard logics of programs

AbstractWe 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 Manna-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 provides new methods which are strictly stronger than the Manna-Cooper method. In the end we turn to partial correctness issues related to the main body of the paper