# Notes on Structured Programming – Section 5, Remark 3

Here is a Dafny proof of the “exercise for the reader” from section 5 of E.W.Dijkstra’s “Notes on Structured Programming” monograph in the book “Structured Programming (1972)”.

```method Section5RemarkThree(A:int, B:int) returns (z:int) requires A > 0 requires B >= 0 ensures z == power(A,B) { var x := A; var y := B; z := 1;   while y != 0 invariant x > 0 invariant y >= 0 invariant power(A, B) == z * power(x, y) { halfExponentSquareBase(x, if odd(y) then y-1 else y);   if odd(y) { y := y - 1; z := z * x; } y := y/2; x := x * x; } }   lemma halfExponentSquareBase(x:int,y:int) requires x > 0 requires y >= 0 requires even(y) ensures power(x, y) == power(x*x, y/2) { if y != 0 { halfExponentSquareBase(x,y-2); } }   predicate method even(n: nat) ensures even(n) <==> n % 2 == 0 { if n == 0 then true else odd(n-1) }   predicate method odd(n: nat) ensures odd(n) <==> n % 2 != 0 { if n == 0 then false else even(n-1) }   function power(x:int, n:int):int { if n <= 0 then 1 else x * power(x, n-1) }```

# Dafny Matrix Mutiplication

So, I spent quite a while helping someone on stackoverflow prove the correctness of a matrix multiplication algorithm. Once we got to a point where they were happy with it and thanked me, then they deleted their question. I take this, and the fact that in hindsight their understanding did not seem to match up with the code they had, to mean that they were cheating on some university coursework. It took me quite a lot of effort to write the answer, and I wasn’t doing it primarily to help them specificaly, I was doing it to help Dafny become more popular. By which I mean: it was only worth the effort of writing such a detailed answer if the answer can help many other people.

Unfortunately, I don’t have a copy of the answer I wrote. But I do I have a copy of all the code. So here it is. If you are a lecturer and this is your coursework question then I can be contacted on the “about” page.

First the question:

http://rise4fun.com/Dafny/Bztr

```method Main() { var m1: array2<int>, m2: array2<int>, m3: array2<int>; m1 := new int[2,3]; m2 := new int[3,1]; m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3; m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6; m2[0,0] := 7; m2[1,0] := 8; m2[2,0] := 9; m3 := Multiply'(m1, m2); PrintMatrix(m1); print "\n*\n"; PrintMatrix(m2); print "\n=\n"; PrintMatrix(m3); }   method PrintMatrix(m: array2<int>) requires m != null { var i: nat := 0; while (i < m.Length0) { var j: nat := 0; print "\n"; while (j < m.Length1) { print m[i,j]; print "\t"; j := j + 1; } i := i + 1; } print "\n"; } predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>) { // m3 is the result of multiplying the matrix m1 by the matrix m2 m1 != null && m2 != null && m3 != null && m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 && forall i,j :: 0 <= i < m3.Length0 && 0 <= j < m3.Length1 ==> m3[i,j] == RowColumnProduct(m1,m2,i,j) }   function RowColumnProduct(m1: array2<int>, m2: array2<int>, row: nat, column: nat): int requires m1 != null && m2 != null && m1.Length1 == m2.Length0 requires row < m1.Length0 && column < m2.Length1 { RowColumnProductFrom(m1, m2, row, column, 0) }   function RowColumnProductFrom(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat): int requires m1 != null && m2 != null && k <= m1.Length1 == m2.Length0 requires row < m1.Length0 && column < m2.Length1 decreases m1.Length1 - k { if k == m1.Length1 then 0 else m1[row,k]*m2[k,column] + RowColumnProductFrom(m1, m2, row, column, k+1) }   function RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat,i:nat): int requires m1 != null && m2 != null && k <= m1.Length1 == m2.Length0 requires row < m1.Length0 && column < m2.Length1 && i < m1.Length1 == m2.Length0 requires k<=i decreases i - k { if k == i then 0 else m1[row,k]*m2[k,column] + RowColumnProductTo(m1, m2, row, column, k+1,i) }   predicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat) { // m3 is the result of multiplying the matrix m1 by the matrix m2 m1 != null && m2 != null && m3 != null && m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 && row <= m1.Length0 && col <= m2.Length1 && forall i,j :: 0 <= i < row && 0 <= j < col ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)   }   predicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat) { // m3 is the result of multiplying the matrix m1 by the matrix m2 m1 != null && m2 != null && m3 != null && m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 && row <= m1.Length0 && col <= m2.Length1 && forall i,j :: 0 <= i < row && 0 <= j < col ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)   } predicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,i:nat) { // m3 is the result of multiplying the matrix m1 by the matrix m2 m1 != null && m2 != null && m3 != null && m1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 && row < m1.Length0 && col < m2.Length1 && 0<=i<m1.Length1 && forall n,j :: 0 <= n < row && 0 <= j < col ==> m3[n,j] == RowColumnProduct(m1,m2,n,j) && m3[row,col] == RowColumnProductTo(m1, m2, row, col ,0,i) }   method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>) requires m1 != null && m2 != null requires m1.Length1 > 0 && m2.Length0 > 0 requires m1.Length1 == m2.Length0 ensures MM(m1, m2, m3) { m3 := new int[m1.Length0, m2.Length1]; var row:nat := 0; var col:nat := 0; var i:nat := 0;   while(row != m1.Length0) invariant MMROW(m1, m2, m3,row, col) invariant (0<=row<= m1.Length0) decreases m1.Length0 - row { while(col != m2.Length1) invariant MMCOL(m1, m2, m3,row, col) invariant (0<=col<= m2.Length1) decreases m2.Length1 - col { while(i != m1.Length1) invariant MMI(m1, m2, m3,row, col,i) invariant (i<= m1.Length1==m2.Length0)&&(0<=col<= m2.Length1)&&(0<=row<= m1.Length0) decreases m1.Length1 - i { m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]); i := i+1; } col := col+1; i := 0; } row := row+1; col:= 0; } }```

