TU Darmstadt / ULB / TUbiblio

Technical Report: Using Loop Scopes with for-Loops

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 View Item