root/branches/compiler/cSharp/ooasCompiler/doc/examples/Sum.ooas
| 3 | krennw | 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
|