Class wide preconditions: error in the Ada 2012 Rationale?

Class wide preconditions: error in the Ada 2012 Rationale?

[Yannick Duchêne (Hibou57)]

I have a doubt, and this one disturb me, so this topic.

I was reading the revised version (fourth draft) of the Ada 2012  
Rationale, when I saw this:

> However, the rules regarding preconditions are perhaps surprising.
> The specific precondition Pre for Equilateral_Triangle must be true 
> (checked in the body) but so long as just one of the class wide 
> preconditions Pre'Class for Object and Triangle is true then all iswell.

Then later, a summary of the rule:

> In summary, class wide preconditions are checked at the point of call. 
> Class wide postconditions and both specific pre- and postconditionsare  
> checked in the actual body.

I believe either my understanding is wrong, or the Rationale is wrong. The  
above statements are not compatible with the substitution principle. What  
if a sub‑program expects a a class wide type with a root type and its  
precondition, and get a derived type with a specific precondition it can't  
know about?

There may be a comment on that point, see below, but first, an example  
test, compiled with GNAT:


     with Ada.Text_IO;

     procedure Ex
     is
        package P1 is

           type T is interface;
           Condition : Boolean;

           procedure P (E : T) is abstract
           with Pre'Class => P1.Condition;
        end;

        package P2 is

           type T is interface and P1.T;
           Condition : Boolean;

           overriding
           procedure P (E : T) is abstract
           with Pre'Class => P2.Condition;
        end;

        package P3 is

           type T is new P2.T with null record;
           Condition : Boolean;

           overriding
           procedure P (E : T)
           with Pre'Class => P3.Condition;
        end;

        package body P3 is
           procedure P (E : T)
           is begin
              Ada.Text_IO.Put_Line ("You're OK!");
           end;
        end;

        E : P3.T;
     begin
        P1.Condition := True;
        P2.Condition := True;
        P3.Condition := True; -- Hint: try to set this to `False`.
        E.P;
     end Ex;


Side‑note: the package prefix added to access the condition in the  
“Pre'Class”, are not strictly required, but required with GNAT to bypass  
one of its bug.

Test this example modifying each of the conditions: it `P3.Condition` is  
set to `False`, there won't be any error at runtime, and you'll be OK,  
although `P3.Condition` is the specific precondition for the concrete  
implementation. It will fails only if all preconditions are false. No  
specific precondition seems to be checked in the body of `P`, or else it  
would trigger an exception when `P3.Condition` is set to `False`.

GNAT's interpretation is compatible with my own, and does not seems to be  
compatible with the one from the Rationale.

But there may be a trick? Let's try turning `E.P;` into `P3.P (E);`: same  
result. Not let's try turning `P3.P (E);` into `P3.P (P3.T'(E));`: same  
result. GNAT does not know about anything like specific precondition, and  
I'm OK with GNAT this time.

So is this me not understanding the Rationale? Or the Rationale has either  
wrong or unclear words?


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Class wide preconditions: error in the Ada 2012 Rationale?

[Yannick Duchêne (Hibou57)]

Le Mon, 05 Nov 2012 21:41:48 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> I have a doubt, and this one disturb me, so this topic.
>
> I was reading the revised version (fourth draft) of the Ada 2012  
> Rationale, when I saw this:
>
>> However, the rules regarding preconditions are perhaps surprising.
>> The specific precondition Pre for Equilateral_Triangle must be true 
>> (checked in the body) but so long as just one of the class wide 
>> preconditions Pre'Class for Object and Triangle is true then all iswell.
>
> Then later, a summary of the rule:
>
>> In summary, class wide preconditions are checked at the point of call. 
>> Class wide postconditions and both specific pre- and postconditionsare  
>> checked in the actual body.
>

Oh no! I forget the link:
http://www.ada-auth.org/standards/12rat/html/Rat12-2-3.html

Pardon me.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Class wide preconditions: error in the Ada 2012 Rationale?

[sbelmont700]

On Monday, November 5, 2012 3:41:57 PM UTC-5, Hibou57 (Yannick Duchêne) wrote:
> 
> I believe either my understanding is wrong, or the Rationale is wrong. The  
> 
> above statements are not compatible with the substitution principle. What  
> 
> if a sub-program expects a a class wide type with a root type and its  
> 
> precondition, and get a derived type with a specific precondition it can't  
> 
> know about?
> 

A foundation of the LSP is that you should not be strengthening preconditions for derived types.  After all, when you substitue a child for a parent, you cannot know anything about the child, which includes any additional preconditions that have been added.  If classwide preconditions are checked at the point of the call, then it might dispatch to subprograms with preconditions that haven't even been written yet (that it clearly cannot check beforehand).

-sb

Re: Class wide preconditions: error in the Ada 2012 Rationale?

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2025 bytes --]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.wnbifyvyule2fv@cardamome...
>I have a doubt, and this one disturb me, so this topic.
>
...
>> In summary, class wide preconditions are checked at the point of call. 
>> Class wide postconditions and both specific pre- and postconditionsare 
>> checked in the actual body.
>
>I believe either my understanding is wrong, or the Rationale is wrong.

The above is correct.

> The above statements are not compatible with the substitution principle.

*Specific* preconditions and postconditions are not necessarily compatible 
with the substitution principle. If you want that, you either have to be 
careful what you write, or (better IMHO) use only class-wide preconditions 
and postconditions.

You don't always want strict LSP, and using specific preconditions gives you 
a way to get that when needed. But of course, in that case, dispatching 
calls may fail for no reason visible at the point of the call. (LSP = Liskov 
Substitutability Principle).

> What if a sub-program expects a a class wide type with a root type and its 
> precondition, and get a derived type with a specific precondition it can't 
> know about?

You still evaluate the specific precondition associated with the subprogram 
that is actually called.

My understanding is that a lot of GNAT users only use carefully written 
specific preconditions (probably because they learned how to do that before 
class-wide preconditions existed in GNAT). Those can be, but don't have to, 
follow LSP. OTOH, class-wide preconditions follow LSP by design.

My rule of thumb is that in a given derivation chain, you should only use 
one or the other. (I wanted to make that a requirement, but that was shot 
down.)

I think given the sorts of programs that you write, you should only use 
class-wide preconditions and postconditions, and forget that specific ones 
exist at all. In which case, you won't have a problem with LSP.

                                       Randy.

Re: Class wide preconditions: error in the Ada 2012 Rationale?

[Yannick Duchêne (Hibou57)]

Le Fri, 09 Nov 2012 01:57:51 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> My rule of thumb is that in a given derivation chain, you should only use
> one or the other.
I fully agree, and was thinking of the same conclusion.

> (I wanted to make that a requirement, but that was shot down.)
How shot down? (if the question is not too much inquisitive)


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Class wide preconditions: error in the Ada 2012 Rationale?

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 695 bytes --]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.wnhfv7yjule2fv@cardamome...
Le Fri, 09 Nov 2012 01:57:51 +0100, Randy Brukardt <randy@rrsoftware.com>
a �crit:
>> (I wanted to make that a requirement, but that was shot down.)
>How shot down? (if the question is not too much inquisitive)

I don't recall the details, but I think most people wanted as few 
restrictions as possible. "Methodological restrictions" have a bad history 
in Ada, and thus we often avoid them. Clearly a tool like AdaControl can 
enforce style rules beyond those the language requires, and that was thought 
to be the best option here.

                                 Randy.