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-16 06:01:04 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!postnews1.google.com!not-for-mail From: rod.chapman@praxis-cs.co.uk (Rod Chapman) Newsgroups: comp.lang.ada Subject: Re: [Spark] Using defered constants Date: 16 Apr 2003 06:01:04 -0700 Organization: http://groups.google.com/ Message-ID: References: NNTP-Posting-Host: 62.173.119.178 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1050498064 1293 127.0.0.1 (16 Apr 2003 13:01:04 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 16 Apr 2003 13:01:04 GMT Xref: archiver1.google.com comp.lang.ada:36183 Date: 2003-04-16T13:01:04+00:00 List-Id: Lutz Donnerhacke wrote in message news:> 7 private > 8 --# hide t; > 9 type x is new Integer; > 10 cx : constant x := 0; > 11 end t; Tricky! You are trying to arrange a package as follows: Visible spec: SPARK Private part of spec: hidden, Ada95 Body: SPARK This is actually very difficult, since logically the private is _is_ part of the body! In partiular, the Examiner does not assume anything much about the content of the private part when analysing the body, hence the error that you're seeing. Obvious point: why "type x is new Integer;"?? Do you really need an explicit derived type there? Why not "type X is Integer'First .. Integer'Last;"? This is legal SPARK, so no need to hide the private part at all. - Rod