{"id":9944,"date":"2016-02-13T11:39:22","date_gmt":"2016-02-13T11:39:22","guid":{"rendered":"http:\/\/www.lexicalscope.com\/blog\/?p=9944"},"modified":"2016-02-28T11:04:47","modified_gmt":"2016-02-28T11:04:47","slug":"dafny-matrix-mutiplication","status":"publish","type":"post","link":"https:\/\/www.lexicalscope.com\/blog\/2016\/02\/13\/dafny-matrix-mutiplication\/","title":{"rendered":"Dafny Matrix Mutiplication"},"content":{"rendered":"<p>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 <a href=\"http:\/\/stackoverflow.com\/questions\/35273222\/verification-of-matrix-multiplication-in-dafny\/35313508?noredirect=1#comment58451891_35313508\">deleted their question<\/a>. 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&#8217;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.<\/p>\n<p>Unfortunately, I don&#8217;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 &#8220;about&#8221; page.<\/p>\n<p>First the question:<\/p>\n<p><a href=\"http:\/\/rise4fun.com\/Dafny\/Bztr\">http:\/\/rise4fun.com\/Dafny\/Bztr<\/a><\/p>\n<pre lang=\"dafny\">\r\nmethod Main()\r\n{\r\n\tvar m1: array2<int>, m2: array2<int>, m3: array2<int>;\r\n\tm1 := new int[2,3];\r\n\tm2 := new int[3,1];\r\n\tm1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;\r\n\tm1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;\r\n\tm2[0,0] := 7;\r\n\tm2[1,0] := 8;\r\n\tm2[2,0] := 9;\r\n\tm3 := Multiply'(m1, m2);\r\n\tPrintMatrix(m1);\r\n\tprint \"\\n*\\n\";\r\n\tPrintMatrix(m2);\r\n\tprint \"\\n=\\n\";\r\n\tPrintMatrix(m3);\r\n}\r\n\r\nmethod PrintMatrix(m: array2<int>)\r\n\trequires m != null\r\n{\r\n\tvar i: nat := 0;\r\n\twhile (i < m.Length0)\r\n\t{\r\n\t\tvar j: nat := 0;\r\n\t\tprint \"\\n\";\r\n\t\twhile (j < m.Length1)\r\n\t\t{\r\n\t\t\tprint m[i,j];\r\n\t\t\tprint \"\\t\";\r\n\t\t\tj := j + 1;\r\n\t\t} \r\n\t\ti := i + 1;\r\n\t} \r\n\tprint \"\\n\";\r\n}\r\npredicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)\r\n{ \/\/ m3 is the result of multiplying the matrix m1 by the matrix m2\r\n\tm1 != null && m2 != null && m3 != null &&\r\n\tm1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&\r\n\tforall i,j :: 0 <= i < m3.Length0 &#038;&#038; 0 <= j < m3.Length1 ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)\r\n}\r\n\r\nfunction RowColumnProduct(m1: array2<int>, m2: array2<int>, row: nat, column: nat): int\r\n\trequires m1 != null && m2 != null && m1.Length1 == m2.Length0\r\n\trequires row < m1.Length0 &#038;&#038; column < m2.Length1 \r\n{\r\n\tRowColumnProductFrom(m1, m2, row, column, 0)\r\n}\r\n\r\nfunction RowColumnProductFrom(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat): int\r\n\trequires m1 != null && m2 != null && k <= m1.Length1 == m2.Length0\r\n\trequires row < m1.Length0 &#038;&#038; column < m2.Length1\r\n\tdecreases m1.Length1 - k\r\n{\r\n\tif k == m1.Length1 then 0 else m1[row,k]*m2[k,column] + RowColumnProductFrom(m1, m2, row, column, k+1)\r\n}\r\n\r\nfunction RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat,i:nat): int\r\n\trequires m1 != null && m2 != null && k <= m1.Length1 == m2.Length0\r\n\trequires row < m1.Length0 &#038;&#038; column < m2.Length1 &#038;&#038; i < m1.Length1 == m2.Length0\r\n  requires k<=i\r\n\tdecreases i - k\r\n{\r\n\tif k == i then 0 else m1[row,k]*m2[k,column] + RowColumnProductTo(m1, m2, row, column, k+1,i)\r\n}\r\n\r\npredicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat)\r\n{ \/\/ m3 is the result of multiplying the matrix m1 by the matrix m2\r\n\tm1 != null && m2 != null && m3 != null &&\r\n\tm1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&\r\n  row <= m1.Length0 &#038;&#038; col <= m2.Length1 &#038;&#038;\r\n\tforall i,j :: 0 <= i < row &#038;&#038; 0 <= j < col ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)\r\n  \r\n}\r\n\r\npredicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat)\r\n{ \/\/ m3 is the result of multiplying the matrix m1 by the matrix m2\r\n\tm1 != null && m2 != null && m3 != null &&\r\n\tm1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&\r\n  row <= m1.Length0 &#038;&#038; col <= m2.Length1 &#038;&#038;\r\n\tforall i,j :: 0 <= i < row &#038;&#038; 0 <= j < col ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)\r\n  \r\n}\r\npredicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,i:nat)\r\n{ \/\/ m3 is the result of multiplying the matrix m1 by the matrix m2\r\n\tm1 != null && m2 != null && m3 != null &&\r\n\tm1.Length1 == m2.Length0 && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 &&\r\n  row < m1.Length0 &#038;&#038; col < m2.Length1 &#038;&#038; 0<=i<m1.Length1 &#038;&#038;\r\n\tforall n,j :: 0 <= n < row &#038;&#038; 0 <= j < col ==> m3[n,j] == RowColumnProduct(m1,m2,n,j)\r\n  && m3[row,col] == RowColumnProductTo(m1, m2, row, col ,0,i)\r\n}\r\n\r\nmethod Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)\r\n\trequires m1 != null && m2 != null\r\n  requires m1.Length1 > 0 && m2.Length0 > 0\r\n\trequires m1.Length1 == m2.Length0\r\n\tensures MM(m1, m2, m3)\r\n{\r\n\tm3 := new int[m1.Length0, m2.Length1];\r\n  var row:nat := 0;\r\n  var col:nat  := 0;\r\n  var i:nat  := 0;\r\n  \r\n  while(row != m1.Length0)\r\n    invariant MMROW(m1, m2, m3,row, col)\r\n    invariant (0<=row<= m1.Length0)\r\n\t\tdecreases m1.Length0 - row\r\n  {\r\n      while(col != m2.Length1)\r\n      invariant MMCOL(m1, m2, m3,row, col)\r\n      invariant (0<=col<= m2.Length1)\r\n  \t\tdecreases m2.Length1 - col\r\n      {\r\n          while(i != m1.Length1)\r\n            invariant MMI(m1, m2, m3,row, col,i)\r\n            invariant (i<= m1.Length1==m2.Length0)&#038;&#038;(0<=col<= m2.Length1)&#038;&#038;(0<=row<= m1.Length0)\r\n    \t\t    decreases m1.Length1 - i\r\n           {   \r\n             m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]);\r\n             i := i+1;\r\n           }\r\n           col := col+1;\r\n           i := 0;\r\n      }\r\n      row := row+1;\r\n      col:= 0;\r\n  }\r\n}\r\n<\/pre>\n<p>Now several different solutions.<\/p>\n<p>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.<\/p>\n<p><a href=\"http:\/\/rise4fun.com\/Dafny\/noVy\">http:\/\/rise4fun.com\/Dafny\/noVy<\/a><\/p>\n<pre lang=\"dafny\">\r\nmethod Main()\r\n{\r\n    var m1: array2<int>, m2: array2<int>, m3: array2<int>;\r\n    m1 := new int[2,3];\r\n    m2 := new int[3,1];\r\n    m1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;\r\n    m1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;\r\n    m2[0,0] := 7;\r\n    m2[1,0] := 8;\r\n    m2[2,0] := 9;\r\n    m3 := Multiply'(m1, m2);\r\n    PrintMatrix(m1);\r\n    print \"\\n*\\n\";\r\n    PrintMatrix(m2);\r\n    print \"\\n=\\n\";\r\n    PrintMatrix(m3);\r\n}\r\n\r\nmethod PrintMatrix(m: array2<int>)\r\n    requires m != null\r\n{\r\n    var i: nat := 0;\r\n    while (i < m.Length0)\r\n    {\r\n        var j: nat := 0;\r\n        print \"\\n\";\r\n        while (j < m.Length1)\r\n        {\r\n            print m[i,j];\r\n            print \"\\t\";\r\n            j := j + 1;\r\n        } \r\n        i := i + 1;\r\n    } \r\n    print \"\\n\";\r\n}\r\n\r\npredicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) {\r\n  m1 != null && m2 != null && m1.Length1 == m2.Length0 \r\n}\r\n\r\npredicate AllowedToMultiplyInto(m1: array2<int>, m2: array2<int>, m3: array2<int>) {\r\n  AllowedToMultiply(m1,m2) && \r\n  m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 \r\n}\r\n\r\npredicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)\r\n{ \/\/ m3 is the result of multiplying the matrix m1 by the matrix m2\r\n    AllowedToMultiplyInto(m1,m2,m3) &&\r\n    forall i,j :: 0 <= i < m3.Length0 &#038;&#038; 0 <= j < m3.Length1 ==> m3[i,j] == RowColumnProduct(m1,m2,i,j)\r\n}\r\n\r\nfunction RowColumnProduct(m1: array2<int>, m2: array2<int>, row: nat, column: nat): int\r\n    requires AllowedToMultiply(m1,m2)\r\n    requires row < m1.Length0 &#038;&#038; column < m2.Length1 \r\n{\r\n    RowColumnProductFrom(m1, m2, row, column, 0)\r\n}\r\n\r\nfunction RowColumnProductFrom(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat): int\r\n    requires AllowedToMultiply(m1,m2)\r\n    requires row < m1.Length0 &#038;&#038; column < m2.Length1\r\n    requires k <= m1.Length1\r\n    decreases m1.Length1 - k\r\n{\r\n    if k == m1.Length1 then 0 else m1[row,k]*m2[k,column] + RowColumnProductFrom(m1, m2, row, column, k+1)\r\n}\r\n\r\nfunction RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, k: nat,i:nat): int\r\n    requires AllowedToMultiply(m1,m2)\r\n    requires row < m1.Length0 &#038;&#038; column < m2.Length1 &#038;&#038; i < m1.Length1 == m2.Length0\r\n    requires k<=i\r\n    decreases i - k\r\n{\r\n    if k == i then 0 else m1[row,k]*m2[k,column] + RowColumnProductTo(m1, m2, row, column, k+1,i)\r\n}\r\n\r\nfunction RowColumnProductForCount(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int\r\n    requires AllowedToMultiply(m1, m2)\r\n    requires row < m1.Length0 &#038;&#038; column < m2.Length1 &#038;&#038; n <= m1.Length1\r\n{\r\n  if n == 0 then 0 else\r\n    RowColumnProductForCount(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] \r\n}\r\n\r\npredicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>, rown:nat)\r\n  requires AllowedToMultiplyInto(m1, m2, m3)\r\n  requires rown <= m1.Length0 \r\n{ \r\n    forall r:nat,c:nat :: r < rown &#038;&#038; c < m2.Length1 ==> m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1) \r\n}\r\n\r\npredicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,coln:nat)\r\n  requires AllowedToMultiplyInto(m1, m2, m3)\r\n  requires row < m1.Length0 &#038;&#038; coln <= m2.Length1  \r\n{ \r\n    forall c:nat :: c < coln ==> m3[row,c] == RowColumnProductForCount(m1,m2,row,c,m1.Length1)\r\n}\r\n\r\npredicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,n:nat)\r\n   requires AllowedToMultiplyInto(m1, m2, m3)\r\n   requires row < m1.Length0 &#038;&#038; col < m2.Length1 &#038;&#038; n<=m1.Length1\r\n{ \r\n   m3[row,col] == RowColumnProductForCount(m1, m2, row, col, n)\r\n}\r\n\r\nmethod Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)\r\n    requires AllowedToMultiply(m1, m2)\r\n    ensures MM(m1, m2, m3)\r\n{\r\n    m3 := new int[m1.Length0, m2.Length1];\r\n\r\n  var row:nat := 0;\r\n  \/\/ loop over rows of m1\r\n  while(row < m1.Length0)\r\n    invariant row <= m1.Length0\r\n    invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)\r\n    modifies m3\r\n  {\r\n      assert MMROW(m1, m2, m3, row);\r\n      \/\/ loop over coloums of m2\r\n      var col:nat  := 0;\r\n      while(col < m2.Length1)\r\n        invariant col <= m2.Length1\r\n        invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)\r\n        invariant forall n:nat :: n <= col ==> MMCOL(m1, m2, m3,row, n)\r\n        {\r\n          assert MMCOL(m1, m2, m3, row, col); \/\/\r\n          \/\/ loop over elements of m1 row \/ m2 column\r\n          var i:nat  := 0;\r\n          m3[row,col] := 0;\r\n          while(i < m1.Length1)\r\n            invariant i <= m1.Length1\r\n            invariant forall rn:nat :: rn < row ==> MMROW(m1, m2, m3, rn)\r\n            invariant forall c:nat :: c < col ==> MMCOL(m1, m2, m3, row, c)\r\n            invariant forall j:nat :: j <= i ==> MMI(m1, m2, m3, row, col, j)\r\n           { \r\n             assert MMI(m1, m2, m3, row, col, i);\r\n\r\n             m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]);\r\n             i := i+1;\r\n\r\n             assert MMI(m1, m2, m3, row, col, i);\r\n           }\r\n           assert MMI(m1, m2, m3, row, col, m1.Length1);\r\n           assert m3[row,col] == RowColumnProductForCount(m1,m2,row,col,m1.Length1);\r\n           col := col+1;\r\n           assert MMCOL(m1, m2, m3, row, col);\r\n        }\r\n      assert MMCOL(m1, m2, m3, row, m2.Length1);\r\n      row := row+1;\r\n      assert MMROW(m1, m2, m3, row);\r\n  }\r\n  assert MMROW(m1, m2, m3, m1.Length0);\r\n  MMROWImpliesMM(m1, m2, m3);\r\n}\r\n\r\nlemma MMROWImpliesMM(m1: array2<int>, m2: array2<int>, m3: array2<int>)\r\n   requires AllowedToMultiplyInto(m1,m2,m3)\r\n   requires MMROW(m1, m2, m3, m1.Length0)\r\n   ensures MM(m1, m2, m3)\r\n{\r\n    assert forall r:nat,c:nat :: r < m1.Length0 &#038;&#038; c < m2.Length1 ==> m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1);\r\n    \r\n    forall r:nat,c:nat | r < m1.Length0 &#038;&#038; c < m2.Length1\r\n      ensures m3[r,c] == RowColumnProduct(m1,m2,r,c)\r\n    {\r\n      assert m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1);\r\n      RowColumnProductForCountImpliesRowColumnProduct(m1, m2, m3, r, c);  \r\n    }\r\n    \r\n    assert forall r:nat,c:nat :: r < m3.Length0 &#038;&#038; c < m3.Length1 ==> m3[r,c] == RowColumnProduct(m1,m2,r,c);  \r\n}   \r\n\r\nlemma RowColumnProductForCountImpliesRowColumnProduct(m1: array2<int>, m2: array2<int>, m3: array2<int>, r:nat, c:nat)\r\n   requires AllowedToMultiplyInto(m1,m2,m3)\r\n   requires r < m1.Length0 &#038;&#038; c < m2.Length1;\r\n   requires m3[r,c] == RowColumnProductForCount(m1,m2,r,c,m1.Length1)\r\n   ensures m3[r,c] == RowColumnProduct(m1,m2,r,c)\r\n{\r\n  assert RowColumnProduct(m1,m2,r,c) == RowColumnProductFrom(m1,m2,r,c,0);\r\n  \r\n  var i:nat := 0;\r\n  var total := RowColumnProductForCount(m1,m2,r,c,m1.Length1);\r\n  while i < m1.Length1\r\n     invariant i <= m1.Length1\r\n     invariant total == RowColumnProductForCount(m1,m2,r,c,m1.Length1-i) + RowColumnProductFrom(m1,m2,r,c,m1.Length1-i)\r\n  {\r\n    i := i+1;\r\n  }\r\n}\r\n<\/pre>\n<p>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.<\/p>\n<p><a href=\"http:\/\/rise4fun.com\/Dafny\/mgoeu\">http:\/\/rise4fun.com\/Dafny\/mgoeu<\/a><\/p>\n<pre lang=\"dafny\">\r\nmethod Main()\r\n{\r\n\tvar m1: array2<int>, m2: array2<int>, m3: array2<int>;\r\n\tm1 := new int[2,3];\r\n\tm2 := new int[3,1];\r\n\tm1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;\r\n\tm1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;\r\n\tm2[0,0] := 7;\r\n\tm2[1,0] := 8;\r\n\tm2[2,0] := 9;\r\n\tm3 := Multiply'(m1, m2);\r\n\tPrintMatrix(m1);\r\n\tprint \"\\n*\\n\";\r\n\tPrintMatrix(m2);\r\n\tprint \"\\n=\\n\";\r\n\tPrintMatrix(m3);\r\n}\r\n\r\nmethod PrintMatrix(m: array2<int>)\r\n\trequires m != null\r\n{\r\n\tvar i: nat := 0;\r\n\twhile (i < m.Length0)\r\n\t{\r\n\t\tvar j: nat := 0;\r\n\t\tprint \"\\n\";\r\n\t\twhile (j < m.Length1)\r\n\t\t{\r\n\t\t\tprint m[i,j];\r\n\t\t\tprint \"\\t\";\r\n\t\t\tj := j + 1;\r\n\t\t} \r\n\t\ti := i + 1;\r\n\t} \r\n\tprint \"\\n\";\r\n}\r\n\r\npredicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) {\r\n  m1 != null && m2 != null && m1.Length1 == m2.Length0 \r\n}\r\n\r\npredicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)\r\n  requires AllowedToMultiply(m1, m2)\r\n{ \/\/ m3 is the result of multiplying the matrix m1 by the matrix m2\r\n  m3 != null && \r\n  m3.Length0 == m1.Length0 && \r\n  m3.Length1 == m2.Length1 &&\r\n\tforall r:nat,c:nat :: r < m3.Length0 &#038;&#038; c < m3.Length1 ==> \r\n    m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) \r\n}\r\n\r\nfunction method RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int\r\n\trequires AllowedToMultiply(m1, m2)\r\n\trequires row < m1.Length0 &#038;&#038; column < m2.Length1 &#038;&#038; n <= m1.Length1\r\n{\r\n  if n == 0 then 0 else\r\n    RowColumnProductTo(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] \r\n}\r\n\r\nmethod Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)\r\n\trequires AllowedToMultiply(m1, m2)\r\n\tensures MM(m1, m2, m3)\r\n{\r\n\tm3 := new int[m1.Length0, m2.Length1];\r\n  \r\n  forall r:nat,c:nat | r < m3.Length0 &#038;&#038; c < m3.Length1\r\n  {\r\n     m3[r,c] := RowColumnProductTo(m1,m2,r,c,m1.Length1);\r\n  }\r\n}\r\n<\/pre>\n<p>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 <code>((((a+b)+c)+d)+e)<\/code>, don't have one of the do <code>(a+(b+(c+(d+e))))<\/code>.<\/p>\n<pre lang=\"dafny\">\r\nmethod Main()\r\n{\r\n\tvar m1: array2<int>, m2: array2<int>, m3: array2<int>;\r\n\tm1 := new int[2,3];\r\n\tm2 := new int[3,1];\r\n\tm1[0,0] := 1; m1[0,1] := 2; m1[0,2] := 3;\r\n\tm1[1,0] := 4; m1[1,1] := 5; m1[1,2] := 6;\r\n\tm2[0,0] := 7;\r\n\tm2[1,0] := 8;\r\n\tm2[2,0] := 9;\r\n\tm3 := Multiply'(m1, m2);\r\n\tPrintMatrix(m1);\r\n\tprint \"\\n*\\n\";\r\n\tPrintMatrix(m2);\r\n\tprint \"\\n=\\n\";\r\n\tPrintMatrix(m3);\r\n}\r\n\r\nmethod PrintMatrix(m: array2<int>)\r\n\trequires m != null\r\n{\r\n\tvar i: nat := 0;\r\n\twhile (i < m.Length0)\r\n\t{\r\n\t\tvar j: nat := 0;\r\n\t\tprint \"\\n\";\r\n\t\twhile (j < m.Length1)\r\n\t\t{\r\n\t\t\tprint m[i,j];\r\n\t\t\tprint \"\\t\";\r\n\t\t\tj := j + 1;\r\n\t\t} \r\n\t\ti := i + 1;\r\n\t} \r\n\tprint \"\\n\";\r\n}\r\n\r\npredicate AllowedToMultiply(m1: array2<int>, m2: array2<int>) {\r\n  m1 != null && m2 != null && m1.Length1 == m2.Length0 \r\n}\r\n\r\npredicate AllowedToMultiplyInto(m1: array2<int>, m2: array2<int>, m3: array2<int>) {\r\n  AllowedToMultiply(m1,m2) && \r\n  m3 != null && m3.Length0 == m1.Length0 && m3.Length1 == m2.Length1 \r\n}\r\n\r\npredicate MM(m1: array2<int>, m2: array2<int>, m3: array2<int>)\r\n  requires AllowedToMultiply(m1, m2)\r\n{ \/\/ m3 is the result of multiplying the matrix m1 by the matrix m2\r\n  m3 != null && \r\n  m3.Length0 == m1.Length0 && \r\n  m3.Length1 == m2.Length1 &&\r\n\tforall r:nat,c:nat :: r < m3.Length0 &#038;&#038; c < m3.Length1 ==> \r\n    m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) \r\n}\r\n\r\nfunction RowColumnProductTo(m1: array2<int>, m2: array2<int>, row: nat, column: nat, n:nat): int\r\n\trequires AllowedToMultiply(m1, m2)\r\n\trequires row < m1.Length0 &#038;&#038; column < m2.Length1 &#038;&#038; n <= m1.Length1\r\n{\r\n  if n == 0 then 0 else\r\n    RowColumnProductTo(m1, m2, row, column, n-1) + m1[row,n-1]*m2[n-1,column] \r\n}\r\n\r\npredicate MMROW(m1: array2<int>, m2: array2<int>, m3: array2<int>, rown:nat)\r\n  requires AllowedToMultiplyInto(m1, m2, m3)\r\n  requires rown <= m1.Length0 \r\n{ \r\n\tforall r:nat,c:nat :: r < rown &#038;&#038; c < m2.Length1 ==> m3[r,c] == RowColumnProductTo(m1,m2,r,c,m1.Length1) \r\n}\r\n\r\npredicate MMCOL(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,coln:nat)\r\n  requires AllowedToMultiplyInto(m1, m2, m3)\r\n  requires row < m1.Length0 &#038;&#038; coln <= m2.Length1  \r\n{ \r\n\tforall c:nat :: c < coln ==> m3[row,c] == RowColumnProductTo(m1,m2,row,c,m1.Length1)\r\n}\r\n\r\npredicate MMI(m1: array2<int>, m2: array2<int>, m3: array2<int>,row:nat,col:nat,n:nat)\r\n   requires AllowedToMultiplyInto(m1, m2, m3)\r\n   requires row < m1.Length0 &#038;&#038; col < m2.Length1 &#038;&#038; n<=m1.Length1\r\n{ \r\n   m3[row,col] == RowColumnProductTo(m1, m2, row, col, n)\r\n}\r\n\r\nmethod Multiply'(m1: array2<int>, m2: array2<int>) returns (m3: array2<int>)\r\n\trequires AllowedToMultiply(m1, m2)\r\n\tensures MM(m1, m2, m3)\r\n{\r\n\tm3 := new int[m1.Length0, m2.Length1];\r\n  \r\n  var row:nat := 0;\r\n  \/\/ loop over rows of m1\r\n  while(row < m1.Length0)\r\n    invariant row <= m1.Length0\r\n    invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)\r\n    modifies m3\r\n  {\r\n      assert MMROW(m1, m2, m3, row);\r\n      \/\/ loop over coloums of m2\r\n      var col:nat  := 0;\r\n      while(col < m2.Length1)\r\n        invariant col <= m2.Length1\r\n        invariant forall rn:nat :: rn <= row ==> MMROW(m1, m2, m3, rn)\r\n        invariant forall n:nat :: n <= col ==> MMCOL(m1, m2, m3,row, n)\r\n        {\r\n          assert MMCOL(m1, m2, m3, row, col); \/\/\r\n          \/\/ loop over elements of m1 row \/ m2 column\r\n          var i:nat  := 0;\r\n          m3[row,col] := 0;\r\n          while(i < m1.Length1)\r\n            invariant i <= m1.Length1\r\n            invariant forall rn:nat :: rn < row ==> MMROW(m1, m2, m3, rn)\r\n            invariant forall c:nat :: c < col ==> MMCOL(m1, m2, m3, row, c)\r\n            invariant forall j:nat :: j <= i ==> MMI(m1, m2, m3, row, col, j)\r\n           { \r\n             assert MMI(m1, m2, m3, row, col, i);\r\n             \r\n             m3[row,col]:= m3[row,col]+(m1[row,i]*m2[i,col]);\r\n             i := i+1;\r\n             \r\n             assert MMI(m1, m2, m3, row, col, i);\r\n           }\r\n           assert MMI(m1, m2, m3, row, col, m1.Length1);\r\n           assert m3[row,col] == RowColumnProductTo(m1,m2,row,col,m1.Length1);\r\n           col := col+1;\r\n           assert MMCOL(m1, m2, m3, row, col);\r\n        }\r\n      assert MMCOL(m1, m2, m3, row, m2.Length1);\r\n      row := row+1;\r\n      assert MMROW(m1, m2, m3, row);\r\n  }\r\n  assert MMROW(m1, m2, m3, m1.Length0);\r\n}\r\n<\/pre>\n<p>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\". <\/p>\n<p>In fact, looking in more detail, one of the attempts that they shared with me has this comment in it<\/p>\n<pre lang=\"dafny\">\r\n\/\/ TODO: continue here, multiplying m1 by m2 placing the result in m3 such that MM(m1, m2, m3) will become true\r\n<\/pre>\n<p>Which looks to me just like the kind of thing that I have seen written in many other courseworks. Hmm. Sucks.<\/p>\n<p><a href=\"http:\/\/rise4fun.com\/Dafny\/5F2R2\">http:\/\/rise4fun.com\/Dafny\/5F2R2<\/a><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/6PNo\">http:\/\/rise4fun.com\/Dafny\/6PNo<\/a><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/mXi49\">http:\/\/rise4fun.com\/Dafny\/mXi49<\/a><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/VtXb\">http:\/\/rise4fun.com\/Dafny\/VtXb<\/a><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/mgoeu\">http:\/\/rise4fun.com\/Dafny\/mgoeu<\/a> <!-- previous day --><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/1Yslx\">http:\/\/rise4fun.com\/Dafny\/1Yslx<\/a><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/WUop\">http:\/\/rise4fun.com\/Dafny\/WUop<\/a><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/RPnU\">http:\/\/rise4fun.com\/Dafny\/RPnU<\/a><br \/>\n<a href=\"http:\/\/rise4fun.com\/Dafny\/ji9A\">http:\/\/rise4fun.com\/Dafny\/ji9A<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>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 &hellip; <a href=\"https:\/\/www.lexicalscope.com\/blog\/2016\/02\/13\/dafny-matrix-mutiplication\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_feature_clip_id":0,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2},"jetpack_post_was_ever_published":false},"categories":[15],"tags":[],"class_list":["post-9944","post","type-post","status-publish","format-standard","hentry","category-dafny"],"jetpack_publicize_connections":[],"jetpack_shortlink":"https:\/\/wp.me\/p2e3P7-2Ao","jetpack_sharing_enabled":true,"jetpack_featured_media_url":"","_links":{"self":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/9944","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/comments?post=9944"}],"version-history":[{"count":10,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/9944\/revisions"}],"predecessor-version":[{"id":9972,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/posts\/9944\/revisions\/9972"}],"wp:attachment":[{"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/media?parent=9944"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/categories?post=9944"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.lexicalscope.com\/blog\/wp-json\/wp\/v2\/tags?post=9944"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}