Larger Corpus of SPARK (preferably pre-2014) code?

General
1

I’m looking for larger examples of SPARK code, esp pre-SPARK 2014. It’s easier to find examples of older Ada code bases, and new SPARK code, but I’d like to see larger and more complete examples of older SPARK code. Does anyone know some?

2

I think most are going to be SPARK 2014; prior to this version of SPARK, this language used annotated comments for proving.

There’s a large project “Tokeneer” that was done all in SPARK, I think by the NSA and made available.

3

That example is great, thank you! I actually have John Barnes’ High Integrity Software: The SPARK Approach to Safety and Security, which had me thinking about older SPARK codebases. It seems like there aren’t many complete examples out there, but I’ll look around for Tokeneer.

4

Original SPARK 2005: GitHub - martin-cs/Tokeneer · GitHub
The updated SPARK 2014 code: spark2014/testsuite/gnatprove/tests/tokeneer at master · AdaCore/spark2014 · GitHub

5

Thank you! I found those after you mentioned Tokeneer, as well as some wayback machine references to the original AdaCore site (I wish they didn’t kill old webpages as frequently as they seem to do…). It also looks like the “Ada Gems” papers have some interesting commentary on Tokeneer and other SPARK code bases, so I might try to build some references around it. Thank you again for this!

6

You’re welcome.
I hope it helps.

BTW, what is your interest in the older varient?
SPARK 2014 using Ada 2012’s aspect system was an incredible leap forward: having the proof’s definitions be legitimate code for the host language eliminates the “annotations got out of sync” problem, and it encourages the proof-system to be integrated into the compiler. (Though it is separate with GNAT, I can easily imagine a compiler integrated with static analysis and proof engines.)

7

I’ve been on a bit of an Ada book bender, and SPARK seems extremely interesting, but I couldn’t find as much about older SPARK versions outside of literature. So mainly historical curiosity combined with with an interest in the semantics of the language and how it would manifest in an actual codebase.