Re: ANNOUNCE: SPARK toolset 6.1 now available

["Randy Brukardt" <randy@rrsoftware.com>]

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