2020/02/03 by Nathan Wasser, Wasser, Nathan, Dominic Steinhöfel +1
Computer Science · Mathematics · #FOS: Computer and information sciences #Formal Methods in Verification #History and Theory of Mathematics #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2002.00776
openalex publication_date 2020/02/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Indexed loop scopes have been shown to be a helpful tool in creating sound loop invariant rules in dynamic logic for programming languages with abrupt completion, such as Java. These rules do not require program transformation of the loop body, as other approaches to dealing with abrupt completion do. However, indexed loop scopes were designed specifically to provide a loop invariant rule for while loops and work rather opaquely. Here we propose replacing indexed loop scopes with a more transparent solution, which also lets us extend this idea from while loops to for loops. We further present sound loop unrolling rules for while, do and for loops, which require neither program transformation of the loop body, nor the use of nested modalities. This approach allows for loops to be treated as first-class citizens in proofs -- rather than the usual approach of transforming for loops into while loops -- which makes semi-automated proofs more transparent and easier to follow for the user, whose interactions may be required in order to close the proofs.