Re: ANN: SPARKUnit

[Alexander Senier <mail@senier.net>]

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