Commits

Nadia Polikarpova committed 11639a9 Draft

Integrated Carlo's changes.

  • Participants
  • Parent commits cbda772

Comments (0)

Files changed (1)

 * **Backtrack control flow choices**.
 If a non-deterministic jump leads to an assumption violation, the interpreter will go back and try another branch until it's out of options.
 
-Boogaloo is, however, still under development and lacks many other cool features, for example:
+Boogaloo is still under development and lacks many other important features, for example:
 * **Backtracking value choices**.
-Currently, whenever a value must be chosen non-deterministically (e.g. in a {{{havoc}}} statement),
+Whenever a value must be chosen non-deterministically (e.g. in a {{{havoc}}} statement),
 the interpreter just uses a default value of the appropriate type.
-If this choice leads to an assumption violation, a runtime failure occurs.
+If this choice leads to an assumption violation, a run-time failure occurs.
 In future versions we plan to use a backtracking monad (like [[http://okmij.org/ftp/Computation/LogicT.pdf|LogicT]]) 
 and enable the interpreter to reconsider its value choices.
 
 * **User-defined types**.
-Currently execution is limited to integer and boolean variables.
+Execution is limited to integer and boolean variables.
 
 * **Type inference**.
-The Boogaloo type checker cannot infer types yet.
+The Boogaloo type checker cannot infer types.
 In practice it means that every function application,
 where the the function return type is generic and does not occur among the arguments,
 has to be surrounded by a coercion.
 In the future Boogaloo might use a constraint solver to make smarter non-deterministic choices.
 
 * **Support for bit vectors and reals**.
-Together with some other esoteric constructs, those can not yet be parsed.
+Together with some other esoteric constructs, those cannot be parsed.
 
 * **Debugging**.
 Executing Boogie programs step-by-step and observing variable values and non-deterministic choices at each program location will be be even more helpful in understanding failed verification attempts.
 
 * **Performance**.
-So far Boogaloo was designed with simplicity, not run-time performance in minds,
-so there is a big potential for optimization.
+Boogaloo was designed with simplicity, not run-time performance, in mind,
+so there is a big potential for optimizations.
 
-For a full list of unsupported constructs and planned modifications, see <<file todo>>.
+We're working on adding all these cool things! For a full list of unsupported constructs and planned modifications, see <<file todo>>.