OoasTools

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