SPARK news - May 2005

Please find below the latest installment of SPARK-related news and information from the SPARK team here at Praxis.

Ada community award

SPARK Team was awarded the 2004 ACM SIGAda award for outstanding contribution to the Ada community. At the SPARK User Group meeting, the award was dedicated to Professor Bernard Carré - the founder of Program Validation Limited and principal designer of SPARK.

Ada Usage Survey 2005

The Ada Resource Association is attempting to quantify the global
market for Ada. We'd like to encourage people to fill in their Ada usage survey. This is important to show the outside world that people really are still using Ada, and that SPARK forms a significant share of that market! We hope you can fill the survey in for your projects. The results will be presented at Ada Europe 2005 in York.

GPS Pro 3.0.0 and SPARK

The recent release of GPS Pro 3.0.0, AdaCore's free multi-language IDE, includes a SPARK customization file. This creates a SPARK menu, and allows users to run their SPARK tools from inside GPS - a help to anyone who prefers their life a little more GUI-fied.

UML and SPARK

A joint development effort between I-Logix and Praxis now enables the generation of SPARK Ada code directly from UML models. This involves a new capability to I-Logix’ UML Model-Driven Development (MDD) product, Rhapsody, that facilitates the development of fully SPARK compliant Ada applications.

This development complements the existing support of SPARK in the ARTiSAN Real-Time Studio product line.

A new one-day "UML to SPARK" course has been designed for customers wishing to take advantage of these developments. The first public "UML to SPARK" course will take place in September in Bath.

SPARK black belt training

The new SPARK Black Belt course - designed for advanced users and focusing on proof - has been very successful. Feedback has been overwhelmingly positive.

The next public SPARK and black belt courses are scheduled for September - book now to guarantee your place.

Spreading the word

In April, Praxis hosted a highly successful one-day seminar for senior managers and senior engineers to describe the Correctness by Construction approach. This took place in the National Cryptological Museum in Maryland, USA, and featured guest speaker Randy Johnson from the NSA.

Forthcoming conferences include AdaEurope, where SPARK team will be giving two tutorials, presenting a paper and exhibiting. We will also be giving a tutorial at Formal Methods '05 in the UK in July.

Academic developments

In October, Praxis announced a joint academic initiative with AdaCore, as part of our ongoing attempt to promote SPARK within universities.

The primary objective of AdaCore's Ada Academic Initiative is to provide a collaborative platform where educational materials, knowledge, resources and fresh ideas can be developed and shared. This is perfectly complemented by Praxis' offer of a fully supported professional SPARK toolset offered free-of-charge to university faculty members for teaching and/or research.

Release 7.2

Release 7.2 went out to customers in January this year. Hopefully everyone is now using this upgrade and enjoying the enhancements, particularly in the Simplifier. Upgrades for the "book" demo toolset to release 7.2 are also available

Team news

The SPARK team has been joined for 6 months by research student Bill Ellis. Bill is exploiting research from a previous project (called NuSPADE) to extend the proof capabilities of the SPARK toolset.

Emphasis is being placed on addressing the practicalities of an industrial system, rather than discovering new proof strategies.

For more details click here.

Carys Ottner has joined the team from within Praxis. Carys is mainly working on support, marketing, training and porting the Proof Checker to a new PROLOG compiler.

Contacting us

Please drop us a line - about support, upgrades, the book, or anything! The details are as usual:
email: sparkinfo@praxis-his.com
telephone hot-line: +44 1225 823829

Rod's technical corner - type assertions and proof

For the technically minded, here's the first in what we hope will become a regular feature for the newsletter.

Our first techie corner focusses on the type-assertion annotation and its use.

Before we look at what it does, let's look at the problem! Consider a simple integer type such as:

type T is range 0 .. 100;

and an assignment

A := (B + C) / 2;

where A, B, and C are all of type T.

If you use the Examiner's "/exp" option to generate run-time check VCs, you'll see a VC of the form:

(B in T) and
(C in T)
->
(B + C) in T'Base

to show that the intermediate result of adding A and B doesn't overflow the base type of T. But what is T'Base anyway, and what is it's range?!?! Here's the problem: the choice of T'Base for an integer type T is said to be "implementation-defined" - it's one of the predefined Integer types declared in package Standard, but it's up to the compiler to choose which one, and the Examiner can't guess that, so we have to tell give it a bit of help.

That's where the type assertion comes in. You need to read the documentation (for your _cross_-compiler, of course...) to see what it would choose, then tell the Examiner, thus:

type T is range 0 .. 100;
--# assert T'Base is Short_Integer;

OK..now the Examiner knows that T'Base is Short_Integer, and that T'First is Short_Integer'First and so on. Great - but what's Short_Integer'First?? Yup - you guessed it - this is also implementation- defined, so we need to tell the Examiner, this time using a configuration file approproate for your compiler. We would supply a configuration file containing something like:

package Standard is
type Short_Integer is range -2**15 .. 2**15-1;
type Integer is range -2**31 .. 2**31-1;
end Standard;

This fills in all the blanks. The Examiner can now generate replacement rules for T'Base'First and T'Base'Last that the Simplifier can use. After simplification, the VC comes out something like:

(B >= 0 and B <= 100 and C >= 0 and C <= 100)
->
(B + C) >= -32768 and
(B + C) <= 32767

which is trivially proved by the Simplifier!

Easy huh!

Moral:
1) Always use a configuration file to tell the Examiner about the range of the predefined types.
2) Always direclty follow an integer type declaration with an appropriate type assertion.
3) Always use the "/exp" switch on the Examiner to generate such Overflow_Check VCs.

That's it for this time...
- Rod Chapman and SPARK Team