Wasser, Nathan and Steinhöfel, Dominic (2019):
Technical Report: Using Loop Scopes with for-Loops.
[Report]
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.
Item Type: | Report |
---|---|
Erschienen: | 2019 |
Creators: | Wasser, Nathan and Steinhöfel, Dominic |
Title: | Technical Report: Using Loop Scopes with for-Loops |
Language: | German |
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. |
Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
Date Deposited: | 23 Jan 2019 07:49 |
Official URL: | https://arxiv.org/abs/1901.06839 |
Identification Number: | arXiv:1901.06839 |
Export: | |
Suche nach Titel in: | TUfind oder in Google |
![]() |
Send an inquiry |
Options (only for editors)
![]() |
Show editorial Details |