Boogie currently doesn't have any unit tests and I think this needs to change because
- It is hard to write test cases for bugs found in Boogie's API using the
lit tests because they only really test the behaviour of the Boogie driver
- Boogie's libraries aren't very "library" like right now due to dependencies on Boogie's Command line parser (see
issue 10244). Introduction of unit tests will hopefully encourage this to be slowly fixed as removing the unnecessary dependencies will make it easier to write unit tests.
This is my proposal
Use the NUnit
framework for unit tests. The reason for choosing this is because NUnit works with both MonoDevelop and Visual Studio.
NUnit works with visual studio by using an extension (NUnit test adapter
). There's also a test runner application that can run the tests outside of Visual Studio as well which we'll
need for continuous integration testing. The NUnit framework needs to be manually installed under Windows
NUnit is shipped with mono but unfortunately it's an older version (2.4.8) rather than the latest stable 2.6.3. Using 2.6.3 on Windows seemed fine when I tried it but we have to be careful to not use APIs in 2.6.3 that are not available in 2.4.8
What I'd like to do is create a project for each library we want to write to write tests for, e.g. for
there would be a
Current I only have tests for Core so that's what I add initially. These tests are mainly regression tests rather than tests aimed at testing the full functionality of classes but we have to start somewhere.
We will need a few ugly hacks for these unit tests to work
- As I mentioned earlier
Boogie's libraries have a horrible dependence on a global
CommandLineOptions object. We can hack around this for now but it needs to fixed properly. I think it would be best if we iteratively fixed this until it is possible to use the Core
library (and eventually all libraries) without the global
CommandLineOptions.Clo object being initialised
- Some unit tests need to load
bpl files into memory. The way I currently do this is to have a folder of programs containing the programs which the build system copies into the folder containing the binaries and then have a helper function load
that will load a program, parse it and type check it. An alternative it to have programs written as multi-line string literals, the problem with this is that the boogie program code cannot be shared between tests.
Thoughts? I plan to start doing this soon but I'd like to know if anyone has any thoughts.