finished the specification for sort.

It was rather broken until now.
KeYProject · Jun 15, 2024 · a177cb7 · a177cb7
1 parent a2a7d54
commit a177cb7
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 17 deletions.
diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
@@ -82,28 +82,30 @@ private int binSearch(int v) {
 
     /*@ public normal_behaviour
       @  ensures \dl_seqPerm(\old(seq), seq);
-      @  ensures  (\forall int x; (\forall int y; 0<=x<y<seq.length; (\bigint)seq[x] <= (\bigint)seq[y]));
+      @  ensures  (\forall int x,y; 0<=x<y<seq.length-1; (\bigint)seq[x] <= (\bigint)seq[y]);
       @  assignable footprint;
       @*/
     public void sort() {
 
-        /*@ loop_invariant 0 <= i <= size-1;
-          @ loop_invariant (\forall int k; 0<=k<i; array[k] <= array[k+1]);
-          @ loop_invariant (\forall int l; i<=l<size; array[i] <= array[l]);
+        /*@ loop_invariant 0 <= i <= size;
+          @ loop_invariant (\forall int k,l; 0<=k<l<i; array[k] <= array[l]);
+          @ loop_invariant i > 0 ==> (\forall int m; i<=m<size; array[i-1] <= array[m]);
           @ loop_invariant \dl_seqPerm(\old(seq), seq);
           @ loop_invariant \invariant_for(this);
-          @ assignable array[*];
+          @ assignable array[*], seq;
           @ decreases size - i;
           @*/
         for(int i = 0; i < size-1; i++) {
-            int min = i+1;
-            /*@ loop_invariant i+2 <= j <= size;
-              @ loop_invariant i+2 <= min < j;
-              @ loop_invariant (\forall int x; i+1<=x<j; array[x] <= array[min]);
+            int min = i;
+            /*@ loop_invariant size > 0;
+              @ loop_invariant i < j <= size;
+              @ loop_invariant i <= min < j;
+              @ loop_invariant (\forall int x; i<=x<j; array[min] <= array[x]);
+              @ loop_invariant \dl_seqPerm(\old(seq), seq);
               @ assignable \strictly_nothing;
-              @ decreases size - i;
+              @ decreases size - j;
               @*/
-            for(int j = i+2; j < size; j++) {
+            for(int j = i+1; j < size; j++) {
                 if(array[j] < array[min]) {
                     min = j;
                 }

diff --git a/README.md b/README.md
@@ -45,11 +45,12 @@ This artifact is monitored by continous integration pipeline.
 Deadline: next kakey meeting, 21.06.2024
 
 * MU:
-  * Add link to the FM tutorial webpage
-  * Description of the both case studies. 
-  * Interactive use
-  * Beweis von sort()
-  * Beweis von List::add()
+  * Readme
+    * Add link to the FM tutorial webpage
+    * Description of the both case studies.
+    * Interactive use
+  * DONE: Beweis von sort()
+  * DONE: Beweis von List::add():
 
 * AW: 
   * Zenodo DOI
@@ -58,7 +59,7 @@ Deadline: next kakey meeting, 21.06.2024
   * 
 
 * RB: 
-  * tentative screencast on the FM tutoral web page.  
+  * tentative screencast on the FM tutoral web page.
   * Beweis von List::add()
 
 * WP: