Verification of a class of loop programs without using loop invariants

MaRDI QIDQ2265799zbMATH OpenFDO

Authors L. V. Chernobrod

Publication date 1984

Published in Programming and Computer Software (Search for Journal in Brave)

zbMATH Keywords

Hoare's logicloop invariantsrecursive functionsstructured loop programsverification

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

• Elimination of loop invariants in program verification
• Problem-oriented program verification
• Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
• Inadequacy of computable loop invariants
• Problem-oriented approach to verification of file-processing programs

Cited in

(6)

• Elimination of loop invariants in program verification
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Proving loop termination: Beyond the traditional method
• Inferring Loop Invariants Using Postconditions
• A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Verification of a class of loop programs without using loop invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2265799)