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 08:15:49 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail From: Lutz Donnerhacke Newsgroups: comp.lang.ada Subject: Re: [Spark] Using defered constants Date: Wed, 16 Apr 2003 15:15:48 +0000 (UTC) Organization: IKS GmbH Jena Message-ID: References: <1050505512.114638@master.nyc.kbcfp.com> NNTP-Posting-Host: taranis.iks-jena.de X-Trace: branwen.iks-jena.de 1050506148 26020 217.17.192.37 (16 Apr 2003 15:15:48 GMT) X-Complaints-To: usenet@iks-jena.de NNTP-Posting-Date: Wed, 16 Apr 2003 15:15:48 +0000 (UTC) User-Agent: slrn/0.9.7.4 (Linux) Xref: archiver1.google.com comp.lang.ada:36188 Date: 2003-04-16T15:15:48+00:00 List-Id: * Hyman Rosen wrote: > Lutz Donnerhacke wrote: >> It's an example. I need an access type there. > > SPARK doesn't have access types, I hear. I'm told that this is so that > the correctness of the code is easier to prove, and that code that needs > access types should be written in plain Ada. Your ears are working fine. I can use a sufficient Integer type, too, but playing with such brain damages is subject of the other side of the Spark border. I only have to fullfill the API constraints. You may suggest to not use Spark everytime, an enviroment is accessed, but this is clearly not an option, because it requires the whole programm to be written in Ada not Spark consequently. OTOH my question does not deal with this topic, but with a Spark strangeness. So please keep the ball in the field. Thank you. PS: I use Spark to shrink the executable's size: By proofing the absence of run time errors, I can drop the run time checks completely. In order to not introduce those error handlers again in the patch code written in Ada, the Ada parts has to be as simple as possible. That's why the mix is free from run time errors despite I use glue code! (Otherwise the linker will complain.)