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

DOI10.1007/BF00290145zbMath0546.68011MaRDI QIDQ797985

Jean-Raymond Gagné, Ali Milli, Jules Desharnais

Publication date: 1985

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

loop invariantsStrongest invariant functionswhile statements

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

Regularity of relations: A measure of uniformity ⋮ Convergence: integrating termination and abort-freedom ⋮ Mechanical inference of invariants for FOR-loops ⋮ Reflexive transitive invariant relations: A basis for computing loop functions ⋮ A relation-algebraic approach to the ``Hoare logic of functional dependencies ⋮ A versatile concept for the analysis of loops ⋮ Mathematics for reasoning about loop functions

Cites Work

• Verifying programs by induction on their data structure: general format and applications
• A relational theory of computing
• A generalized control structure and its formal definition
• The new math of computer programming
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item