Finalising exercise 6

05-control-flow/README.md

@@ -108,7 +108,7 @@ claim
    </k>
    <store> STORE => STORE [ $a <- A ] [ $b <- B ] [ $c <- ?C:Int ] </store>
    ensures A <=Int ?C andBool
-            B <=Int ?C
+           B <=Int ?C
 ```
 
 introduces two symbolic integers, `A` and `B`, and states that after the execution of the given program, the store will have been updated so that the value of `$a` equals `A`, the value of `$b` equals `B`, and the value of `$c` equals *some* symbolic integer `?C` such that `A <= C` and `B <= C`. More precisely, for symbolic variables, the notation `?` denotes *existential quantification*, whereas the absence of `?` (for example, the way `A` and `B` are introduced) denotes *universal quantification*. The `ensures` clause corresponds to a post-condition of sorts, stating conditions that must hold after the execution. The last claim states precisely what the value of `?C` is, replacing it with the function `maxInt(A, B)`, defined in the `VERIFICATION` module as the greater of the two parameters.

06-procedures/README.md

@@ -85,4 +85,42 @@ Follow the instructions from the top-level [`README`](../README.md) file to comp
 
 ## Proving program properties
 
-TODO
+For this exercise, we re-use the `while` loop from the [previous exercise](../05-control-flow/README.md), together with its specification, wrap it in a function, then call that function and reason about the obtained result. Using slightly different identifiers and symbolic variables, the specification of the `while` loop is as follows:
+
+```
+claim 
+   <k> 
+      while ( 0 < NID ) {
+         SID = SID + NID ;
+          NID = NID - 1 ;
+      }
+   => . ... </k>
+   <store> 
+      SID |-> (S:Int => S +Int ((N +Int 1) *Int N /Int 2))
+      NID |-> (N:Int => 0)
+   </store>
+requires N >=Int 0
+```
+
+and the main program, together with its specification, is as follows:
+
+```
+claim 
+   <k> 
+      def $sum($n, .Ids) {
+         $s = 0 ;
+         while (0 < $n) {
+            $s = $s + $n ;
+            $n = $n - 1 ;
+         }
+         return $s ;
+      }
+      $n := $sum(N:Int, .Ints) ;
+   => . ... </k>
+   <funcs> .Map => ?_ </funcs>
+   <store> $n |-> (_ => ((N +Int 1) *Int N /Int 2)) </store>
+   <stack> .List </stack>
+   requires N >=Int 0
+```
+
+The specification states that this program, which consists of declaring a function `$sum` and then calling it with a non-negative symbolic integer `N`, ends up storing the sum of first `N` integers in the variable `$n`.

tests/06-procedures/sum-spec.k

@@ -28,26 +28,26 @@ module SUM-SPEC
               }
            => . ... </k>
           <store> SID |-> (S:Int => S +Int ((N +Int 1) *Int N /Int 2))
-                NID |-> (N:Int => 0)
+                  NID |-> (N:Int => 0)
           </store>
       requires N >=Int 0
-       andBool S >=Int 0
-
-    claim <k> def $sum($n, .Ids) {
-                $s = 0 ;
-                while (0 < $n) {
-                  $s = $s + $n ;
-                  $n = $n - 1 ;
-                }
-                return $s ;
-              }
-              return $sum(N:Int, .Ints) ;
-           => return (N +Int 1) *Int N /Int 2 ;
-          </k>
-          <funcs> .Map => ?_ </funcs>
-          <store> .Map => ?_ </store>
-          <stack> .List </stack>
-      requires N >=Int 0
+
+claim 
+   <k> 
+      def $sum($n, .Ids) {
+         $s = 0 ;
+         while (0 < $n) {
+            $s = $s + $n ;
+            $n = $n - 1 ;
+         }
+         return $s ;
+      }
+      $n = $sum(N:Int, .Ints) ;
+   => . ... </k>
+   <funcs> .Map => ?_ </funcs>
+   <store> $n |-> (_ => ((N +Int 1) *Int N /Int 2)) </store>
+   <stack> .List </stack>
+   requires N >=Int 0
 
 endmodule