Re: [Spark] Arrays of Strings

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Matthew Heaney wrote:
> rod.chapman@praxis-cs.co.uk (Rod Chapman) wrote in message news:<cf2c6063.0304110211.596b6b2b@posting.google.com>...
> 
>>Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb95ehu.ob.lutz@taranis.iks-jena.de>...
>>
>>>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