class List {

  // container for the list's elements
  var a: array<int>;
  // size of the list
  var size: nat;

  predicate Valid()
   reads a, this;
  {
    a != null &&
    size >= 0 &&
    size <= a.Length &&
    0 < a.Length 
  }

  constructor init(len:int)
   requires len > 0 ;
   ensures Valid();
   ensures fresh(a);
   ensures size == 0;
   ensures a.Length == len ;
  modifies this;    
  {
    a := new int[len];
    size := 0;
  }

  method snoc(e: int)
   requires Valid() && size < a.Length ;
   ensures Valid();        
   ensures size == old(size) + 1;
   ensures a[old(size)] == e ;   
   ensures forall i :: 0 <= i < old(size) ==> a[i] == old(a[i])
   modifies a, `size;    
  {
    a[size] := e;    
    size := size + 1;    
  }

  method cons(val:int)
   requires Valid() && size < a.Length;
   ensures Valid();
   ensures size == old(size) + 1 ;
   ensures forall i :: 1 <= i <= old(size) ==> a[i] == old(a[i-1]) ;
   ensures a[0] == val;
   modifies a, `size;
  {      
    var i:int := size;
    while (i > 0) 
     invariant 0 <= i <= size ;
     invariant forall j :: 0 <= j < i ==> a[j] == old(a[j]) ;
     invariant forall j :: i < j <= size ==> a[j] == old(a[j-1]) ;
     decreases i;
     modifies a;
    {       
       a[i] := a[i-1];       
       i := i - 1 ;
    }
    a[0] := val;
    size := size + 1;
  }

  method tail()    
   requires Valid() && size > 0;
   ensures Valid();    
   ensures size == old(size) - 1 ;
   ensures forall i :: 0 <= i < size-1 ==> a[i] == old(a[i+1]) ;
   modifies `size, a;
  { 
    var i:int := 0;
    while (i < size-1) 
     invariant 0 <= i < size ;
     invariant forall j :: 0 <= j < i ==> a[j] == old(a[j+1]) ;
     invariant forall j :: i < j < size ==> a[j] == old(a[j]) ;
     decreases size - i;
     modifies a;
    {       
       a[i] := a[i + 1];       
       i := i + 1;
    }
    size := size - 1;
  }
  
  method head() returns (h:int)
   requires Valid() && size > 0;
   ensures Valid();
   ensures h == a[0] ; 
  {
    h := a[0] ;
  }
}