AdaCore and Praxis have released SPARK Pro, an open source development enviroment focused on software development in areas where correct operation is vital.
Here’s a quote from the press release:
SPARK Pro combines the proven SPARK language and supporting toolset with AdaCore’s easy-to-use GNAT Programming Studio (GPS) Integrated Development Environment, backed by unrivalled support services. This provides a powerful method for developing critical systems.
The entire press release can be found here.
A new tool for generating automatic test data from Ada source code. Here’s a quote from the website:
Mika is an entirely automatic tool that analyses your Ada code and generates, carefully constructed, tests that will exercise all the branches or decision within your code at a level suitable for integration testing. With Mika, manual test data generation is no longer necessary.
Lots more information can be found on the MIDOAN website.
A small example of usage can be found here.
From Oliver M. Kellogg we get this news:
He also mentions that the Tcl/Tk and Gtk backends have been updated to newer toolkit versions and that some other backends currently aren’t maintained.
From the Rapid website we get this explanation on what Rapid is:
RAPID is the Rapid Ada Portable Interface Design tool. Using RAPID, programmers can easily create graphical user interfaces (GUIs) for their applications by simply drawing them. RAPID then generates Ada code using a platform independent GUI library.
Oliver ends his post with this:
Thanks go to Martin Carlisle, the original RAPID author, for his
The Rapid can be found here.
Phil Thornley has put up some SPARK tutorials at sparksure.com:
- Proof of absence of run-time error
- Proof Checker usage
Both tutorials contain several sections, with worked examples and exercises.
Also updated were a couple of the tools that help with SPARK proof:
- VC_View makes it easier to read and interpret SPARK verification conditions.
- PCHIF is an interface to the Proof Checker that makes it easier to recall and edit previously entered commands and to control the commands that are saved. (Previous versions of PCHIF were very unstable, but this is now sorted, thanks to Dmitry Kazakov and Maxim Reznik for their Gtk Router.)
The tools are currently only available as Windows executables.
Tools for SPARK Proof
Gautier is as busy as ever, and this time he brings us v.31 of his Zip-Ada library. As some might notice, the name is no longer UnZip-Ada.
Here’s a quote from Gautier:
The library’s name is now Zip-Ada and not UnZip-Ada anymore (except the site name at SF which is in the process of being renamed…)
Changes to Zip-Ada v.31 are:
- Added tiny demos: Demo_Zip, Demo_UnZip
- Added procedure Add_String in Zip.Create
And finally we have one incompatibility with previous versions:
- Zip.Create: Create / Finish: if Info.Stream is to a file, the underlying archive file is also created / closed as well
The entire thing can be found here.
A new QtAda/GtkAda Integration Kit is available, or rather; a technology preview for such a kit is available.
From the website we get this little snippet of information:
QtAda/GtkAda Integration Kit allows to use both toolkits in one application. It makes simple integration of existing GtkAda code into the QtAda application.
Technology preview is available for immediate download from the QtAda download page (see snapshot section).
The QtAda/GtkAda Integration Kit can be used with the latest QtAda 2.2.0 snapshots only.
This just in from Martin Krischik:
I have released a new MacPort version of the GCC compiler. The
Portfiles for the new release has been send up stream as I have become a
MacPorts maintainer and they can be compiled installed like any
other Port (MacPorts is a soucecode based distribution).
Since you need an bootstrap compiler I also created a binary release to get everybody started.
And on top of that I prepared new sourcecode tarballs for booch95 and
The new MacPort version can be found here.
Fast on the heels of v.01 and v.02, Gautier have released v.03 of his Ada Excel Writer.
New in this release is:
- data stream can now by any; supplied: Excel_Out_File, Excel_Out_String
- added “Text_IO”-like Put, Put_Line, New_Line,…
For those using the 01/02 versions, there’s this incompatibility to be aware of:
To write a file, you need to use Excel_Out_File instead of Excel_Out_Stream (which is now abstract); to create it is now Create instead of Create_File, same for Close.
The Excel Writer can be found here.