Loop Scope Invariant Rule

This page supplies additional material for the paper “A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows“, accepted for iFM 2017.

The extended technical report based on the iFM submission can be found here. The technical report additionally contains material that we had to leave out in the submission for space reasons.

Complete Statistics Table

Complementary Files

Below you find the versions of KeY needed to reproduce the examples mentioned in the paper, as well as the problem (.key) and proof (.proof) files representing the examples. You can download the KeY versions using the green buttons. After downloading and unzipping the linked files, start KeY by running java -jar KeY.jar in the newly created directory. A Java Runtime Environment of version 8 or higher is required to start the KeY versions linked on this page. If a file won’t load, please check that there has not been an absolute directory path accidentally left over (.key and .proof files are plain text files, just open them with an editor if there is a problem). If you have questions regarding or problems with running KeY or loading the provided examples, please feel free to contact “steinhoefel (a-t) cs.tu-darmstadt.de” .

Loop Scope Invariant Rule

Below you find the KeY version including the loop scope invariant rule, as well as the examples mentioned in the paper, once for the old and once for the new rule. When loading an existing .proof (or .key) file, the information about which invariant rule to use is already encoded in the file header. Otherwise, you can switch between the invariant rules by setting the desired value for “Loop treatment” in the “Proof Search Strategy” tab of KeY. Please use the corresponding KeY versions when loading .proof files for the examples with the old and the new rule. KeY version with the Loop Scope Invariant Rule KeY version with the old invariant rule KeY input files for the new rule KeY input files for the old rule The archives with example files may contain more files than actually referenced in the paper. The .proof files relevant for the paper are:

/heap/block_contracts/Simple__unnecessaryLoopInvariant.key.proof
/heap/coincidence_count/project.key.proof
/heap/comprehensions/bprodSplit.key.proof
/heap/comprehensions/segsum.key.proof
/heap/comprehensions/sum0.key.proof
/heap/comprehensions/sum1.key.proof
/heap/comprehensions/sum2.key.proof
/heap/comprehensions/sum3.key.proof
/heap/fm12_01_LRS/lcp.key.proof
/heap/javacard/arrayFillNonAtomic.key.proof
/heap/list/ArrayList_concatenate.key.proof
/heap/list/ArrayList_contains_dep.key.proof
/heap/list/ArrayList_enlarge.key.proof
/heap/list_ghost/ArrayList_enlarge.key.proof
/heap/list/LinkedList_get_normal.key.proof
/heap/list_recursiveSpec/ListOperationsNonNull_getNextNN_normal_behavior.key.proof
/heap/list_recursiveSpec/ListOperationsNonNull_setValueAt_normal_behavior.key.proof
/heap/list_seq/ArrayList.contains.key.proof
/heap/list_seq/ArrayList.enlarge.key.proof
/heap/list_seq/ArrayList.remove.0.key.proof
/heap/list_seq/ArrayList.remove.1.key.proof
/heap/observer/ExampleSubject_addObserver.key.proof
/heap/permissions/permissions_method3.key.proof
/heap/removeDups/arrayPart.key.proof
/heap/removeDups/contains.key.proof
/heap/removeDups/removeDup.key.proof
/heap/saddleback_search/Saddleback_search.key.proof
/heap/SemanticSlicing/project.key.proof
/heap/simple/loop2.key.proof
/heap/simple/oldForParams.key.proof
/heap/simple/selection_sort.key.proof
/heap/SmansEtAl/ArrayList_add.key.proof
/heap/vacid0_01_SparseArray/MemoryAllocator_alloc.key.proof
/heap/vacid0_01_SparseArray/MemoryAllocator_alloc_unsigned.key.proof
/heap/vstte10_01_SumAndMax/SumAndMax_sumAndMax.key.proof
/heap/vstte10_03_LinkedList/Node_search.key.proof
/heap/vstte10_04_Queens/Queens_isConsistent.key.proof
/heap/WeideEtAl_01_AddAndMultiply/AddAndMultiply_add.key.proof
/heap/WeideEtAl_02_BinarySearch/BinarySearch_search.key.proof
/newBook/09.list_modelfield/ArrayList.add.key.proof
/newBook/09.list_modelfield/ArrayList.remFirst.key.proof
/standard_key/arith/cubicSum.key.proof
/standard_key/arith/euclidean/gcdHelp-post.key.proof
/standard_key/arith/gemplusDecimal/add.key.proof
/standard_key/java_dl/arrayMax.key.proof
/standard_key/java_dl/java5/for_Array.key.proof
/standard_key/java_dl/java5/for_Iterable.key.proof
/standard_key/java_dl/java5/for_ReferenceArray.key.proof
/standard_key/java_dl/jml-free/loopInvFree.key.proof
/standard_key/java_dl/jml-information-flow.key.proof
/standard_key/java_dl/polishFlagSort.key.proof
/standard_key/java_dl/reverseArray2.key.proof
/standard_key/java_dl/reverseArray.key.proof

For the manually improved outlier proofs discussed in the paper, the additionally relevant files are /heap/coincidence_count/project.key.manually-optimized.proof (in the archive with files for the new rule) and ./standard_key/java_dl/jml-information-flow.key.manually-improved.proof (in the archive for the old rule).

State Merging in Loops

Below you find the KeY version which additionally includes an (experimental) implementation of the discussed state merging approach for loops. There is a “Taclet Option” for setting this technique on or off; it’s accessible by “Options” > “Taclet Options” > “mergeAfterLoopScope”. When loading an existing .key or .proof file, the option is set according to the specification in the file. The examples contain several .key files for starting from scratch with the “partially unrolled find” method discussed in the paper based on different settinsg, as well as finished .proof files. KeY version for state merging in loops KeY input files for state merging