Commits

Nadia Polikarpova committed 75d7fd8 Draft

Edited online

  • Participants
  • Parent commits 4d3fc02

Comments (0)

Files changed (1)

 To check out what else Boogaloo can do 
 try it on sample Boogie programs from the <<file examples>> directory.
 
-=Running Boogaloo=
+=Further Reading=
 
-We are using <<file examples/SumMax.bpl>> as an example in this section.
-
-You can run Boogaloo in one of the three modes.
-
-===General mode===
-
-The most basic Boogaloo invocation is:
-{{{
-boogaloo SumMax.bpl
-}}}
-
-The above command will try to find one valid execution of procedure {{{Main}}} in SumMax.bpl and upon its termination display the values of all global entities and parameters of {{{Main}}} that were read or written during the execution.
-An alternative entry point can be specified through the {{{--proc}}} flag.
-
-You have control over various parameters of the non-deterministic behavior, such as the //branching factor// (the maximum number of possibilities to consider at every choice point), the way integer values are generated (exhaustively or randomly), the limit on the number of executions to try and to display, as well as filtering options for executions.
-
-By default Boogaloo filters out invalid executions (those that end with an assumption violation). If you completely disable filtering then the number of executions to try and to display become the same thing. If you remove the limit on the number of executions, it will only be bounded by the branching factor. So if you further set the branching factor to "unbounded" the interpreter will keep producing new executions infinitely – that is, if you program involves at least one non-deterministic choice of an integer value.
-
-For example, here is how to ask Boogaloo to try 100 executions with a branching factor of 8 and show you the first 5 failing ones:
-{{{
-boogaloo -b 8 -e 100 -N=false -P=false -o 5 SumMax.bpl
-}}}
-
-Check {{{boogaloo --help}}} for additional options.
-
-===Exhaustive testing===
-
-{{{
-boogaloo test --proc SumMax SumMax.bpl
-}}}
-
-The above command will execute procedure {{{SumMax}}} in SumMax.bpl on all inputs within a default range
-and display a summary of the test cases. This is just a shortcut to invoke Boogaloo with an unlimited number of executions, reduced branching factor, no execution filtering and summary output.
-
-===Random testing===
-
-{{{
-boogaloo rtest --proc SumMax SumMax.bpl
-}}}
-
-The above command will execute procedure {{{SumMax}}} in SumMax.bpl on random inputs
-and display a summary of the test cases. This is just a shortcut to invoke Boogaloo with a certain limit on the number of executions, random input generation, no execution filtering and summary output.
-
-
-=Compiling Boogaloo=
-
-To compile Boogaloo you will need [[http://www.haskell.org/ghc/|GHC]] and [[http://www.haskell.org/cabal/|Cabal]],
-which you can get as part of [[http://www.haskell.org/platform/|Haskell Platform]], together with other Haskell tools.
-We are currently using GHC 7.4.1, but other recent versions probably work too.
-
-From the top-level source code directory (where <<file language-boogie.cabal>> is located) run:
-{{{
-cabal install
-}}}
-This will build a Boogaloo executable and store it in the default Cabal binary directory (which should normally already be on your PATH). If you would like to store the executable in another directory, add an option {{{--bindir=another_directory}}}.
-
-The package also provides a language infrastructure library, which contains a Boogie AST, parser, type checker, and pretty-printer.
-Running the above install command will install the library into your system.
-After that you can import modules from the package into your source code, e.g. {{{import Language.Boogie.AST}}}.
-If you would like to install the library without building the Boogaloo executable, add a {{{-boogaloo}}} flag:
-{{{
-cabal install --flags="-boogaloo"
-}}}
-
-In order to also build a {{{boogaloo-tests}}} executable, which tests various parts of the library, add a {{{-tests}}} flag:
-{{{
-cabal install --flags="tests"
-}}}
-
-=Features and limitations=
-
-Boogaloo can do the following exciting things:
-* **Execute non-deterministic programs**.
-For example, for the following statements the interpreter will report eight valid executions, the first of which assigns 2 to {{{x}}} and 3 to {{{y}}}:
-{{{
-#!boogie
-
-    havoc x, y;
-    assume x*x + y*y == 13;
-}}}
-
-* **Infer constraints and definitions from axioms** of a particular shape.
-For example, Boogaloo will understand the following definition of the factorial function:
-{{{
-#!boogie
-
-    function factorial(int): int;
-    axiom factorial(0) == 1 && factorial(1) == 1;
-    axiom (forall x: int :: x > 1 ==> factorial(x) == x * factorial(x - 1));
-}}}
-
-* **Infer quantification domains** from linear constraints. 
-When the interpreter sees an expression like\\{{{forall i: int :: 0 <= i && i < 10 ==> P(i)}}} 
-it figures that it's enough to check if {{{P(i)}}} holds for {{{i}}} between 0 and 9;
-outside this //domain// the scoped formula is always true anyway.
-If it cannot find a finite domain, the scoped formula will be evaluated for all values within globally specified bounds. 
-
-Boogaloo is still under development and lacks many other important features, for example:
-* **Using maps** as indexes in other maps or as quantified variables: those constructs are currently not executable. The same goes for lambda expressions. 
-
-* **Integration with a constraint solver**.
-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 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**.
-Boogaloo was designed with simplicity, not run-time performance, in mind,
-so there is a big potential for optimizations.
-
-We're working on adding all these cool things! For a full list of unsupported constructs and planned modifications, see <<file todo>>.
+* [[User Manual]]: how to use and compile Boogaloo?
+* [[http://se.inf.ethz.ch/people/polikarpova/publications/rv13.pdf|To Run What No One Has Run Before]]: our paper about Boogaloo at RV'13; read this to learn more about what's under the hood.