type myarray

logic acc : myarray, int -> int
logic upd : myarray, int, int -> myarray 

axiom acc_upd_eq : 
forall t:myarray. forall i:int. forall c:int. 
acc(upd(t,i,c),i) = c

axiom acc_upd_neq :
forall t:myarray. forall i:int. forall j:int. forall c:int. 
j<>i -> acc(upd(t,i,c),j) = acc(t,j)


logic length : myarray -> int 

axiom length_upd :
forall t:myarray. forall i:int. forall c:int.
length(upd(t,i,v)) = length(t)

parameter get :
t:myarray ref -> i:int ->
{ 0<=i<length(t) } int reads t { result=acc(t,i) }

parameter set :
t:myarray ref ­> i:int ­> c:int ­>
{ 0<=i<length(t) } unit writes t { t=upd(t@,i,c) }
