Verification of a class of loop programs without using loop invariants (Q2265799)

A method is considered for simplifying the verification of structured loop programs that do not contain embedded loops. An axiomatic system is described that constitutes a modification of Hoare's logic and that uses recursive functions instead of loop invariants, these functions being directly determined in accordance with the syntactic structure of the loops.