From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: Silly and stupid post-condition or not ?
Date: Sun, 5 Feb 2012 10:23:06 -0000
Date: 2012-02-05T10:23:06+00:00 [thread overview]
Message-ID: <MPG.299868e7ebbd43b1989683@news.zen.co.uk> (raw)
In-Reply-To: jgl70g$l9i$1@munin.nbi.dk
In article <jgl70g$l9i$1@munin.nbi.dk>, randy@rrsoftware.com says...
>
> "Phil Thornley" <phil.jpthornley@gmail.com> wrote in message
> news:MPG.29972ec7befb6ae9989682@news.zen.co.uk...
> > ...
> > 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.
The original SPARK Rationale says: "All Ada features which require
dynamic storage allocation were ruled out, for several reasons. The
specification and modelling of access type manipulations, which can
involve aliasing, is extremely difficult; for programs using access
types it may also be very difficult to achieve security ..., let alone
verification."
Remember that everything in a SPARK program must have a name, and that
it is quite easy to implement dynamic storage for a single type by a
simple array (access value <-> array index). Furthermore when dealing
with dynamically sized data structures the invariant typically needs to
include predicates for the storage space that is not currently in use as
well as the storage that is.
>
> 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.
I guess here that the issue is complexity of implementation versus gain
in expressibility. All that the SPARK programmer has to do is to create
the appropriate case statement. Yes, this does create an additional
maintenance task, but No, it does not (have to) spoil the clarity of the
calling code. (A common SPARK idiom is to use locally defined
parameterless subprograms - since accessing data globally is no
different to access via a parameter - so you just hide the case
statement away in one of these.)
>
> 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).
The SPARK Rationale says: "Exceptions, designed for dealing with errors
or other exceptional situations, might at first sight seem very
desirable for safety-critical programming. However, it is easier and
more satisfactory to write a program which is exception-free, and prove
it to be so, than to prove that the corrective action performed by
exception-handlers would be appropriate under all possible
circumstances; if checks with recovery actions are required in a
program, these can be introduced without resorting to exception
handlers, and in general the embedded code will be easier to verify.
Since exception-handling also seriously complicates the formal
definition of even the sequential part of Ada we believe it should be
omitted."
There is a huge advantage in compiling a program with all checks
suppressed - because the validation must deal with all executable paths
in the object code, not just the source code.
Support for user defined exceptions is probably one of the enhancements
I would most like to have in SPARK - to eliminate all those "Success"
parameters that you otherwise need.
>
> 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 :-).
A final quote from the Rationale:
"Of course, the extent to which Ada must be simplified for high-
integrity programming will be a matter of opinion: our preoccupation
with simplicity is based on experience of what can be achieved with a
high degree of confidence in practice, rather than what can be proved in
principle.
Pedagogical considerations also suggest to us that drastic
simplifications must be made. Safety-critical work demands complete
mastery of a programming language, so that the programmer can
concentrate on what he or she wants to say rather than struggle with the
means of expression."
Cheers,
Phil
next prev parent reply other threads:[~2012-02-05 10:23 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
2012-02-05 10:23 ` Phil Thornley [this message]
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