Now several different solutions.

The questioners insisted that I not change their definition of the main MM predicate, even though the direction of recursion in the predicate is opposite to the direction of recursion in the while loop. The proof strategy I showed them was to define a new predicate that did recurse in he same direction as the while loop, and then prove the equivalence of the two predicates.

http://rise4fun.com/Dafny/noVy

```method Main() { var m1: array2<int>, m2: array2<int>, m3: array2<int>; m1 := new int[2,3]; m2 := new int[3,1]; m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3; m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6; m2[0,0] := 7; m2[1,0] := 8; m2[2,0] := 9; m3 := Multiply'(m1, m2); PrintMatrix(m1); print "\n*\n"; PrintMatrix(m2); print "\n=\n"; PrintMatrix(m3); }   method PrintMatrix(m: array2<int>) requires m != null { var i: nat := 0; while (i < m.Length0) { var j: nat := 0; print "\n"; while (j < m.Length1) { print m[i,j]; print "\t"; j := j + 1; } i := i + 1; } print "\n"; }   predicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) { m1 != null && m2 != null && m1.Length1 == m2.Length0 }   predicate AllowedToMultiplyInto(m1: array2<int>, m2: array2<int>, m3: array2<int>) { AllowedToMultiply(m1,m2) && m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 }   predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>) { // m3 is the result of multiplying the matrix m1 by the matrix m2 AllowedToMultiplyInto(m1,m2,m3) && forall i,j :: 0 <= i < m3.Length0 && 0 <= j < m3.Length1 ==> m3[i,j] == RowColumnProduct(m1,m2,i,j) }   function RowColumnProduct(m1: array2<int>, m2: array2<int>, row: nat, column: nat): int requires AllowedToMultiply(m1,m2) requires row < m1.Length0 && column < m2.Length1 { RowColumnProductFrom(m1, m2, row, column, 0) }   function RowColumnProductFrom(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat): int requires AllowedToMultiply(m1,m2) requires row < m1.Length0 && column < m2.Length1 requires k <= m1.Length1 decreases m1.Length1 - k { if k == m1.Length1 then 0 else m1[row,k]*m2[k,column] + RowColumnProductFrom(m1, m2, row, column, k+1) }   function RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat,i:nat): int requires AllowedToMultiply(m1,m2) requires row < m1.Length0 && column < m2.Length1 && i < m1.Length1 == m2.Length0 requires k<=i decreases i - k { if k == i then 0 else m1[row,k]*m2[k,column] + RowColumnProductTo(m1, m2, row, column, k+1,i) }   function RowColumnProductForCount(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int requires AllowedToMultiply(m1, m2) requires row < m1.Length0 && column < m2.Length1 && n <= m1.Length1 { if n == 0 then 0 else RowColumnProductForCount(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] }   predicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>, rown:nat) requires AllowedToMultiplyInto(m1, m2, m3) requires rown <= m1.Length0 { forall r:nat,c:nat :: r < rown && c < m2.Length1 ==> m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1) }   predicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,coln:nat) requires AllowedToMultiplyInto(m1, m2, m3) requires row < m1.Length0 && coln <= m2.Length1 { forall c:nat :: c < coln ==> m3[row,c] == RowColumnProductForCount(m1,m2,row,c,m1.Length1) }   predicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,n:nat) requires AllowedToMultiplyInto(m1, m2, m3) requires row < m1.Length0 && col < m2.Length1 && n<=m1.Length1 { m3[row,col] == RowColumnProductForCount(m1, m2, row, col, n) }   method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>) requires AllowedToMultiply(m1, m2) ensures MM(m1, m2, m3) { m3 := new int[m1.Length0, m2.Length1];   var row:nat := 0; // loop over rows of m1 while(row < m1.Length0) invariant row <= m1.Length0 invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn) modifies m3 { assert MMROW(m1, m2, m3, row); // loop over coloums of m2 var col:nat := 0; while(col < m2.Length1) invariant col <= m2.Length1 invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn) invariant forall n:nat :: n <= col ==> MMCOL(m1, m2, m3,row, n) { assert MMCOL(m1, m2, m3, row, col); // // loop over elements of m1 row / m2 column var i:nat := 0; m3[row,col] := 0; while(i < m1.Length1) invariant i <= m1.Length1 invariant forall rn:nat :: rn < row ==> MMROW(m1, m2, m3, rn) invariant forall c:nat :: c < col ==> MMCOL(m1, m2, m3, row, c) invariant forall j:nat :: j <= i ==> MMI(m1, m2, m3, row, col, j) { assert MMI(m1, m2, m3, row, col, i);   m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]); i := i+1;   assert MMI(m1, m2, m3, row, col, i); } assert MMI(m1, m2, m3, row, col, m1.Length1); assert m3[row,col] == RowColumnProductForCount(m1,m2,row,col,m1.Length1); col := col+1; assert MMCOL(m1, m2, m3, row, col); } assert MMCOL(m1, m2, m3, row, m2.Length1); row := row+1; assert MMROW(m1, m2, m3, row); } assert MMROW(m1, m2, m3, m1.Length0); MMROWImpliesMM(m1, m2, m3); }   lemma MMROWImpliesMM(m1: array2<int>, m2: array2<int>, m3: array2<int>) requires AllowedToMultiplyInto(m1,m2,m3) requires MMROW(m1, m2, m3, m1.Length0) ensures MM(m1, m2, m3) { assert forall r:nat,c:nat :: r < m1.Length0 && c < m2.Length1 ==> m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1);   forall r:nat,c:nat | r < m1.Length0 && c < m2.Length1 ensures m3[r,c] == RowColumnProduct(m1,m2,r,c) { assert m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1); RowColumnProductForCountImpliesRowColumnProduct(m1, m2, m3, r, c); }   assert forall r:nat,c:nat :: r < m3.Length0 && c < m3.Length1 ==> m3[r,c] == RowColumnProduct(m1,m2,r,c); }   lemma RowColumnProductForCountImpliesRowColumnProduct(m1: array2<int>, m2: array2<int>, m3: array2<int>, r:nat, c:nat) requires AllowedToMultiplyInto(m1,m2,m3) requires r < m1.Length0 && c < m2.Length1; requires m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1) ensures m3[r,c] == RowColumnProduct(m1,m2,r,c) { assert RowColumnProduct(m1,m2,r,c) == RowColumnProductFrom(m1,m2,r,c,0);   var i:nat := 0; var total := RowColumnProductForCount(m1,m2,r,c,m1.Length1); while i < m1.Length1 invariant i <= m1.Length1 invariant total == RowColumnProductForCount(m1,m2,r,c,m1.Length1-i) + RowColumnProductFrom(m1,m2,r,c,m1.Length1-i) { i := i+1; } }```

