Strongest invariant functions: Their use in the systematic analysis of while statements

DOI10.1007/BF00290145MaRDI QIDQ797985zbMATH OpenFDO

Authors Ali Mili, Jules Desharnais, Jean-Raymond Gagné

Publication date 1985

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00290145

zbMATH Keywords

loop invariantsStrongest invariant functionswhile statements

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Review text

Strongest invariant functions, a useful tool in the analysis of while statements, are defined and discussed. Their relationships to loop invariants and to the function computed by the while statement are investigated.

Recommendations

• Invariant functions and invariant relations: an alternative to invariant assertions
• A versatile concept for the analysis of loops
• Reflexive transitive invariant relations: A basis for computing loop functions
• Relational methods in the analysis of while loops: observations of versatility
• Computing Preconditions and Postconditions of While Loops

Cites work

• A generalized control structure and its formal definition
• A relational theory of computing
• An axiomatic basis for computer programming
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3768952 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3630186 (Why is no real title available?)
• The new math of computer programming
• Verifying programs by induction on their data structure: general format and applications

Cited in

(9)

• Mathematics for reasoning about loop functions
• Convergence: integrating termination and abort-freedom
• Invariant functions and invariant relations: an alternative to invariant assertions
• Regularity of relations: A measure of uniformity
• Relational methods in the analysis of while loops: observations of versatility
• A relation-algebraic approach to the ``Hoare logic of functional dependencies
• A versatile concept for the analysis of loops
• Mechanical inference of invariants for FOR-loops
• Reflexive transitive invariant relations: A basis for computing loop functions

This page was built for publication: Strongest invariant functions: Their use in the systematic analysis of while statements

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