ANNOUNCE: SPARK toolset 6.1 now available

ANNOUNCE: SPARK toolset 6.1 now available

[Rod Chapman]

Praxis Critical Systems is pleased to announce
the immediate availability of release 6.1 of
the SPARK language and the SPARK toolset.

Commercial supported customers will receive their
upgrades within the next few weeks.  Tool partners
and academic users will be upgraded following that.
A new release for readers of John Barnes' "SPARK Book"
will be available soon.

The full release note is available on-line at www.sparkada.com

The full definition of SPARK ("The SPARK Report") is
also available to interested parties upon request.

Release 6.1 of the SPARK language adds:

  - A useful subset of Ada95's tagged types are now permitted
    in SPARK95.  Inheritance and extension of tagged types are
    allowed, as is the overriding of basic operations.  Dispatching
    operations are not permitted.

  - A new "type assertion" annotation can be used to specify the
    predefined base type from which an integer type declaration
    is derived.  A complementary configuration-file mechanism allows
    a user to specify the details of packages Standard and System for
    a particular implementation.  When used together, these facilities
    greatly improve the Simplifier's ability to discharge run-time
    exceptions verification conditions arising from Overflow_Check
    in both SPARK83 and SPARK95.

  - Both full-range and constrained subtypes of modular types are
    now permitted in SPARK95.

There are also significant enhancements to the Examiner, Simplifier
and Checker with this release.  Highlights include:

  - When the configuration file mechanism is used to specify packages
    Standard and System, the Examiner can check a number of additional
    static semantic rules of Ada.  This also improves VC generation
    and simplification where the ranges of the predefined base types
    are required.

  - Simplifier version 2.04 ships on Windows and Solaris
    platforms with this release.  This includes improved proof
    tactics for enumerated inequalities, common SPARK idioms
    such as a "for" loop over an enumerated range, and simplification
    of quantified expressions.  The performance of the simplifier
    has also been greatly improved on large VCs.

  - Checker 1.47 ships on Windows and Solaris with this release. This
    includes extended rule families for dealing with modular arithmetic,
    bitwise operators and enumerated types.

This release re-inforces SPARK's position as the leading language
subset and static analysis technology for the construction of
high-integrity, critical software.

Please email us for more information at sparkinfo@praxis-cs.co.uk
or see www.sparkada.com

Yours,
  The SPARK Team
  Praxis Critical Systems

Note: The SPARK programming language is not sponsored
by or affiliated with SPARC International Inc and is
not based on SPARC(tm) architecture.

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Ted Dennison]

rod@praxis-cs.co.uk (Rod Chapman) wrote in message news:<ba18d5cb.0207102357.27f22745@posting.google.com>...
>   - A useful subset of Ada95's tagged types are now permitted
>     in SPARK95.  Inheritance and extension of tagged types are
>     allowed, as is the overriding of basic operations.  Dispatching
>     operations are not permitted.

By "dispatching" do you mean runtime polymorphisim as opposed to
compile-time polymorphisim? In other words, you wouldn't be allowed to
call a primitive routine with a classwide type, but you'd still be
allowed to call an inherited routine (or an overrided version of one)
with a specific tagged type object (not using 'class).


-- 
T.E.D.
Home     -  mailto:dennison@telepath.com (Yahoo: Ted_Dennison)
Homepage -  http://www.telepath.com/~dennison/Ted/TED.html

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Rod Chapman]

dennison@telepath.com (Ted Dennison) wrote in message news:
> By "dispatching" do you mean runtime polymorphisim as opposed to
> compile-time polymorphisim?

Correct. Run-time polymorhpism is not permitted.  Calling an
inherited (or overridden) basic operation with a specific tagged
subtype is OK.
 - Rod

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Randy Brukardt]

Rod Chapman wrote in message ...
>dennison@telepath.com (Ted Dennison) wrote in message news:
>> By "dispatching" do you mean runtime polymorphisim as opposed to
>> compile-time polymorphisim?
>
>Correct. Run-time polymorhpism is not permitted.  Calling an
>inherited (or overridden) basic operation with a specific tagged
>subtype is OK.


Do you do that by prohibiting T'Class, or do you allow it for uses like
hetrogeneous lists? If the latter, it seems as if there wouldn't be any
problem supporting run-time polymorphism. And if the former is true, its
hard to imagine what uses type extension can be put to...

           Randy Brukardt.

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> Rod Chapman wrote in message ...
> >dennison@telepath.com (Ted Dennison) wrote in message news:
> >> By "dispatching" do you mean runtime polymorphisim as opposed to
> >> compile-time polymorphisim?
> >
> >Correct. Run-time polymorhpism is not permitted.  Calling an
> >inherited (or overridden) basic operation with a specific tagged
> >subtype is OK.
> 
> 
> Do you do that by prohibiting T'Class, or do you allow it for uses
> like hetrogeneous lists? If the latter, it seems as if there
> wouldn't be any problem supporting run-time polymorphism. And if the
> former is true, its hard to imagine what uses type extension can be
> put to...

