Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 23.06.12 01:08, Dmitry A. Kazakov wrote:
>> And Ada*always*  has had dynamic preconditions:
>> >
>> >       procedure New_Line (Spacing : in Positive_Count := 1);
> The precondition here is Spacing in Positive_Count'Base because the
> behavior of New_Line is*defined*  when Spacing is not in
> Positive_Count'Range.
>
>     New_Line(0)
>
> is a*legal*  Ada program.
  
The behavior of New_Line is not relevant, because New_Line's body
is not performed when "Spacing not in Positive_Count". New_Line does not
behave, because it can't; it also does not propagate anything from its
body. The program does behave without New_Line being called.
But that's the point.

Although there is a post-state in the program, the subprogram New_Line
does not get a chance to run, hence cannot establish its (its!)
postcondition.  Its postcondition is conceptually different
from the condition the program is in, at the place after the New_Line
statement.

When New_Line (Spacing) where

  Spacing in Positive_Count'Base

is legal Ada, then still New_Line (Spacing) where

  Spacing not in Positive_Count

is a contract violation, duly noted by an Ada program executing
properly.

The notions of precondition seem to differ.

Looking at assignments of variables before a call and then calling
this set the precondition, and then looking at assignments and exceptions
after the call, if any, and calling that set the postcondition,
is too meaningless and narrow to be equated to DbC.

There are two separate kinds of rules working here.