ANN: SPARKUnit

ANN: SPARKUnit

[Alexander Senier]

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

Re: ANN: SPARKUnit

[yannick.moy]

Hi Alexander,

This is interesting to see how you manage to push the Ada/SPARK
boundary towards a nearly all-SPARK framework! I guess you plan to use
SPARKUnit to test your SPARKCrypto library? BTW, has SPARKSkein been
integreted in SPARKCrypto? I had seen in some initial discussion that
it was quite feasible.

just curious: how is it that AdaBrowse includes your SPARK contracts
in the HTML output, without even the # sign? Did you have to trick it?

Thx,
--
Yannick

Re: ANN: SPARKUnit

[Alexander Senier]

Hello Yannick,

> This is interesting to see how you manage to push the Ada/SPARK
> boundary towards a nearly all-SPARK framework! I guess you plan to use
> SPARKUnit to test your SPARKCrypto library?

Exactly! Actually it is already used in libsparkcrypto's current
development version. Unit test are much better compared to the ad-hoc
tests I had before. Naturally, SPARKUnit currently only does what I
need in libsparkcrypto - comments and suggestions for improvement are
therefore very welcome!

> BTW, has SPARKSkein been integreted in SPARKCrypto? I had seen in
> some initial discussion that it was quite feasible.

Technically it seams to be manageable. However, I changed the license in
version 0.1.1 from modified GPLv3 to simplified BSD, as I felt that I
do not fully understand the implications of my own project's license
terms. (As this was the only change, I never formally released version
0.1.1 - it is available from http://senier.net/libsparkcrypto).
Unfortunately this makes my library legally incompatible with
SPARKSkein...

> just curious: how is it that AdaBrowse includes your SPARK contracts
> in the HTML output, without even the # sign? Did you have to trick it?

No tricks - AdaBrowse actually has a feature that handles special
comment blocks like the SPARK annotations. By adding

   Format."--#" = enclose ("<pre class=spark>", "</pre>")

to your AdaBrowse configuration, SPARK annotations will get enclosed by
a special <pre> block. You can then use CSS to layout these blocks as
desired.

Regards,
Alex