Matrix transpose

Specified and verified implementation of a (copying) matrix transpose.

General Information

Backend: Silicon
Language: PVL
Features: Iteration contracts, Arrays, Matrices
Path to Example File: arrays/Transpose.pvl
Should Verify: Yes
Date: 2017-06-12
Lines of Code: 23 (comments not included)
Lines of Specification: 19 (82.6% of total)
Computation Time: 40.5 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases TransposeCopy
//:: tools silicon
//:: verdict Pass

/*
  Specified and verified implementation of a copying matrix transpose.
*/

class Ref {
  context_everywhere out != null && inp != null && M>0 && N > 0;
	context_everywhere out.length == M*N && inp.length == N*M;
  context  (\forall* int i1 ; 0 <= i1 && i1 < M ;
             (\forall* int j1 ; 0 <= j1 && j1 < N ;
               Perm(out[i1][j1],write)));
  context  (\forall* int i1 ; 0 <= i1 && i1 < N ;
             (\forall* int j1 ; 0 <= j1 && j1 < M ;
               Perm(inp[i1][j1],1\2)));
  ensures  (\forall int i ; 0 <= i && i < M ;
             (\forall int j ; 0 <= j && j < N ;
               out[i][j]==inp[j][i]));
  ensures  (\forall int i ; 0 <= i && i < M ;
             (\forall int j ; 0 <= j && j < N ;
               inp[j][i]==\old(inp[j][i])));
  void transpose(int M,int N,int[M][N] out,int[N][M] inp){
    par(int i=0..M,int j=0..N)
        context  Perm(out[i][j],write);
        context  Perm(inp[j][i],1\4);
        ensures  out[i][j]==inp[j][i];
      {
        out[i][j]=inp[j][i];
      }
  }
}

Language: