Merge pull request #53 from rems-project/mdd/write-example-cleanup

Example cleanup: remove redundant instantiate, add stronger post to write_5 example
rems-project · Jul 22, 2024 · 1fc7c0a · 1fc7c0a
2 parents 813d5a0 + c7aa17b
commit 1fc7c0a
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/src/example-archive/dafny-tutorial/working/linear_search.c b/src/example-archive/dafny-tutorial/working/linear_search.c
@@ -26,7 +26,6 @@ int linear_search(int *a, int length, int key)
         each (i32 j; 0i32 <= j && j < idx) {IndexPre[j] != key}; @*/
   {
     /*@ extract Owned<int>, idx; @*/
-    /*@ instantiate good<int>, idx;  @*/
     if (*(a + idx) == key)
     {
       return idx;

diff --git a/src/example-archive/simple-examples/working/write_5.c b/src/example-archive/simple-examples/working/write_5.c
@@ -6,7 +6,9 @@ void write_5(int *pair)
       take Cell2Pre = Owned(pair + 1i32); @*/
 /*@ ensures 
       take Cell1Post = Owned(pair);
-      take Cell2Post = Owned(pair + 1i32); @*/
+      take Cell2Post = Owned(pair + 1i32); 
+      Cell1Post == 7i32; 
+      Cell2Post == 8i32; @*/
 {
   pair[0] = 7;
   pair[1] = 8;
@@ -18,7 +20,10 @@ void write_5_alt(int *pair)
 /*@ requires 
       take PairPre = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; @*/
 /*@ ensures 
-      take PairPost = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; @*/
+      take PairPost = each (i32 j; j == 0i32 || j == 1i32) {Owned(pair + j)}; 
+      PairPost[0i32] == 7i32; 
+      PairPost[1i32] == 8i32; 
+      @*/
 {
   /*@ extract Owned<int>, 0i32; @*/
   pair[0] = 7;