repairing proof for Tree.classify

KeYProject · Dec 28, 2023 · ef7ca71 · ef7ca71
1 parent 4cf5d85
commit ef7ca71
Show file tree

Hide file tree

Showing 3 changed files with 14,580 additions and 12,810 deletions.
diff --git a/contract-order.txt b/contract-order.txt
@@ -9,6 +9,12 @@ de.wiesler.Buffers[de.wiesler.Buffers::align_to_next_block(int)].JML normal_beha
 de.wiesler.Buffers[de.wiesler.Buffers::blockAligned(int)].JML model_behavior operation contract.0
 
 # constructors here just to be safe that they don't use contracts proven in the final heap
+de.wiesler.Tree[de.wiesler.Tree::piLemmaUpperBound(int)].JML model_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::piInRangeLower(int,int)].JML model_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::piInRangeUpper(int,int)].JML model_behavior operation contract.0
+
+de.wiesler.Tree[de.wiesler.Tree::build([I)].JML normal_behavior operation contract.0
+
 de.wiesler.Tree[de.wiesler.Tree::Tree([I,[I,int)].JML normal_behavior operation contract.0
 de.wiesler.Tree[de.wiesler.Tree::build(int,[I,int,int)].JML normal_behavior operation contract.0
 
@@ -30,6 +36,21 @@ de.wiesler.Functions[de.wiesler.Functions::isSortedSlice([I,int,int)].JML model_
 de.wiesler.Functions[de.wiesler.Functions::isSortedSliceTransitive([I,int,int)].JML model_behavior operation contract.0
 de.wiesler.Functions[de.wiesler.Functions::isValidBucketStarts([I,int)].JML model_behavior operation contract.0
 
+de.wiesler.Tree[de.wiesler.Tree::binarySearchInvariant(int,int,int)].JML model_behavior operation contract.0
+
+de.wiesler.Tree[de.wiesler.Tree::binarySearchInvariant(int,int,int)].JML accessible clause.0
+
+de.wiesler.Tree[de.wiesler.Tree::piOf1(int)].JML model_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::piLemmaLeft(int, int)].JML model_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::piLemmaRight(int, int)].JML model_behavior operation contract.0
+
+de.wiesler.Tree[de.wiesler.Tree::piLemma(int, int)].JML model_behavior operation contract.0
+
+de.wiesler.Tree[de.wiesler.Tree::treeSearchInvariantLemmaImpl(int,int,int,int,int)].JML normal_behavior operation contract.0
+
+de.wiesler.Tree[de.wiesler.Tree::treeSearchInvariantLemma(int,int,int,int,int)].JML model_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::binarySearchInvariantLemma(int,int,int,int)].JML model_behavior operation contract.0
+
 de.wiesler.Tree[de.wiesler.Tree::classOfFirstSplitters()].JML model_behavior operation contract.0
 de.wiesler.Tree[de.wiesler.Tree::isClassifiedAs(int,int)].JML model_behavior operation contract.0
 

diff --git a/src/main/java-overflow/de/wiesler/Tree.java b/src/main/java-overflow/de/wiesler/Tree.java
@@ -25,19 +25,19 @@ public final class Tree {
       @ requires_free (1 << log_buckets) <= tree.length;
       @ requires_free \disjoint(sorted_splitters[*], tree[*]);
       @
-      @ ensures_free this.log_buckets == log_buckets;
-      @ ensures_free this.tree == tree;
-      @ ensures_free this.sorted_splitters == sorted_splitters;
+      @ ensures this.log_buckets == log_buckets;
+      @ ensures this.tree == tree;
+      @ ensures this.sorted_splitters == sorted_splitters;
       @
-      @ assignable_free tree[*];
+      @ assignable tree[*];
       @*/
     public Tree(int[] sorted_splitters, int[] tree, int log_buckets) {
         //@ set num_buckets = 1 << log_buckets;
         //@ set this.sorted_splitters = sorted_splitters;
         final int num_buckets = 1 << log_buckets;
         final int num_splitters = num_buckets - 1;
 
-        //@ assume 2 <= num_buckets <= tree.length;
+        //@ assert 2 <= num_buckets <= tree.length;
 
         this.log_buckets = log_buckets;
         this.tree = tree;
@@ -280,9 +280,9 @@ boolean treeSearchInvariantLemmaImpl(int b, int l, int b_bin, int d_bin, int val
 
     /*@ normal_behaviour
       @ requires_free \dl_inInt(value);
-      @ ensures_free this.num_buckets <= \result < 2 * this.num_buckets;
+      @ ensures this.num_buckets <= \result < 2 * this.num_buckets;
       @
-      @ ensures_free this.isClassifiedAs(value, \result - this.num_buckets);
+      @ ensures this.isClassifiedAs(value, \result - this.num_buckets);
       @
       @ // Needed to bring this method to logic
       @ ensures_free \result == this.classify(value);
@@ -336,11 +336,11 @@ int classify(int value) {
       @ requires_free indices.length == end - begin;
       @ requires_free \disjoint(values[*], indices[*], this.tree[*], this.sorted_splitters[*]);
       @
-      @ ensures_free (\forall int i; 0 <= i < indices.length; this.num_buckets <= indices[i] < 2 * this.num_buckets);
+      @ ensures (\forall int i; 0 <= i < indices.length; this.num_buckets <= indices[i] < 2 * this.num_buckets);
       @ // Needed to bring this method to logic
-      @ ensures_free (\forall int i; 0 <= i < indices.length; indices[i] == this.classify(values[begin + i]));
+      @ ensures (\forall int i; 0 <= i < indices.length; indices[i] == this.classify(values[begin + i]));
       @
-      @ assignable_free indices[*];
+      @ assignable indices[*];
       @*/
     void classify_all(int[] values, int begin, int end, int[] indices) {
         Functions.fill(indices, 0, indices.length, 1);