ANN: SPARKUnit

[Alexander Senier <mail@senier.net>]

Beware of bugs in the above code;
I have only proved it correct, not tried it.
(Donald E. Knuth)

Hi All,

I'm proud to announce the release of SPARKUnit version 0.1.0.

SPARKUnit is a unit test framework for the SPARK programming language.
It enables the developer to create unit tests in SPARK which can be
analysed by the SPARK Examiner. This allows for testing of SPARK
operations with preconditions and flow analysis of test cases.

Source code, license and further information is available from

   http://senier.net/SPARKUnit

The main design goal of SPARKUnit was to make unit testing in SPARK as
simple and flexible as possible and to avoid introduction of additional
verification overhead. Consequently, no preconditions must be
established to use SPARKUnit primitives and some errors (like
out-of-memory) will not be detected before running the test harness.
For the SPARKUnit library itself "only" absence of run-time errors has
been proven.

Regards,
Alex