From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,b761e94375940f9f X-Google-Attributes: gid103376,public X-Google-Thread: 108717,b761e94375940f9f X-Google-Attributes: gid108717,public X-Google-Thread: 115aec,b761e94375940f9f X-Google-Attributes: gid115aec,public X-Google-Thread: f43e6,b761e94375940f9f X-Google-Attributes: gidf43e6,public X-Google-ArrivalTime: 2002-07-13 17:35:36 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!sn-xit-05!sn-xit-06!sn-post-01!supernews.com!corp.supernews.com!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada,comp.realtime,comp.programming,comp.software-eng Subject: Re: ANNOUNCE: SPARK toolset 6.1 now available Date: Sat, 13 Jul 2002 19:27:35 -0500 Organization: Posted via Supernews, http://www.supernews.com Message-ID: References: <4519e058.0207110604.62691233@posting.google.com> X-Newsreader: Microsoft Outlook Express 4.72.3612.1700 X-MimeOLE: Produced By Microsoft MimeOLE V4.72.3719.2500 X-Complaints-To: newsabuse@supernews.com Xref: archiver1.google.com comp.lang.ada:27076 comp.realtime:5845 comp.programming:35132 comp.software-eng:12113 Date: 2002-07-13T19:27:35-05:00 List-Id: 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