|
types
|
|
MyInt = int [0..42];
|
|
SmallInt = int [0..3];
|
|
MyTuple = (MyInt, SmallInt);
|
|
Sum = autocons system
|
|
|[
|
|
var
|
|
my_list : list [4] of SmallInt = [5,5,5,5]
|
|
methods
|
|
add(a: MyInt, b: SmallInt) : MyInt =
|
|
requires true :
|
|
result := a + b
|
|
end
|
|
end ;
|
|
sum(Xs : list [4] of SmallInt) : MyInt =
|
|
requires true :
|
|
result := add :: (0) :>: (Xs)
|
|
end
|
|
end
|
|
actions
|
|
obs Sum(a: MyInt) =
|
|
requires a = sum(my_list) :
|
|
skip
|
|
end
|
|
do
|
|
var A : MyInt : Sum(A)
|
|
od
|
|
]|
|
|
system
|
|
Sum
|
|
|