I suggested an alternative strategy which uses Dafny’s forall statement to implement the matrix multiplication. Since this is not a loop it does not require any invariants to be given in order to verify. This is the best solution if you are just trying to get a matrix multiply working.

http://rise4fun.com/Dafny/mgoeu

```method Main() { var m1: array2<int>, m2: array2<int>, m3: array2<int>; m1 := new int[2,3]; m2 := new int[3,1]; m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3; m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6; m2[0,0] := 7; m2[1,0] := 8; m2[2,0] := 9; m3 := Multiply'(m1, m2); PrintMatrix(m1); print "\n*\n"; PrintMatrix(m2); print "\n=\n"; PrintMatrix(m3); }   method PrintMatrix(m: array2<int>) requires m != null { var i: nat := 0; while (i < m.Length0) { var j: nat := 0; print "\n"; while (j < m.Length1) { print m[i,j]; print "\t"; j := j + 1; } i := i + 1; } print "\n"; }   predicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) { m1 != null && m2 != null && m1.Length1 == m2.Length0 }   predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>) requires AllowedToMultiply(m1, m2) { // m3 is the result of multiplying the matrix m1 by the matrix m2 m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 && forall r:nat,c:nat :: r < m3.Length0 && c < m3.Length1 ==> m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) }   function method RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int requires AllowedToMultiply(m1, m2) requires row < m1.Length0 && column < m2.Length1 && n <= m1.Length1 { if n == 0 then 0 else RowColumnProductTo(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] }   method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>) requires AllowedToMultiply(m1, m2) ensures MM(m1, m2, m3) { m3 := new int[m1.Length0, m2.Length1];   forall r:nat,c:nat | r < m3.Length0 && c < m3.Length1 { m3[r,c] := RowColumnProductTo(m1,m2,r,c,m1.Length1); } }```

