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,463c5796782db6d8 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-04-12 03:06:07 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!fu-berlin.de!uni-berlin.de!62.164.178.183!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: [Spark] Arrays of Strings Date: Sat, 12 Apr 2003 11:08:02 +0100 Message-ID: <3E97E582.9010806@praxis-cs.co.uk> References: <1ec946d1.0304111041.7edae9a@posting.google.com> NNTP-Posting-Host: 62.164.178.183 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: fu-berlin.de 1050141966 13260394 62.164.178.183 (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:36099 Date: 2003-04-12T11:08:02+01:00 List-Id: Matthew Heaney wrote: > rod.chapman@praxis-cs.co.uk (Rod Chapman) wrote in message news:... > >>Lutz Donnerhacke wrote in message news:... >> >>>In order to implement thin an execve binding, I wonder how to emulate the >>>C-Type "char const * const x []". Any bright ideas? >> >> >>Lutz and others, >> Here are some thoughts and a possible solution to this problem. >>The execve() API is indeed a complex one for SPARK, since the >>type "pointer to unconstrained array of pointer to null terminated >>C String" is a tricky one for SPARK to model. > > > [Rod's example snipped] > > > [Mathew Heaney...] > Personally, I find Rod's solution way too heavy. > > Why can't Spark model an access constant to a constant object? For > example: > The answer is it probably _could_ (but whether it _should_ is a much closer value judgement). In fact we are looking very seriously at "static" access discriminants as part of our work on adding the Ravenscar tasking profile to SPARK. (We have a working Ravenscar SPARK already without this feature). We have never claimed that SPARK is the largest subset of Ada for which formal verification is feasible; we claim only that it is big enough to write a large class of programs efficiently and that it represents a reasonable tradeoff of power and simplicity. Peter