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,c8d893e8045967db X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-04-23 02:25:57 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!fu-berlin.de!uni-berlin.de!62.173.119.178!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: [Spark] Using defered constants Date: Wed, 23 Apr 2003 10:28:06 +0100 Message-ID: <3EA65CA6.5010705@praxis-cs.co.uk> References: NNTP-Posting-Host: 62.173.119.178 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: fu-berlin.de 1051089955 6629074 62.173.119.178 (16 [69815]) User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.0.2) Gecko/20030208 Netscape/7.02 X-Accept-Language: en-us, en Xref: archiver1.google.com comp.lang.ada:36395 Date: 2003-04-23T10:28:06+01:00 List-Id: This one is down to a decision I made years ago. If the full definition of a private type is hidden then there is some uncertainty about what element types it contains and that has implications for the analysis the Examiner can do. It seemed to me that I shouldn't make assumptions about what might be in the hidden private part of a package and therefore shouldn't allow the use of that type (and hence deferred constants of that type) in the subsequent package body. In general it seemed that if the private part of the package spec was hidden then the body was unlikely to be legal SPARK either. Lutz's question has caused me to reconsider all this and the next release of the Examiner will relax these rules so that after the point that Ada requires that the deferred constant to be complete it can be used even if the SPARK Examiner has not seen it (because it is hidden). The worst consequence for the Examiner will be the ability to construct programs with hidden pakcage private parts that will examine cleanly but not compile because soemthing in the hidden part makes them illegal Ada; at least this is "safe". As with all these things, it is feedback from active users that drive things forward! Peter Lutz Donnerhacke wrote: > The following error does not make much sense for me. Any workaround? > > $ cat example.lst > Line > 1 > 2 package t is > 3 type x is private; > 4 cx : constant x; > 5 procedure copy(o : out x; i : Integer); > 6 --# derives o from i; > 7 private > 8 --# hide t; > 9 type x is new Integer; > 10 cx : constant x := 0; > 11 end t; > 12 > 13 package body t is > 14 procedure doupdate(o : in out x; i : Integer) > 15 --# derives o from i, o; > 16 is > 17 --# hide doupdate; > 18 begin > 19 o := o + x(i); > 20 end doupdate; > 21 > 22 procedure copy(o : out x; i : Integer) is > 23 begin > 24 o := cx; > ^3 > *** ( 3) Semantic Error:611: Illegal use of deferred constant prior to its > full declaration. > > 25 doupdate(o, i); > 26 end copy; > 27 end t;