Additional transformations for multiple‐level escape statements
Ronald A. Olsson · Software Testing Verification and Reliability · 2002
Abstract Earlier work suggests that program transformations can simplify program verification. A given program containing complex language features is transformed into a semantically equivalent program containing only simpler language features. The transformed program is proven using a set of proof rules for only the simpler features. That approach was illustrated by transforming a given program that may contain multiple‐level escape statements within nested loops into an equivalent program that contains no escape statements. This paper gives additional transformations, which map a given program that may contain multiple‐level escape statements to a semantically equivalent program (TP) that contains only single‐level escape statements. The proof of TP uses proof rules for single‐level escape statements, or the earlier transformations further map TP to a program with no escape statements, whose proof uses proof rules for loops without escape statements. This paper also discusses escape statements where the number of levels is determined at run‐time. Copyright © 2002 John Wiley & Sons, Ltd.