In this version I take the approach of changing the definition of the MM predicate to work in the same direction as the iteration. If you don’t want to go down the route of using the forall statement, then in my opinion it is usually most productive if you get your recursive and iterative definitions to bracket the same way. For example, have them both do `((((a+b)+c)+d)+e)`, don’t have one of the do `(a+(b+(c+(d+e))))`.

```method Main() { var m1: array2<int>, m2: array2<int>, m3: array2<int>; m1 := new int[2,3]; m2 := new int[3,1]; m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3; m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6; m2[0,0] := 7; m2[1,0] := 8; m2[2,0] := 9; m3 := Multiply'(m1, m2); PrintMatrix(m1); print "\n*\n"; PrintMatrix(m2); print "\n=\n"; PrintMatrix(m3); }   method PrintMatrix(m: array2<int>) requires m != null { var i: nat := 0; while (i < m.Length0) { var j: nat := 0; print "\n"; while (j < m.Length1) { print m[i,j]; print "\t"; j := j + 1; } i := i + 1; } print "\n"; }   predicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) { m1 != null && m2 != null && m1.Length1 == m2.Length0 }   predicate AllowedToMultiplyInto(m1: array2<int>, m2: array2<int>, m3: array2<int>) { AllowedToMultiply(m1,m2) && m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 }   predicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>) requires AllowedToMultiply(m1, m2) { // m3 is the result of multiplying the matrix m1 by the matrix m2 m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 && forall r:nat,c:nat :: r < m3.Length0 && c < m3.Length1 ==> m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) }   function RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int requires AllowedToMultiply(m1, m2) requires row < m1.Length0 && column < m2.Length1 && n <= m1.Length1 { if n == 0 then 0 else RowColumnProductTo(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] }   predicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>, rown:nat) requires AllowedToMultiplyInto(m1, m2, m3) requires rown <= m1.Length0 { forall r:nat,c:nat :: r < rown && c < m2.Length1 ==> m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) }   predicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,coln:nat) requires AllowedToMultiplyInto(m1, m2, m3) requires row < m1.Length0 && coln <= m2.Length1 { forall c:nat :: c < coln ==> m3[row,c] == RowColumnProductTo(m1,m2,row,c,m1.Length1) }   predicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,n:nat) requires AllowedToMultiplyInto(m1, m2, m3) requires row < m1.Length0 && col < m2.Length1 && n<=m1.Length1 { m3[row,col] == RowColumnProductTo(m1, m2, row, col, n) }   method Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>) requires AllowedToMultiply(m1, m2) ensures MM(m1, m2, m3) { m3 := new int[m1.Length0, m2.Length1];   var row:nat := 0; // loop over rows of m1 while(row < m1.Length0) invariant row <= m1.Length0 invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn) modifies m3 { assert MMROW(m1, m2, m3, row); // loop over coloums of m2 var col:nat := 0; while(col < m2.Length1) invariant col <= m2.Length1 invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn) invariant forall n:nat :: n <= col ==> MMCOL(m1, m2, m3,row, n) { assert MMCOL(m1, m2, m3, row, col); // // loop over elements of m1 row / m2 column var i:nat := 0; m3[row,col] := 0; while(i < m1.Length1) invariant i <= m1.Length1 invariant forall rn:nat :: rn < row ==> MMROW(m1, m2, m3, rn) invariant forall c:nat :: c < col ==> MMCOL(m1, m2, m3, row, c) invariant forall j:nat :: j <= i ==> MMI(m1, m2, m3, row, col, j) { assert MMI(m1, m2, m3, row, col, i);   m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]); i := i+1;   assert MMI(m1, m2, m3, row, col, i); } assert MMI(m1, m2, m3, row, col, m1.Length1); assert m3[row,col] == RowColumnProductTo(m1,m2,row,col,m1.Length1); col := col+1; assert MMCOL(m1, m2, m3, row, col); } assert MMCOL(m1, m2, m3, row, m2.Length1); row := row+1; assert MMROW(m1, m2, m3, row); } assert MMROW(m1, m2, m3, m1.Length0); }```

