# Technical Report: Using Loop Scopes with for-Loops

**Authors:** Nathan Wasser, Dominic Steinhöfel  
**arXiv:** [1901.06839](https://arxiv.org/abs/1901.06839)  
**Date:** 2019-01-21  
**Summary page:** https://www.summarizepaper.com/fr/arxiv-id/1901.06839v2/

## 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.