Generalizing specifications for uniformly implemented loops

DOI10.1145/2363.2708zbMATH Open0559.68003OpenAlexW1985830587MaRDI QIDQ5184367FDOQ5184367

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/

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

zbMATH Keywords

verificationwhile loopsgeneralizing functional specificationsiteration conditionuniformly implemented loops

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

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)