logic m,n,p : int

type matrix

logic get : matrix, int, int -> int

parameter c : matrix ref

logic ab : int,int -> int


let test () =
  { 0 < m and 0 < n and 0 < p }
  let i = ref 0 in
  while !i < m do 
    { invariant i <= m and
      forall i',j':int. 
        0 <= i' < i -> 0 <= j' < p -> get(c,i',j') = ab(i',j') }
    L2:
    let j = ref 0 in
    while !j < p do 
      { invariant 0 <= j <= p and
  (forall j':int. 0 <= j' < j -> get(c,i,j') = ab(i,j')) and
  (forall i',j':int. 0 <= i' < i -> 0 <= j' < p 
	-> get(c,i',j') = get(c@L2,i',j')) }
      [ {} unit writes c 
        { get(c,i,j) = ab(i,j) and
  (forall j':int. 0 <= j' < j -> get(c,i,j') = ab(i,j')) and
  (forall i',j':int. 0 <= i' < i -> 0 <= j' < p -> get(c,i',j') = ab(i',j')) }
      ];
      j := !j + 1
    done;
    i := !i + 1
  done
  { forall i',j':int. 0 <= i' < m -> 0 <= j' < p -> get(c,i',j') = ab(i',j') }