Here are various other intermidiate stages and suggestions. We went through quite a few iterations, because their requirements on what I could and couldn’t change were not intuiative. I now presume that was because they didn’t want to say to me “here is the coursework specification, look it says don’t change that bit”.

In fact, looking in more detail, one of the attempts that they shared with me has this comment in it

`// TODO: continue here, multiplying m1 by m2 placing the result in m3 such that MM(m1, m2, m3) will become true`

Which looks to me just like the kind of thing that I have seen written in many other courseworks. Hmm. Sucks.

# Calculations In Dafny

Here is an example of using `calc` in Dafny.

Notes:

• Instead of using `==`, you can write another relational operator, for example implication `==>`
• I set the `Add` function to opaque, and disabled automatic induction, because otherwise Dafny will prove almost all of these lemmas automatically
• I wrote in the decreases clauses for didactic reasons. I wrote `decreases 0` where there is no recursive call
• I got the idea for this example from this document by Sophia Drossopoulou
```datatype Num = Zero | Succ(pred:Num)   function {:opaque true} Add(x:Num, y:Num) : Num decreases x; { match x { case Zero => y case Succ(z) => Succ(Add(z, y)) } }   lemma {:induction false} ZeroIdentity(x:Num) decreases x; ensures Add(x,Zero) == x { match x { case Zero => calc == { Add(Zero,Zero); {reveal_Add();} Zero; } case Succ(z) => calc == { Add(x,Zero); {reveal_Add();} Succ(Add(z,Zero)); {ZeroIdentity(z);} Succ(z); // definition of Num x; } } }   lemma {:induction false} SuccSymmetry(x:Num, y:Num) decreases 0; ensures Add(Succ(x),y) == Add(x,Succ(y)) { calc == { Add(Succ(x),y); {reveal_Add();} Succ(Add(x,y)); {SuccLemmaFour(x, y);} Add(x,Succ(y)); } }   lemma {:induction false} SuccLemmaFour(x:Num, y:Num) decreases x; ensures Succ(Add(x, y)) == Add(x,Succ(y)); { match x { case Zero => calc == { Succ(Add(Zero, y)); {reveal_Add();} Succ(y); {reveal_Add();} Add(Zero,Succ(y)); } case Succ(z) => calc == { Succ(Add(x, y)); {reveal_Add();} Succ(Succ(Add(z, y))); {SuccLemmaFour(z, y);} Succ(Add(z, Succ(y))); {reveal_Add();} Add(x,Succ(y)); } } }   lemma {:induction false} AddCommutative(x:Num, y:Num) decreases x; ensures Add(x, y) == Add(y, x) { match x { case Zero => calc == { Add(Zero, y); {reveal_Add();} y; {ZeroIdentity(y);} Add(y, Zero); } case Succ(z) => calc == { Add(x, y); {reveal_Add();} Succ(Add(z, y)); {AddCommutative(z, y);} Succ(Add(y, z)); {SuccLemmaFour(y, z);} Add(y,Succ(z)); // definition Num Add(y, x); } } }   lemma {:induction false} AddAssociative(x:Num, y:Num, z:Num) decreases x; ensures Add(Add(x,y),z) == Add(x,Add(y,z)); { match x { case Zero => calc == { Add(Add(Zero,y),z); {reveal_Add();} Add(y,z); {reveal_Add();} Add(Zero,Add(y,z)); } case Succ(w) => calc == { Add(Add(x,y),z); {reveal_Add();} Add(Add(Succ(w),y),z); {SuccSymmetry(w,y);} Add(Add(w,Succ(y)),z); {SuccLemmaFour(w, y);} Add(Succ(Add(w,y)),z); {SuccSymmetry(Add(w,y),z);} Add(Add(w,y),Succ(z)); {SuccLemmaFour(Add(w,y), z);} Succ(Add(Add(w,y),z)); {AddAssociative(w,y,z);} Succ(Add(w,Add(y,z))); {SuccLemmaFour(w, Add(y,z));} Add(w,Succ(Add(y,z))); {SuccSymmetry(w,Add(y,z));} Add(Succ(w),Add(y,z)); {reveal_Add();} Add(x,Add(y,z)); } } }```

