Progression of Zeno systems

During the past week Adam has been implementing a series of models developed by Walid, Jan and Adam, evaluating the enclosure semantics' performance on Zeno systems. An example of such a model is the following, inspired by a formulation of Zeno's paradox:

class Main(simulator)

  private

    d := 1; d' := -1;

    s := 1/2;

    mode := "q"; 

  end

  switch mode assume s <= abs(d)

    case "q"

      if s == d 

        s := s/2; 

        mode := "q" 

      end;

      d' = -1;

  end;

end

Adding a mode invariant (using the assume keyword) enables the interpreter to prune enclosures of impossible solutions, yielding a better overall enclosure. Though, at first glance, s <= d seems to be a suitable invariant for this system, this invariant does not hold after d crosses zero – changing this to s <= abs(d) ensures that the invariant holds for the entire simulation time. 

Adam will spend the coming week participating in a one-week Scala course given at Chalmers, learning about things such as implicit conversions, API design, polymorphic embedding of DSLs, scala-virtualized and LMS.