arrays.pvs

arrays : THEORY
BEGIN

  RetType : TYPE = int; %% below(20);

  Arr1 : TYPE = [below(10) -> RetType ]
  Arr2 : TYPE = [below(10) -> [below(8) -> below(6)] ]
  Arr3 : TYPE = [below(10) -> RetType ]
  Arr4 : TYPE = [below(10) -> Arr3 ]

  b:Arr1 = lambda (x:below(10)) : x

  getb(a:below(10)):Arr1 =  b
  
  id(t:Arr1) :Arr1 = t
  
  id2(t:Arr1) :Arr1 = id ( id (t) )
  
  incr(t:Arr1) : Arr1 = t with [ (t(0)) := t(9) ]
  decr(t:Arr1) : Arr1 = b with [ (0) := 1 ]

  sum( T:Arr1, U:Arr1) :Arr1 = lambda (x:below(10)) : T(x) + U(x)
  
  foo(t:Arr1)  : Arr1 = t with [ (0) := t(9) + 1, (t(0)) :=  t(0) + 1 ]
  
  bar(t:Arr2)  : Arr2 =
    let a = t with [ (0)(0) := 0 ]
    in a

  test(t:Arr3) : Arr3 = t with [ (0) := 8 + 1 ]
  
  set0( t:Arr4, x:below(10), y:below(10)) : Arr4 = t with [ (x) := (  t(0) WITH [ (0) := 0 ] ) ]


END arrays