The general method in Dafny for proving something by contradiction is:

```lemma X() ensures Q(x) { if !Q(x) { // derive contradiction assert false; } }```

# Dafny Sum and Max solution

A Dafny solution to the Sum and Max verification benchmark. I added some additional specification to verify that the result `max` is really the maximum and the `sum` is really the sum.

```method SumMax(a: array<int>) returns (sum:int, max:int) requires a != null; requires a.Length >= 0; requires forall i :: 0 <= i < a.Length ==> a[i] >= 0; ensures sum <= a.Length*max; ensures forall i :: 0 <= i < a.Length ==> a[i] <= max; ensures a.Length == 0 || (exists i :: 0 <= i < a.Length && a[i] == max); ensures sum == Sum(a); { max := 0; sum := 0;   var idx:int := 0; while idx<a.Length invariant idx <= a.Length; invariant forall i :: 0 <= i < idx ==> a[i] <= max; invariant (idx==0 && max==0) || exists i :: 0 <= i < idx && a[i] == max; invariant sum <= idx*max; invariant sum == Sum'(a, 0, idx); { if (max < a[idx]) { max := a[idx]; } sum := sum + a[idx]; idx := idx + 1; } }   function Sum(a: array<int>) : int reads a; requires a != null; { Sum'(a, 0, a.Length) }   function Sum'(a: array<int>, i:int, j:int) : int reads a; requires a != null; requires 0 <= i <= j <= a.Length; { if j == i then 0 else Sum'(a, i, j-1) + a[j-1] }   lemma SumOfIntervalOneIsElement(a: array<int>, i:int) requires a != null; requires 0 <= i < a.Length; ensures a.Length > 0; ensures Sum'(a, i, i+1) == a[i]; { }   lemma SumOfIntervalIsSumOfSubIntervals (a: array<int>, i:int, j:int, k:int) requires a != null; requires 0 <= i <= j <= k <= a.Length; ensures Sum'(a, i, j) + Sum'(a, j, k) == Sum'(a, i, k); { }```

# Distributivity of Sequence Map over Function Composition in Dafny

Distributivity of Sequence Map over Function Composition in Dafny

```lemma MapDistributivity(xs:seq<int>, f:int->int, g:int->int) requires forall x :: x in xs ==> f.requires(x); requires forall x :: x in xs ==> g.requires(f(x)); ensures forall x :: x in MapSeq(xs,f) ==> g.requires(x); ensures MapSeq(MapSeq(xs,f), g) == MapSeq(xs, Compose(f,g)); { if xs != [] { MapDistributivity(xs[1..], f, g); } }   function Compose(f:int->int, g:int->int) : int->int { x reads f.reads(x) reads if f.requires(x) then g.reads(f(x)) else {} requires f.requires(x) requires g.requires(f(x)) -> g(f(x)) }   function MapSeq(xs:seq<int>, f:int->int) : seq<int> reads MapSeqReads(xs, f); requires forall x :: x in xs ==> f.requires(x); ensures |xs| == |MapSeq(xs,f)|; ensures forall x :: x in xs ==> f(x) in MapSeq(xs,f); { if xs == [] then [] else [f(xs[0])] + MapSeq(xs[1..], f) }   function MapSeqReads(xs:seq<int>, f:int->int) : set<object> reads if |xs| > 0 then f.reads(xs[0]) + MapSeqReads(xs[1..], f) else {}; decreases xs; ensures forall x :: x in xs ==> f.reads(x) <= MapSeqReads(xs,f); { if xs == [] then {} else f.reads(xs[0]) + MapSeqReads(xs[1..],f) }```

