Re: Generic-Package Elaboration Question / Possible GNAT Bug.

[Brian Drummond <brian@shapes.demon.co.uk>]

On Thu, 24 Nov 2011 08:07:45 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

>>
>> Should it mean that you don't care about separation of implementation
>> and interface?
> 
> What I think I was trying to say was that it doesn't seem to me to make
> a lot of difference whether the pre/post-conditions are dynamic.
> Providing, of course, I've understood your point.

I think it does.

> To take Georg's example of the stack, I don't see how you're going to
> express the fact that its capacity is bounded other than by comments
> about constraint errors or by preconditions.
> 
> I seem to be tempted into speculations about SPARK at this point. Stacks
> seem to be a rather dangerous construct from the point of view of
> proving correctness, logic not being very good at counting.

Indeed. But if you also prohibit recursion, maximum stack use is provable.

Spark is interesting in that some implementation facts (but not really 
details) do leak into the annotations (contracts) in the specification, 
though not into the Ada code for the specification. 

It has strategies to hide the details (this procedure modifies the state 
in that package, via an accessor) which are "refined" internally in the 
package implementation (the accessor modifies stack contents, stack 
pointer). 

But the state of the art seems to be that for contracts to be statically 
determinable, you must restrict how you program, compared to full Ada.

In this world, I come down on the side of: dynamically determinable 
contracts may not be perfect, but they are a lot better than nothing. I 
would use them and try to create tests to catch them out.

Ada is full of such implicit contracts, though they may have other names; 
some statically determinable...
for i in my_array'range loop 	-- I is contracted to be in range
and some dynamically determinable
a * 1000000	-- raises Constraint_Error if violated
and I don't see any objections to these (maybe from C programmers!)
so I think only good can come of the ability to create additional 
contracts.

Unless perhaps the programmer gains a false sense of security from having 
written contracts. But how is that any different from using the implicit 
ones?

Perhaps the best that can be hoped for is an assessment of each contract 
by the compiler (or proof tool), and a "WARNING: may raise exception" for 
the not-proven, to minimise such complacency.

- Brian