From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Silly and stupid post-condition or not ?
Date: Sun, 5 Feb 2012 00:18:44 -0600
Date: 2012-02-05T00:18:44-06:00 [thread overview]
Message-ID: <jgl70g$l9i$1@munin.nbi.dk> (raw)
In-Reply-To: MPG.29972ec7befb6ae9989682@news.zen.co.uk
"Phil Thornley" <phil.jpthornley@gmail.com> wrote in message
news:MPG.29972ec7befb6ae9989682@news.zen.co.uk...
> ...
>> I think that things like SPARC can actually be harmful, as they focus
>> attention on the wrong things. There is a lot that can be proved about
>> dynamic constructs in Ada (far more than in other most languages), and it
>> is
>> unfortunate that instead of taking advantage of this (and making widely
>> usable results), most of effort has been on proving the Fortran 66 subset
>> of
>> Ada. (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.
next prev parent reply other threads:[~2012-02-05 6:19 UTC|newest]
Thread overview: 84+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-01-30 23:11 Silly and stupid post‑condition or not ? Yannick Duchêne (Hibou57)
2012-01-31 6:47 ` J-P. Rosen
2012-01-31 18:48 ` Jeffrey Carter
2012-01-31 22:02 ` Yannick Duchêne (Hibou57)
2012-01-31 8:54 ` Dmitry A. Kazakov
2012-01-31 9:35 ` Georg Bauhaus
2012-01-31 10:22 ` Dmitry A. Kazakov
2012-01-31 12:33 ` Georg Bauhaus
2012-01-31 13:52 ` Dmitry A. Kazakov
2012-01-31 15:34 ` Georg Bauhaus
2012-01-31 16:24 ` Dmitry A. Kazakov
2012-01-31 19:44 ` Georg Bauhaus
2012-02-01 8:41 ` Dmitry A. Kazakov
2012-02-01 10:37 ` stefan-lucks
2012-02-01 10:51 ` Yannick Duchêne (Hibou57)
2012-02-01 13:49 ` Yannick Duchêne (Hibou57)
2012-02-01 13:49 ` Dmitry A. Kazakov
2012-02-01 16:37 ` stefan-lucks
2012-02-02 1:50 ` Silly and stupid post�?'condition " Randy Brukardt
2012-02-02 1:56 ` Silly and stupid postâ?'condition or not ? Yannick Duchêne (Hibou57)
2012-02-03 2:45 ` Silly and stupid post�?'condition or not ? Randy Brukardt
2012-02-02 8:25 ` Silly and stupid post‑condition " Dmitry A. Kazakov
2012-02-02 9:01 ` stefan-lucks
2012-02-02 9:18 ` stefan-lucks
2012-02-02 10:04 ` Dmitry A. Kazakov
2012-01-31 22:08 ` Yannick Duchêne (Hibou57)
2012-01-31 17:28 ` Dmitry A. Kazakov
2012-01-31 22:12 ` Yannick Duchêne (Hibou57)
2012-02-01 8:49 ` Dmitry A. Kazakov
2012-02-01 8:36 ` Stephen Leake
2012-02-01 16:30 ` Silly and stupid post-condition " Adam Beneschan
2012-02-02 9:40 ` Stephen Leake
2012-02-02 13:20 ` Georg Bauhaus
2012-02-02 13:35 ` Yannick Duchêne (Hibou57)
2012-02-03 3:13 ` Randy Brukardt
2012-02-03 3:33 ` Yannick Duchêne (Hibou57)
2012-02-03 8:12 ` Simon Wright
2012-02-07 2:29 ` BrianG
2012-02-07 10:43 ` Simon Wright
2012-02-08 2:25 ` BrianG
2012-02-07 21:15 ` Robert A Duff
2012-02-03 9:11 ` Dmitry A. Kazakov
2012-02-04 3:27 ` Randy Brukardt
2012-02-04 10:15 ` Dmitry A. Kazakov
2012-02-03 12:25 ` Phil Thornley
2012-02-04 9:30 ` Phil Thornley
2012-02-04 12:02 ` Phil Thornley
2012-02-05 6:18 ` Randy Brukardt [this message]
2012-02-05 10:23 ` Phil Thornley
2012-02-05 10:55 ` Yannick Duchêne (Hibou57)
2012-02-05 15:03 ` Robert A Duff
2012-02-05 18:04 ` Phil Thornley
2012-02-05 21:27 ` Robert A Duff
2012-02-05 23:09 ` Phil Thornley
2012-02-07 2:05 ` Randy Brukardt
2012-02-07 9:38 ` Dmitry A. Kazakov
2012-02-05 11:31 ` Yannick Duchêne (Hibou57)
2012-02-05 14:50 ` Robert A Duff
2012-02-07 2:11 ` Randy Brukardt
2012-02-07 2:34 ` BrianG
2012-02-07 4:38 ` Yannick Duchêne (Hibou57)
2012-02-09 3:10 ` Randy Brukardt
2012-02-04 23:07 ` Stephen Leake
2012-02-05 2:49 ` Yannick Duchêne (Hibou57)
2012-02-05 6:29 ` Randy Brukardt
2012-02-05 11:40 ` Yannick Duchêne (Hibou57)
2012-02-07 1:36 ` Randy Brukardt
2012-02-05 15:16 ` Robert A Duff
2012-02-06 4:56 ` Yannick Duchêne (Hibou57)
2012-02-06 14:39 ` Robert A Duff
2012-02-06 16:12 ` Yannick Duchêne (Hibou57)
2012-02-07 1:46 ` Randy Brukardt
2012-02-07 17:24 ` Robert A Duff
2012-02-03 6:26 ` J-P. Rosen
2012-02-03 9:12 ` Dmitry A. Kazakov
2012-02-03 9:48 ` Yannick Duchêne (Hibou57)
2012-02-03 11:09 ` Dmitry A. Kazakov
2012-02-03 11:40 ` Yannick Duchêne (Hibou57)
2012-02-03 13:18 ` Dmitry A. Kazakov
2012-02-03 14:14 ` Yannick Duchêne (Hibou57)
2012-02-03 14:45 ` Dmitry A. Kazakov
2012-02-04 3:16 ` Randy Brukardt
2012-02-04 6:27 ` Yannick Duchêne (Hibou57)
2012-02-04 10:47 ` Dmitry A. Kazakov
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox