Re: Exceptions and out procedure arguments (using GNAT GPL)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 21 Jun 2007 11:52:09 +0200, Georg Bauhaus wrote:

> On Wed, 2007-06-20 at 22:40 +0200, Dmitry A. Kazakov wrote:

>> I don't know how often you are using global variables, but if documenting
>> side effects looks ambitious, then you should probably review your
>> programming guidelines.
> 
> I'm not taking this as an argument when your offer is that
> there exists a LRM that says "dynamic semantics". We cannot just
> squeeze a copy of the LRM a bit and expect to have a formal apparatus
> for expressing formal expectations in your *Different-from-DbC*
> *states-plus-exceptions* approach (IIUC),

In which way is it different?

I didn't talk about formal correctness or pre-/postconditions, but if you
bring this topic in. What is so difficult in:

require: ...
   ... Ptr.all ...
ensure: (Ptr=null and Propagated(Constraint_Error)) or ...

>>  See any part of ARM which defines "dynamic semantics" of an operation.
> 
> I think I fail to express myself clearly, as IMHO you talk evasively
> around the real question: What is your formal documentation language,
> with set-of-words = {program variables, pre/post/inv, ...} such that
> a compiler/translator/analysis program can be used as a programmer's
> aid in demonstrating correctness of a program.

Then I probably understood you wrong. What was your objection? A) to
documenting side effects in case of exception propagation, B) to proving
formal correctness of a program in the same case, C) to both?

A or B or C imply a total ban on any exceptions. Clearly, you need not
document anything that cannot happen...

>> For the operation ".all" the *only* correct outcome with the parameter null
>> is propagation Constraint_Error. Note that this also presumes no side
>> effects like:
>> 
>>    X := 4;
>>    Ptr := null;
>>    .. Ptr.all ...;  -- Surprise, this shall not change X!
>> 
>> Is it ambitious to require?
> 
> Will it change Ptr.all?

Yes, if the compiler is broken or else some erroneous execution is
underway.

> Is erroneous execution correct or incorrect, valid or invalid, and how
> does this affect having exceptions a possible values of any type?

This question is meaningless. Erroneous execution does not have this
property. You should specify a program, be it an application program or
then compiler. When the application program enters erroneous execution
where ARM allows this, then the compiler used to compile that program is
correct. When the specification of the application program allows erroneous
execution in the corresponding problem space states, then the program is
correct as well.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de