# Dafny: Permutations, sequences and multisets

Dafny has support for multisets, which are really useful for reasoning about programs that permute, or otherwise deal with permutations, of sequences or arrays.

```predicate Subpermutation(xs:seq, ys:seq) ensures Subpermutation(xs,ys) ==> forall x :: x in xs ==> x in ys; { assert forall x :: x in xs ==> x in multiset(xs); multiset(xs) <= multiset(ys) }   // THEOREM lemma SubpermutationIsSmaller(xs:seq, ys:seq) requires Subpermutation(xs,ys); ensures |xs| <= |ys|; { assert |multiset(xs)| == |xs|; assert |multiset(ys)| == |ys|;   var xs',ys' := xs,ys;   var XS',YS' := multiset(xs),multiset(ys); var XS'',YS'' := multiset{},multiset{}; while(|XS'|>0) invariant Subpermutation(xs',ys'); invariant XS' == multiset(xs'); invariant YS' == multiset(ys'); invariant XS' + XS'' == multiset(xs); invariant YS' + YS'' == multiset(ys); invariant XS'' == YS''; invariant XS' <= YS'; { assert RemoveFromSequenceReducesMultiSet(xs,multiset(xs),multiset(xs[1..])); var x := xs'[0]; xs' := Remove(x,xs');   ys' := Remove(x,ys');   XS' := XS'[x := XS'[x] - 1]; XS'' := XS''[x := XS''[x] + 1]; YS' := YS'[x := YS'[x] - 1]; YS'' := YS''[x := YS''[x] + 1]; } }   // SUPPORTING DEFINITIONS   // following is a function lemma predicate RemoveFromSequenceReducesMultiSet(xs:seq<T>, XS:multiset<T>, XS':multiset<T>) requires xs != []; requires XS' == multiset(xs[1..]); ensures XS' == multiset(xs)[xs[0] := multiset(xs)[xs[0]] - 1]; ensures RemoveFromSequenceReducesMultiSet(xs,XS,XS'); { assert [xs[0]]+xs[1..] == xs; assert multiset([xs[0]]+xs[1..]) == multiset(xs); true }   function Remove(x:T, xs:seq<T>) :seq<T> requires x in xs; ensures multiset(Remove(x,xs)) == multiset(xs)[x := multiset(xs)[x] - 1]; ensures |Remove(x,xs)|+1 == |xs|; { assert RemoveFromSequenceReducesMultiSet(xs,multiset(xs),multiset(xs[1..])); if xs[0]==x then xs[1..] else [xs[0]] + Remove(x,xs[1..]) }```

# Dafny Triggers

It is possible to write tiggers for particular quantifiers in Dafny programs.

```predicate P(x:int) { true }   lemma ThereIsMoreThanOneInteger(x:int) ensures exists z:int :: z!=x; { // can't prove }   lemma NoReallyThereIsMoreThanOneInteger(x:int) ensures exists z:int {:trigger P(z)} :: z!=x; { assert P(x+1); // can prove }```

# Dafny Function Lemmas

Sometimes it is hard to use a normal Dafny method lemma where you need it. For example, if you want to use a lemma inside a function or in a contract. There is a simple solution.

Given a method lemma:

```static lemma SomethingValid(s:S) requires P(s); ensures Q(s);```

We can produce a function lemma:

```static lemma SomethingValidFn(s:S) requires P(s); ensures Q(s); ensures SomethingValidFn(s); { SomethingValid(s); true }```

# Dafny: Proving forall x :: P(x) ==> Q(x)

The general method in Dafny for proving something of the form `forall x :: P(x) ==> Q(x)` is:

```lemma X() ensures forall x :: P(x) ==> Q(x); { forall x | P(x) ensures Q(x); { // prove Q(x) } }```