Generalizing specifications for uniformly implemented loops

DOI10.1145/2363.2708MaRDI QIDQ5184367zbMATH OpenOpenAlexFDO

Authors Douglas D. Dunlop, Victor R. Basili

Publication date 1985

Published in ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL http://www.acm.org/pubs/contents/journals/toplas/1985-7/

zbMATH Keywords

verificationwhile loopsgeneralizing functional specificationsiteration conditionuniformly implemented loops

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Recommendations

• A Heuristic for Deriving Loop Functions
• Reasoning about loops in total and general correctness
• Mechanical inference of invariants for FOR-loops
• A versatile concept for the analysis of loops
• Synthesis of the programmed functions offor loops on data structures

Cited in

(3)

• A Heuristic for Deriving Loop Functions
• Symbolic verification method for definite iteration over data structures
• Verification of a finite iteration over data structures

This page was built for publication: Generalizing specifications for uniformly implemented loops

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