Adding unit tests to Boogie

Oct 21, 2014 at 3:04 PM
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 Core there would be a CoreTests project.

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.
Oct 22, 2014 at 9:22 AM
Hi Dan,

this sounds good to me in general. I have two questions though:
  • Is it possible to run those unit tests using lit?
  • Why is it necessary to load .bpl files into memory? It seems like then you might as well write a system test, which is already possible with the existing setup. If you write a unit test it would seem like you could use mocking to avoid this.
Thank you,

Valentin
Oct 22, 2014 at 3:49 PM
Is it possible to run those unit tests using lit?
I think so but we will have to extend lit which I don't want to right now. You can simply run the nunit console for now.
nunit-console /path/to/test.dll
Why is it necessary to load .bpl files into memory? It seems like then you might as well write a system test, which is already possible with the existing setup. If you write a > unit test it would seem like you could use mocking to avoid this.
It is necessary for one of the tests because it checks for bugs in duplicating a whole program, you can't test this using the existing lit framework. Mocking is nice but I think you need proper interfaces for that and Boogie isn't really written that way.
Nov 17, 2014 at 9:16 PM
The unit tests are now in Boogie and are documented here