Parallel Block: Blanking

Simple verification example case where multiple sorts of data structures are "blanked" (that is, `0` is assigned to each element); first a single variable, then an array, and finally a matrix. All three sorts are connected via consecutive parallel blocks.

General Information

Backend: Silicon
Language: PVL
Features: Iteration contracts, Arrays, Matrices, Statically-scoped parallelism, Quantified permissions
Path to Example File: parallel/zero-many.pvl
Should Verify: Yes
Date: 2017-06-20
Lines of Code: 36 (comments not included)
Lines of Specification: 17 (47.2% of total)
Computation Time: 53.4 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases ZeroMultiple

class ZeroMany {
  int x;

context_everywhere ar != null && matrix != null && M>=0 && N>=0;
	context_everywhere ar.length == N;
	context_everywhere \matrix(matrix, M, N);
  context Perm(x,1);
  context (\forall* int i;0 <= i && i < N ; Perm(ar[i],write));
  context (\forall* int i1 ; 0 <= i1 && i1 < M ;
            (\forall* int j1 ; 0 <= j1 && j1 < N ;
              Perm(matrix[i1][j1],write)));
  ensures x==0;
  ensures (\forall int i;0 <= i && i < N ; ar[i]==0);
  ensures (\forall int i3 ; 0 <= i3 && i3 < M ;
            (\forall int j3 ; 0 <= j3 && j3 < N ;
              matrix[i3][j3]==0));
  void initialise(int M, int N, int[N] ar, int[M][N] matrix){
    par
      context Perm(x,1);
      ensures x==0;
    {
      x=0;
    }
    and (int i = 0 .. N)
      context Perm(ar[i],write);
      ensures ar[i]==0;
    {
      ar[i]=0;
    }
    and (int i=0..M,int j=0..N)
      context Perm(matrix[i][j],write);
      ensures matrix[i][j]==0;
    {
      matrix[i][j]=0;
    }
  }

}

Language: