Re: Silly and stupid post-condition or not ?

["Randy Brukardt" <randy@rrsoftware.com>]

"Phil Thornley" <phil.jpthornley@gmail.com> wrote in message 
news:MPG.299868e7ebbd43b1989683@news.zen.co.uk...
> In article <jgl70g$l9i$1@munin.nbi.dk>, randy@rrsoftware.com says...
...
> The original SPARK Rationale says:

I don't much care why SPARK is the way it is -- it's obvious that it makes 
sense for a certain set of customers, and that's great.

I want a tool that would be useful for typical Ada programs, and these are 
going to have dispatching and access types and exceptions and tasks ...

There is no way that SPARK is ever going to be that tool, it would destroy 
its purpose.

But I don't necessarily want complete proofs, and as I noted last week, I 
don't think that there is much value to complete proofs as a goal, because 
if you have a language that can describe the specifications well enough that 
you can prove the result, you no longer need the Ada code that's being 
proved (just execute the specification). We need "enough" proof, but not too 
much.

I'm much more interested in proving that a subprogram meets its 
postconditions (including exception postconditions) given its parameter 
types and preconditions.

SPARK insists that you go back to the bad old days of using essentially 
untyped arrays for data storage rather than typed pointers, using error 
codes and piles of exceptional logic rather than exceptions, and the like --  
all of the reasons that I moved to Ada in the first place. It eliminates 
virtually everything that makes Ada better than "just another programming 
language", which is not a step forward for my uses. (Obviously, other 
people's experiences and needs will vary.)

Yes, aliasing analysis is hard. That's the point -- if the typing of the 
underlying system is correct, it rarely could matter to a proof, and it 
would be fairly easy to point out the rare exceptions.

Yes, you could write a case statement instead of using dispatching. Your 
program maintenance costs will skyrocket (having to rewrite all of those 
cases and reprove everything every time a new object type is added). Unless 
your program never changes after it's constructed, which is not remotely the 
case for anything I work on.

> (Personally I wouldn't want to write a compiler at all .....)

Well, there's the problem. :-) Real programmers always want to write a 
compiler (and already have written several). [Not necessarily for a language 
the size of Ada, though. That requires a form of insanity. ;-)]

                                        Randy.