Well, I suppose you can use implementation inheritance and save
yourself repeating the code for inherited operations.

I would be _very_ surprised if SPARKada allowed T'Class
(uncertainty being something you don't want in safety-related
software).

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Robert A Duff]

Simon Wright <simon@pushface.org> writes:

> I would be _very_ surprised if SPARKada allowed T'Class
> (uncertainty being something you don't want in safety-related
> software).

If you have the entire program source code (which you should in a
safety-critical context), then I don't see why a dispatching call is any
more "uncertain" than a case statement.

- Bob

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Simon Wright]

Robert A Duff <bobduff@shell01.TheWorld.com> writes:

> Simon Wright <simon@pushface.org> writes:
> 
> > I would be _very_ surprised if SPARKada allowed T'Class
> > (uncertainty being something you don't want in safety-related
> > software).
> 
> If you have the entire program source code (which you should in a
> safety-critical context), then I don't see why a dispatching call is
> any more "uncertain" than a case statement.

I don't want to put words into Praxis's mouths, as it were, but a case
statement is very localised and less hard to reason about than a
dispatching call over an extended space.

Some of the reasoning for the position is probably practical: if you
have proof obligations to discharge and you can get machine help in
the proving, but only if you avoid Feature X (because -- for whatever
reason -- the tool doesn't do it), you probably will avoid Feature X
because the pain of doing the proof by hand is so much greater!

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Rod Chapman]

In answer to several points:

1) No - we don't currently allow 'Class anywhere, which means heterogeneous
lists are not supported directly in SPARK, although these may
be achieved by suitable hiding and abstraction.

2) SPARK does not currently include access type of any kind, since these
create some very difficult problems with the analysis of pointer effects
and aliasing.  If we can work out the analysis, then including some
support for general access types in future may in within scope.

3) Whether the restrictions implied by points 1) and 2) constitute
a "useful subset" of tagged types is really a matter of taste and outlook.
I guess time will tell if our users find the existing subset useful
for writing real programs of not...

Finally, in answer to Bob's point:

> If you have the entire program source code (which you should in a
> safety-critical context), then I don't see why a dispatching call is any
> more "uncertain" than a case statement.

But waiting until you have the "entire program" is _way_ too late!  One of
the major design goals of SPARK is to enable _constructive_ static
analysis of incomplete programs - hence the need for annotations
to strengthen the contracts in package specifications, for instance.

 - Rod Chapman, SPARK Team, Praxis Critical Systems.

Re: ANNOUNCE: SPARK toolset 6.1 now available

[Randy Brukardt]

Simon wrote:
>I would be _very_ surprised if SPARKada allowed T'Class (uncertainty
>being something you don't want in safety-related software).

There is nothing "uncertain" about T'Class. The family of types rooted
at T'Class is just a variant record with the tag as the discriminant.
There isn't even any defaults for the discriminant (the tag cannot be
changed). The only difference is that the exact set of variants isn't
determined until link time.

Similarly, a dispatching call is just a case statement on the variant
discriminant (that is, the tag), making a call to the body of the
appropriate routine. You can even write that in Ada, assuming you know
all of the types (which is the value of dispatching calls, that you
don't have to know them when you write the call).

         Disp (T'Class (Obj));

can be written as:

     if Obj'Tag = T'Tag then
            Disp (T(Obj));
     elsif Obj'Tag = T1'Tag then
            Disp (T1(Obj));
     ...
     end if;

Which was the point of my original query: if you can (usefully) write
the latter, it is trival to implement the former via expansion.

Rod Chapman wrote:.
>Finally, in answer to Bob's point:
>
>> If you have the entire program source code (which you should in a
>> safety-critical context), then I don't see why a dispatching call is
any
>> more "uncertain" than a case statement.
>
>But waiting until you have the "entire program" is _way_ too late!  One
of
>the major design goals of SPARK is to enable _constructive_ static
>analysis of incomplete programs - hence the need for annotations
>to strengthen the contracts in package specifications, for instance.

OK, but I don't quite see the connection. Clearly, if an overriding
routine has a contract that is different (other than strengthening based
on extension components) than that of the routine it overrrides, that is
a bug. The entire point of overriding is that the routines implement the
same abstract operation. So, you can do useful analysis on dispatching
calls simply with the root type's contract defined. (And it would have
to be defined before you could write any calls.) It might be necessary
to rerun the analysis as additional extending types are added to the
program, but that seems necessary anyway. Such a rerun mainly would find
problems in the specifications of the extending types.

In any case, the point is moot unless T'Class is supported in some
capacity. And I can see why you didn't bother if you don't have access
types, since T'Class is useful only in classwide routines (almost always
implemented with dispatching routines) and in access types for
hetrogeneous lists.

                     Randy Brukardt