Re: Silly and stupid post-condition or not ?

[BrianG <me@null.email>]

On 02/05/2012 01:18 AM, Randy Brukardt wrote:
> "Phil Thornley"<phil.jpthornley@gmail.com>  wrote in message
> news:MPG.29972ec7befb6ae9989682@news.zen.co.uk...
>>> ... (I do see signs that this is changing, finally, but I think a lot of
>>> the work should have been done years ago.)
>>
>> It would be interesting to have some examples of what you have in mind
>> here.
>
> People forget that Ada uses "access types" rather than "pointers", and the
> reason for that is that access types are type-safe (in the absence of
> erroneous execution, anyway). When you have type-safety, you know a lot
> about what an individual access value can and (more importantly) cannot
> point at. That can be used in a compiler optimizer to prove
> non-interference, among other things. I'd be surprised if similar
> information couldn't be used in proof systems.
>
> Another area is similar: the profile and contract of a subprogram. Even when
> subprograms are dynamically selected (with access-to-subprogram values or
> dynamic dispatching), many of the details of the called subprogram are
> known. Strengthen that contract even further, and it should be possible to
> prove most properties of both sides of the call without knowing anything
> significant about exactly *what* subprogram is actually called. (If all of
> the subprograms have been proven to conform to the contract, and all
> existing calls have been proven to conform to the contract, then dynamic
> calls (dispatching and access values) are safe.
>
> Finally, it's perfectly reasonable to prove useful things about exceptions.
> I've heard people say that's impossible because you get a combinational
> explosion. But I know that's not really true; a compiler optimizer has to
> deal with this and its just adding a single edge to each basic block. And it
> could even be simplified more for a program improvement tool by detecting
> and rejecting programs that violate the 11.6 rules for use of objects after
> an exception. Such programs aren't portable anyway, so they should be
> detected and eliminated anyway. Ada compilers can't do this, of course (such
> programs being legal but ill-defined; we still have to produce something for
> any legal program).
>
> Of course, everything I've talked about requires knowing that there is no
> erroneousness and no 11.6 violations. This it probably the hard part, but it
> seems to be the first job necessary to make a truly usable proof system
> (detect and reject all programs that contain any erroneousness or other
> problems). Again, this is not something that an Ada compiler can do, since
> such programs are legal but not portable.
>
> One imagines that you'd have to eliminate a few Ada features from
> consideration (abort and it's cousin ATC come to mind), and possible require
> the use of storage pools that detect dangling pointers (Ada 2012 gives a
> program the possibility of preventing use of the standard storage pool, so
> using an alternative is safer).
>
> Anyway, I know that there is a lot that can be done that hasn't. Of course,
> none of this is easy (if it was, it all would have been done years ago by
> some hobbyest :-).
>
>                                               Randy.
>
>
It sounds like you don't want SPARK (as it is now, at least), but 
something like an Ada equivalent to LINT.  (Not an Ada version of lint, 
but something that does for Ada what lint does for C - covers Ada's 
needs, rather than C's.)

-- 
---
BrianG
000
@[Google's email domain]
.com