# Technical Report: Using Loop Scopes with for-Loops

## TL;DR

This paper extends the concept of loop scopes from while-loops to for-loops and introduces sound loop unrolling rules, enabling more straightforward semi-automated proofs without program transformation.

## Contribution

It presents a novel extension of loop scopes to for-loops and provides sound unrolling rules that treat for-loops as first-class citizens, simplifying proof processes.

## Key findings

- Extended loop scopes to for-loops
- Developed sound unrolling rules for loops
- Facilitated easier semi-automated proofs

## Abstract

Loop scopes have been shown to be a helpful tool in creating sound loop invariant rules which do not require program transformation of the loop body. Here we extend this idea from while-loops to for-loops and also present sound loop unrolling rules for while- 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 -- rather than the usual approach of transforming for-loops into while-loops -- which makes semi-automated proofs easier to follow for the user, who may need to provide help in order to finish the proof.