2 papers
cs.PL2020
Treating for-Loops as First-Class Citizens in Proofs
Nathan Wasser, Dominic Steinhöfel
Indexed loop scopes have been shown to be a helpful tool in creating sound loop invariant rules in dynamic logic for programming languages with abrupt completion, such as Java. The…
cs.PL2019
Technical Report: Using Loop Scopes with for-Loops
Nathan Wasser, Dominic Steinhöfel
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…