draft.pvs

draft : THEORY
BEGIN
  
  
  
%  Cint : TYPE = subrange(-1000, 1000)
  Cint : TYPE = below(1000)
  Culi : type = below(1000000)
  
  pair : TYPE = [# x: Cint, y:nat  #]
  
  a:pair = (# x := 2, y := 12  #)
  first(a:pair):Cint = a`x
  zero(a:pair):pair = a with [ `x := 0 ]
  
  % Testing types
  a:Culi = 2
  b:Cint = 3+1
  c:int  = 3*(1+2)
  
  % Testing basic arithmetic

  incr(x:Cint):Cint = x + 1
  zero(x:int):Cint = 0
  f(a:Cint, b:Cint):Cint = zero(b) * incr(a)
  
  % Testing tests
  f(x:Cint):Cint =
    if x <= 1 and true then
      if x = 0 or x < 0 then 0 else x endif
    else 
      if x > 10 then 10 else x - 5 endif
    endif
   
  % Testing simple arrays
  Arr : TYPE = [ Cint -> Cint ]
  t:Arr = lambda(x:Cint) : x

  id2(t:Arr):Arr = t

  f(x:Cint):Arr = t
  update(x:Arr):Arr = x with [(0) := 0]

  % More complicated arrays
  Arr2: TYPE = [Cint -> Arr ]
  t2:Arr2 = lambda (x:Cint) : (lambda (y:Cint) : x + y)
  
  id(t:Arr2): Arr = let a = t in a(0)
  
  te:Arr = update(update(t))
  
  update(x:Arr2):Arr2 = x with [(0)(1) := 0 , (1) := lambda (x:Cint): x ]
  
END draft