Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less

—Increasingly, tools and their underlying theories are able to cope with “real code” written as part of industrial grade applications almost as is. It has been our experience that one area that would benefit from further improvements is the treatment of loops. Most existing verification techniques are solely applicable to a structured and disciplined use of loops. Unfortunately, unstructured loops are fairly common: e.g. over 40% of the 1500 loops in the Eclipse JDT are unstructured, either having a condition with side-effects and/or break, return or continue statements in the body. We illustrate how the total correctness of while loops in Java, structured or not, can be supported by small adaptations to the corresponding classical Hoare Logic rule. Other changes we propose result in a loop semantics that enable verification tools to offer better diagnostics despite allowing more concise loop specifications. Keywords-Hoare Logic; static loop verification; unstructured loops; side...

• Type: Conference
• Year: 2009
• Where: SEFM
• Authors: Patrice Chalin
• Keywords: Most Existing Verification, SEFM 2009, Side-effects And/or Break, Software Engineering, Unstructured Loops