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