From: Alexander Senier on 28 Jul 2010 18:43 Hi, SPARK GPL 2010 is out (check out http://libre.adacore.com) as binaries and source. While the SPARK and Ada tools can be build with gcc, the parts implemented in Prolog (namely the Simplifier and the Checker) require a commercial license of SICStus Prolog. I put together an experimental set of patches to build SPARK GPL 2010 using SWI Prolog. Preliminary tests indicate that the Simplifier built with SWI actually does the right thing. The patches can be downloaded here: http://senier.net/spark-gpl-2010-swi_patches.tgz Instructions how to build and test SPARK and known limitations are contained within the README file. Caveat: This port is in a very early stage -- use it at your own risk! Comments, suggestions and contributions are very welcome. Please do not use it to verify your airplane firmware (or any other critical piece of software) ;-) Regards Alex
From: Yannick DuchĂȘne (Hibou57) on 7 Aug 2010 16:16 Le Thu, 29 Jul 2010 00:43:28 +0200, Alexander Senier <mail(a)senier.net> a Ă©crit: > Caveat: This port is in a very early stage -- use it at your own risk! > Comments, suggestions and contributions are very welcome. Just wanted to express my interest for now (so that you do not feel alone). But will only test it for an unknown later date. Have a nice time any way :) Cheers -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
|
Pages: 1 Prev: ANN: GtkAda contributions v2.8 Next: What is your preferred VCS? |