Wasser, Nathan and Steinhöfel, Dominic (2019):
Technical Report: Using Loop Scopes with for-Loops.
[Online-Edition: https://arxiv.org/abs/1901.06839],
[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: |
Optionen (nur für Redakteure)
 |
View Item |
Drucken
Impressum