method matmul(a: array2<int>, b: array2<int>) returns (c : array2<int>)
  requires a != null
  requires a.Length0 > 0 && a.Length1 > 0
  requires a.Length0 == a.Length1 // que pour matrices carrées
  requires b != null
  requires b.Length0 > 0 && b.Length1 > 0
  requires b.Length0 == b.Length1 // que pour matrices carrées
  requires a.Length0 == b.Length0
  requires a.Length1 == b.Length1
  ensures fresh(c)
  ensures c.Length0 > 0 && c.Length1 > 0
  ensures c.Length0 == a.Length0 == b.Length0
  ensures c.Length1 == c.Length1 == b.Length1
  ensures a == old(a)
  ensures b == old(b)
{
  c := new int[a.Length0,a.Length1];

  var i := 0;
  var n := c.Length0;
  while (i < n)
    invariant 0 <= i <= n
  {
    var j := 0;
    while (j < n)
      invariant 0 <= i <= n
      invariant 0 <= j <= n
    {
      var k := 0;
      while (k < n)
        invariant 0 <= i <= n
        invariant 0 <= j <= n
        invariant 0 <= k <= n
      {
        c[i,j] := c[i,j] + a[i,k] * b[k,j];
        k := k + 1;
      }
      j := j + 1;
    }
    i := i + 1;
  }
}

method Main() {
  var a,b := new int[3,3], new int[3,3];
  a[0,0] := 1;
  a[0,1] := 2;
  a[0,2] := 3;
  a[1,0] := 4;
  a[1,1] := 5;
  a[1,2] := 6;
  a[2,0] := 7;
  a[2,1] := 8;
  a[2,2] := 9;

  b[0,0] := 9;
  b[0,1] := 8;
  b[0,2] := 7;
  b[1,0] := 6;
  b[1,1] := 5;
  b[1,2] := 4;
  b[2,0] := 3;
  b[2,1] := 2;
  b[2,2] := 1;

  var c := matmul(a, b);
  var x := 0;

  while (x < c.Length0)
    invariant 0 <= x <= c.Length0
  {
    var y := 0;
    while (y < c.Length1)
        invariant 0 <= y <= c.Length1
    {
        print(c[x,y]);
        print(" ");
        y := y + 1;
    }
    print "\n";
    x := x + 1;
  }
}