automaton SquareRoot
  signature
    internal compute
    output halt
  states
    x: Nat,
    u: Nat := 1,
    w: Nat := 1,
    z: Nat := 0,
    done : Bool := false
  transitions
    internal compute
      pre ~done /\ w <= x
      eff z := z+1;
          u := u+2;
          w := w+u
    output halt
      pre ~done /\ w > x
      eff done := true

invariant of SquareRoot:
  done => (z*z) <= x /\ x < ((z+1)*(z+1))