Silly and stupid post‑condition or not ?

Silly and stupid post‑condition or not ?

[Yannick Duchêne (Hibou57)]

Hi people out there,

A matter of style or more than style.

I wanted to add a post‑condition to a function to make its specification  
more predictive. The function returns a type à la SML, i.e. instead of a  
boolean status on failure along with an undefined value, it returns a  
record containing nothing. There is an obvious case where it is sure to  
fail, so I wanted to express this obvious behavior in a post‑condition.  
But I can't make up my mind, can't clearly feel if that's simply silly and  
useless wast of source or else.

May I request for your opinion on the simple sample please ? The main  
point is on the function post‑condition at the end.


    type Parsed_Type (Status : Parsed_Status_Type) is record
       case Status is
          when Parsed =>
             Instance : Instance_Type;
          when Format_Error =>
             null;
       end case;
    end record; -- Parsed_Type

    function Parsed (S : String) return Parsed_Type
       with Post =>
         (if S'Length not in Image_Length_Type then
             Parsed'Result.Status = Format_Error);
          -- There may be other failure conditions.


Is such a post‑condition a good or bad practice in your humble or  
authoritative opinion ?

Keep in mind there may be many other cases where “Parsed'Result.Status =  
Format_Error” could be True; the one in the Post is not the only possible  
one.


-- 
“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: Silly and stupid post‑condition or not ?

[J-P. Rosen]

Le 31/01/2012 00:11, Yannick Duchêne (Hibou57) a écrit :
> Is such a post‑condition a good or bad practice in your humble or
> authoritative opinion ?
> 
1) There is not stupid question

2) A precondition expresses what you require from the user of your
package. A postcondition is what you promise to the user. The important
point is that these conditions are part of the specification - visible.

Like any check (including simple constraints), conditions have no effect
whatsoever on a working program (presuming such a thing exists). It
helps during program development by having exceptions raised closer to
the cause of the problem, and work as kinds of lemma, intermediate steps
that help to make program proofs.

Is this particular one useful? If you think that it is a property of
your subprogram that should be made explicit to the user, yes. If you
think it is just a redundant property that only repeats the properties
of the specification, no. Really a matter of appreciation.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:

>     function Parsed (S : String) return Parsed_Type
>        with Post =>
>          (if S'Length not in Image_Length_Type then
>              Parsed'Result.Status = Format_Error);
>           -- There may be other failure conditions.
> 
> 
> Is such a post‑condition a good or bad practice in your humble or  
> authoritative opinion ?

I would say it would be a bad practice. The reason is that IMO the
postcondition must be complete, it must tell all truth or nothing. Your
prostcondition is a partial truth, it does not describe all cases when
Status is mandated to be Format_Error.

Yes, it boils down to the implied semantics of the postconditions. If you
consider them mere comments occasionally breaking the program execution by
throwing exceptions at random, then your example might fit into that model.
If you rather view them as contracts, then good contracts should have no
holes.

Note that it is not necessarily about how detailed the semantics is to be
described by pre-/postconditions. I mean, there is a space between
pre-/postconditions suitable for correctness proofs and ones which don't.
You can have the latter if you wish, but still it must be complete. In your
case such a loose postcondition would actually be:

   Status = Format_Error if something is wrong

If you cannot spell that using available means then don't.

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

Re: Silly and stupid post‑condition or not ?

[Georg Bauhaus]

On 31.01.12 09:54, Dmitry A. Kazakov wrote:
> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:
>
>>      function Parsed (S : String) return Parsed_Type
>>         with Post =>
>>           (if S'Length not in Image_Length_Type then
>>               Parsed'Result.Status = Format_Error);
>>            -- There may be other failure conditions.
>>
>>
>> Is such a post‑condition a good or bad practice in your humble or
>> authoritative opinion ?
>
> I would say it would be a bad practice. The reason is that IMO the
> postcondition must be complete, it must tell all truth or nothing. Your
> prostcondition is a partial truth, it does not describe all cases when
> Status is mandated to be Format_Error.

One way to express a "hints only" postcondition is

   with Post => True or  -- yes, mathniks, just FTR:
     (if ... then ...

The idea is that the partial truth, in the shape of a
formal note, can later lead to an improved program
structure.

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Tue, 31 Jan 2012 10:35:35 +0100, Georg Bauhaus wrote:

> On 31.01.12 09:54, Dmitry A. Kazakov wrote:
>> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:
>>
>>>      function Parsed (S : String) return Parsed_Type
>>>         with Post =>
>>>           (if S'Length not in Image_Length_Type then
>>>               Parsed'Result.Status = Format_Error);
>>>            -- There may be other failure conditions.
>>>
>>>
>>> Is such a post‑condition a good or bad practice in your humble or
>>> authoritative opinion ?
>>
>> I would say it would be a bad practice. The reason is that IMO the
>> postcondition must be complete, it must tell all truth or nothing. Your
>> prostcondition is a partial truth, it does not describe all cases when
>> Status is mandated to be Format_Error.
> 
> One way to express a "hints only" postcondition is
> 
>    with Post => True or  -- yes, mathniks, just FTR:
>      (if ... then ...
> 
> The idea is that the partial truth, in the shape of a
> formal note, can later lead to an improved program
> structure.

Apply your idea to the case statement:

case Char is
   when 'A' => Put_Line ("Got A");
end case;

Fortunately Ada compiler would not let you further "improving" this program
structure, just rejecting the program. Such a nasty math-thinking on its
part!

Ada, at least Ada 83, considers program as a whole, trying minimize partial
truths where possible. Because where truth is partial, there is a place for
a lie. And in the case of software lies are always complete lies.

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

Re: Silly and stupid post‑condition or not ?

[Georg Bauhaus]

On 31.01.12 11:22, Dmitry A. Kazakov wrote:
> On Tue, 31 Jan 2012 10:35:35 +0100, Georg Bauhaus wrote:
> 
>> On 31.01.12 09:54, Dmitry A. Kazakov wrote:
>>> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:
>>>
>>>>      function Parsed (S : String) return Parsed_Type
>>>>         with Post =>
>>>>           (if S'Length not in Image_Length_Type then
>>>>               Parsed'Result.Status = Format_Error);
>>>>            -- There may be other failure conditions.
>>>>
>>>>
>>>> Is such a post‑condition a good or bad practice in your humble or
>>>> authoritative opinion ?
>>>
>>> I would say it would be a bad practice. The reason is that IMO the
>>> postcondition must be complete, it must tell all truth or nothing. Your
>>> prostcondition is a partial truth, it does not describe all cases when
>>> Status is mandated to be Format_Error.
>>
>> One way to express a "hints only" postcondition is
>>
>>    with Post => True or  -- yes, mathniks, just FTR:
>>      (if ... then ...
>>
>> The idea is that the partial truth, in the shape of a
>> formal note, can later lead to an improved program
>> structure.
> 
> Apply your idea to the case statement:
> 
> case Char is
>    when 'A' => Put_Line ("Got A");
> end case;

I was only picking up the idea that a case statement's completeness
is decidable and postconditions aren't. Nor need they be. Yet, incomplete
information ("lies") can add value to the "about" part of the
annotated thing. Until the formalists succeed in making the
program better ("correct" WRT a set of decidable hypotheses),
that's something.

If aspects are misused to make an impression, to produce a cover-up
of premature (non-)design, then that's not different form using
something more complete: a decidable cover-up does not change
the premature state (the "lie") of the software. It just is a formally
more correct lie. :-)

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Tue, 31 Jan 2012 13:33:41 +0100, Georg Bauhaus wrote:

> On 31.01.12 11:22, Dmitry A. Kazakov wrote:
>> On Tue, 31 Jan 2012 10:35:35 +0100, Georg Bauhaus wrote:
>> 
>>> On 31.01.12 09:54, Dmitry A. Kazakov wrote:
>>>> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:
>>>>
>>>>>      function Parsed (S : String) return Parsed_Type
>>>>>         with Post =>
>>>>>           (if S'Length not in Image_Length_Type then
>>>>>               Parsed'Result.Status = Format_Error);
>>>>>            -- There may be other failure conditions.
>>>>>
>>>>>
>>>>> Is such a post‑condition a good or bad practice in your humble or
>>>>> authoritative opinion ?
>>>>
>>>> I would say it would be a bad practice. The reason is that IMO the
>>>> postcondition must be complete, it must tell all truth or nothing. Your
>>>> prostcondition is a partial truth, it does not describe all cases when
>>>> Status is mandated to be Format_Error.
>>>
>>> One way to express a "hints only" postcondition is
>>>
>>>    with Post => True or  -- yes, mathniks, just FTR:
>>>      (if ... then ...
>>>
>>> The idea is that the partial truth, in the shape of a
>>> formal note, can later lead to an improved program
>>> structure.
>> 
>> Apply your idea to the case statement:
>> 
>> case Char is
>>    when 'A' => Put_Line ("Got A");
>> end case;
> 
> I was only picking up the idea that a case statement's completeness
> is decidable and postconditions aren't.

The case statement was designed with a mindset opposite to this idea. This
is why the alternatives of a case are required to be static, why the choice
cannot be a class-wide object.

> Nor need they be.

So are the alternatives of case. In other languages alternatives are tested
in the order of their appearance, no big deal, they say.

> Yet, incomplete
> information ("lies") can add value to the "about" part of the
> annotated thing.

Incomplete information /= exhaustiveness. Considering paraconsistent,
fuzzy, probabilistic and other logics used to handle unknown things, they
long for all alternatives to be specified even more than the conventional
logic does. In order to infer anything useful in such a logic, you need to
know something about both A and not A, since A or not A is no more true
(the law of excluded middle fails).

Using the example of the case statement, all incomplete information is
concentrated in the value of the choice. There is nothing incomplete in the
case's alternatives.

Take another example, let you see:

   x := 1;

The information about x is incomplete. You know that it could probably
accommodate the value 1, and that is. You may argue at nausea that this
"adds value", but that is not Ada, which requires the type of x manifested
before its use. And what does a type declaration? It lists all possible
values of x, exhaustively. Again, there are languages that take a different
path, so my comment is Ada's POV, of course.

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

Re: Silly and stupid post‑condition or not ?

[Georg Bauhaus]

On 31.01.12 14:52, Dmitry A. Kazakov wrote:

> Take another example, let you see:
> 
>    x := 1;
> 
> The information about x is incomplete. You know that it could probably
> accommodate the value 1, and that is. You may argue at nausea that this
> "adds value", but that is not Ada, which requires the type of x manifested
> before its use. And what does a type declaration? It lists all possible
> values of x, exhaustively. Again, there are languages that take a different
> path, so my comment is Ada's POV, of course.
> 

OK, I see, even though the claim of Ada's POV is seems
biased, see below. -- I will not presume any kind of formal logic when
watching people judge software systems. We just say words and argue,
referring to other things that seem relevant when discussing software
systems. Words like "LRM" or "Ariane" or "engineering" or "constructivism"
or "deadlines" or "cost" or "DRY", etc.

The program below is also an example of Ada's POV. Alas, it exhibits
the least desirable state of things. It must be Ada's POV,
since the program is legal, is simple, and uses perfectly usual
statements.  Its effect is, however, unpredictable at any level
of precision, because Ada does *not*, by default, require that variables
be initialized. (And no exception propagates out of T_IO if X
happens to be in T'Base, IINM.)  One might say "predictable
with precision" is still true when this label is attached to
some set of all possible effects. But this doesn't sound right.

Anyway, Ada's POV still requires (a) programmers to do
the right thing, and (b) requires us to make good guesses as to
what this right thing might be.  In the program below, it might have
been to see what the bits at X'Address happen to be.

Notice that the declarations list the possible values, exhaustively.

with Ada.Text_IO;

procedure Ada_POV is

   use Ada.Text_IO;

   type T is range 1 .. 10;
   package T_IO is new Integer_IO (T);

   X : T;  -- perfectly legal from Ada's POV
begin
   Put ("X is "); T_IO.Put (X); New_Line;
end Ada_POV;

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Tue, 31 Jan 2012 16:34:23 +0100, Georg Bauhaus wrote:

> The program below is also an example of Ada's POV.

I fail to see your point. Are you arguing that uninitialized variables are
good, add value, illustrate the ideas behind Ada's design?

They are tolerated. It was said on many occasions before, that a better Ada
should have required all variables initialized by default. Leaving a
variable or member component uninitialized should better have had a special
syntax, There are other cases in Ada when the default is unsafe. Should we
multiply these cases?

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

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duch�ne (Hibou57) wrote:

>     type Parsed_Type (Status : Parsed_Status_Type) is record
>        case Status is
>           when Parsed =>
>              Instance : Instance_Type;
>           when Format_Error =>
>              null;
>        end case;
>     end record; -- Parsed_Type
> 
>     function Parsed (S : String) return Parsed_Type
>        with Post =>
>          (if S'Length not in Image_Length_Type then
>              Parsed'Result.Status = Format_Error);
>           -- There may be other failure conditions.

Returning the discussion from the astral spheres back to the topic. A 
better design could be to split Format_Error into Length_Error and other 
errors. Then for Parsed the postcondition would become complete for one 
case: if and only if S'Length not in Image_Length_Type then the result is 
Length_Error.

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

Re: Silly and stupid post‑condition or not ?

[Jeffrey Carter]

On 01/30/2012 11:47 PM, J-P. Rosen wrote:
>
> Is this particular one useful? If you think that it is a property of
> your subprogram that should be made explicit to the user, yes. If you
> think it is just a redundant property that only repeats the properties
> of the specification, no. Really a matter of appreciation.

The condition in question looks more like a precondition than a postcondition to me:

with Pre => S'Length in Image_Length_Type

-- 
Jeff Carter
"Brave Sir Robin ran away."
Monty Python and the Holy Grail
59

--- Posted via news://freenews.netfront.net/ - Complaints to news@netfront.net ---

Re: Silly and stupid post‑condition or not ?

[Georg Bauhaus]

On 31.01.12 17:24, Dmitry A. Kazakov wrote:
> On Tue, 31 Jan 2012 16:34:23 +0100, Georg Bauhaus wrote:
>
>> The program below is also an example of Ada's POV.
>
> I fail to see your point.

The point is that from Ada's POV, there is a preference
for detecting many things early. But this preference does
not mean that all things would be detected by the compiler,
or should be detected by the compiler.
Ada provides for things checked at run-time, allowing
programs to be written that can only be written because
some amount of information need not be present at compile
time.

Ada does allow writing if statements without else part. Thus
suppose the argument is that a postcondition should either
state everything or, if this is not feasible, state nothing
at all (True). From Ada's POV, then,  nothing should ever
be implicit, or unspoken.  All if-statements should really
be case-statements without "when others". Though shalt not
write "if" without also stating what "else" should happen.

Not saying that deferring until run-time, or leaving out
the "else" part, is always a good idea, but given what
Ada is, the motto all-or-nothing is not Ada's POV, IMHO.
Hence, there is a mode of writing postcondition that lacks
rigor but still reduces the risk of errors, by reducing
their number, by informing the client programmer. Obviously,
there are uses of Ada where one wants
   Count (Number_of_Errors) in Boolean.
I cannot really think of a way the language can hope to do
more than encourage this relation.

Re: Silly and stupid post‑condition or not ?

[Yannick Duchêne (Hibou57)]

Le Tue, 31 Jan 2012 19:48:19 +0100, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:

> On 01/30/2012 11:47 PM, J-P. Rosen wrote:
>>
>> Is this particular one useful? If you think that it is a property of
>> your subprogram that should be made explicit to the user, yes. If you
>> think it is just a redundant property that only repeats the properties
>> of the specification, no. Really a matter of appreciation.
>
> The condition in question looks more like a precondition than a  
> postcondition to me:
>
> with Pre => S'Length in Image_Length_Type

I understand your point, but no, this is not a precondition, as the  
condition will not raise an exception. Although an error status may be  
returned, this error status is a legal result here.

-- 
“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: Silly and stupid post‑condition or not ?

[Yannick Duchêne (Hibou57)]

Le Tue, 31 Jan 2012 13:33:41 +0100, Georg Bauhaus  
<rm.dash-bauhaus@futureapps.de> a écrit:

> On 31.01.12 11:22, Dmitry A. Kazakov wrote:
>> On Tue, 31 Jan 2012 10:35:35 +0100, Georg Bauhaus wrote:
>>
>>> On 31.01.12 09:54, Dmitry A. Kazakov wrote:
>>>> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:
>>>>
>>>>>      function Parsed (S : String) return Parsed_Type
>>>>>         with Post =>
>>>>>           (if S'Length not in Image_Length_Type then
>>>>>               Parsed'Result.Status = Format_Error);
>>>>>            -- There may be other failure conditions.
>>>>>
>>>>>
>>>>> Is such a post‑condition a good or bad practice in your humble or
>>>>> authoritative opinion ?
>>>>
>>>> I would say it would be a bad practice. The reason is that IMO the
>>>> postcondition must be complete, it must tell all truth or nothing.  
>>>> Your
>>>> prostcondition is a partial truth, it does not describe all cases when
>>>> Status is mandated to be Format_Error.
>>>
>>> One way to express a "hints only" postcondition is
>>>
>>>    with Post => True or  -- yes, mathniks, just FTR:
>>>      (if ... then ...
>>>
>>> The idea is that the partial truth, in the shape of a
>>> formal note, can later lead to an improved program
>>> structure.
>>
>> Apply your idea to the case statement:
>>
>> case Char is
>>    when 'A' => Put_Line ("Got A");
>> end case;
>
> I was only picking up the idea that a case statement's completeness
> is decidable and postconditions aren't. Nor need they be. Yet, incomplete
> information ("lies") can add value to the "about" part of the
> annotated thing. Until the formalists succeed in making the
> program better ("correct" WRT a set of decidable hypotheses),
> that's something.

You both got it. I was exactly hesitating between Dmitry's comment and  
yours and had both in mind.

-- 
“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: Silly and stupid post‑condition or not ?

[Yannick Duchêne (Hibou57)]

Le Tue, 31 Jan 2012 18:28:54 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote:
>
>>     type Parsed_Type (Status : Parsed_Status_Type) is record
>>        case Status is
>>           when Parsed =>
>>              Instance : Instance_Type;
>>           when Format_Error =>
>>              null;
>>        end case;
>>     end record; -- Parsed_Type
>>
>>     function Parsed (S : String) return Parsed_Type
>>        with Post =>
>>          (if S'Length not in Image_Length_Type then
>>              Parsed'Result.Status = Format_Error);
>>           -- There may be other failure conditions.
>
> Returning the discussion from the astral spheres back to the topic. A
> better design could be to split Format_Error into Length_Error and other
> errors. Then for Parsed the postcondition would become complete for one
> case: if and only if S'Length not in Image_Length_Type then the result is
> Length_Error.

Could be an idea if the program could make use of this extra information.  
But it won't, a program won't fix an erroneous image received as input,  
and a Length_Error will result in the same behavior as with a Format_Error  
result.

-- 
“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: Silly and stupid post‑condition or not ?

[Stephen Leake]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

>    type Parsed_Type (Status : Parsed_Status_Type) is record
>       case Status is
>          when Parsed =>
>             Instance : Instance_Type;
>          when Format_Error =>
>             null;
>       end case;
>    end record; -- Parsed_Type
>
>    function Parsed (S : String) return Parsed_Type
>       with Post =>
>         (if S'Length not in Image_Length_Type then
>             Parsed'Result.Status = Format_Error);
>          -- There may be other failure conditions.
>
>
> Is such a post‑condition a good or bad practice in your humble or
> authoritative opinion ?
>
> Keep in mind there may be many other cases where “Parsed'Result.Status
> = Format_Error” could be True; the one in the Post is not the only
> possible  one.

That means the post condition is misleading, and therefore bad.

--
-- Stephe

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Tue, 31 Jan 2012 20:44:07 +0100, Georg Bauhaus wrote:

> On 31.01.12 17:24, Dmitry A. Kazakov wrote:
>> On Tue, 31 Jan 2012 16:34:23 +0100, Georg Bauhaus wrote:
>>
>>> The program below is also an example of Ada's POV.
>>
>> I fail to see your point.
> 
> The point is that from Ada's POV, there is a preference
> for detecting many things early. But this preference does
> not mean that all things would be detected by the compiler,
> or should be detected by the compiler.

Don't mix undecidable things with undefined ones. That pre-/postconditions
should have been decidable is another story. This train has already left. 

But that seems not bad enough. To make the disaster complete, it should
become undefined as well. Right?

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

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Tue, 31 Jan 2012 23:12:57 +0100, Yannick Duch�ne (Hibou57) wrote:

> Le Tue, 31 Jan 2012 18:28:54 +0100, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
> 
>> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duch�ne (Hibou57) wrote:
>>
>>>     type Parsed_Type (Status : Parsed_Status_Type) is record
>>>        case Status is
>>>           when Parsed =>
>>>              Instance : Instance_Type;
>>>           when Format_Error =>
>>>              null;
>>>        end case;
>>>     end record; -- Parsed_Type
>>>
>>>     function Parsed (S : String) return Parsed_Type
>>>        with Post =>
>>>          (if S'Length not in Image_Length_Type then
>>>              Parsed'Result.Status = Format_Error);
>>>           -- There may be other failure conditions.
>>
>> Returning the discussion from the astral spheres back to the topic. A
>> better design could be to split Format_Error into Length_Error and other
>> errors. Then for Parsed the postcondition would become complete for one
>> case: if and only if S'Length not in Image_Length_Type then the result is
>> Length_Error.
> 
> Could be an idea if the program could make use of this extra information.  
> But it won't, a program won't fix an erroneous image received as input,  
> and a Length_Error will result in the same behavior as with a Format_Error  
> result.

What is the point in exempting it in the postcondition? The Georg's idea:
do what looks simple enough and ignore the rest, maybe nobody would ask for
that?

I argue that this attitude is characteristic to bad design. Apart from
thousands other reasons, like leaking implementation details/faults into
the specification etc.

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

Re: Silly and stupid post‑condition or not ?

[stefan-lucks]

On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote:

> But that seems not bad enough. To make the disaster complete, it should
> become undefined as well. Right?

This doesn't need to be a disaster. 

1. For the purpose of proving program correctness, you don't necessarily 
need complete postconditions. As a trivial example, consider 

     function F(X: Natural) return Natural 
        with Post => (if (X mod 2) = 1 then ...); 

   We don't have any precondition. For even X, we don't even have a 
   postcondition. But using the partial postcondition we have, we can 
   completely define the semantic behavior of 

     Y := F(X) * (F(X) mod 2); 

   If that is all what we need F for, why should we bother with any 
   postcondition or even X? 

2. Sometimes, it may hard to prove the entire contract. So we will try to 
   prove the "important" requirements in the contract, and try to convince 
   ourselves by conventional means (testing, code review, ...) that other
   requirements are also satisfied. E.g., for a database with confidential 
   and non-confidential data, we be very happy to prove that any response 
   to a query from an unauthorized entity will be derived from 
   non-confidential data only. You have proven your system to be secure!

   A system may be secure but still be not quite functional. E.g., you may 
   further like to prove that the response to a query from an authorized 
   entity will be derived from all data, the confidential and the 
   non-confidential ones. If you can, fine! Otherwise, apply conventional 
   means ... 

   In fact, some relevant contract requirements may actually be hard to 
   specify. What is the "correct" answer in some informational retrieval 
   setting (e.g., when you google for "Dmitry A. Kazakov")? Do you really 
   propose not to formally specify anything, just because we cannot specify 
   everything?

   This is pretty much the same in the real world. When you go to a 
   restaurant and order a meal, you expect a tasty meal. But the end, 
   being "tasty" is ... a matter of taste. If you have no other complaints 
   than "it wasn't to my taste", you still have to pay the bill. Thus, 
   being "tasty" is expected by the customer, but not part of the 
   postcondition. On the other hand, certain  hygienic standards are 
   defined binding laws for all restaurants (in a given country or state). 
   This is actually a postcondition, inherited from the abstract class of 
   "all restaurants in my country". Would you claim that hygienic 
   standards are useless, because you cannot define tasty Ness?

Back to the original poster's question:

>>  function Parsed (S : String) return Parsed_Type
>>     with Post =>
>>       (if S'Length not in Image_Length_Type then
>>           Parsed'Result.Status = Format_Error);
>>        -- There may be other failure conditions.

What is special about that specific failure condition that singles it out 
from all other failure conditions? 

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: Silly and stupid post‑condition or not ?

[Yannick Duchêne (Hibou57)]

Le Wed, 01 Feb 2012 11:37:31 +0100, <stefan-lucks@see-the.signature> a  
écrit:

> On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote:
>
>> But that seems not bad enough. To make the disaster complete, it should
>> become undefined as well. Right?
>
> This doesn't need to be a disaster.
>
> 1. For the purpose of proving program correctness, you don't necessarily
> need complete postconditions. As a trivial example, consider

Will read the remaining of your post later, but for now, I agree with you.  
Post conditions are not even necessarily a matter of correctness, this may  
also be a matter of completing a behavior description. At least here, no  
exception is raised, and it may deals with input from the outside world,  
which can hardly be proved to be always correct.

In the area of correctness however, there is another signature I did not  
quote before, which may talk better to Dmitry. Here is:

    function Image (Instance : Instance_Type) return Image_Type
       with Post =>
         (Parsed (Image'Result).Status = Parsed) and
         (Parsed (Image'Result).Instance = Instance);
       -- Result can always be successfully parsed and the resulting
       -- instance is always equal to the one whose image is returned.

The postcondition for Image, also talks about Parsed behavior. So you have  
an option to ensure correctness, providing a given image was produced by  
the Image function.


-- 
“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: Silly and stupid post‑condition or not ?

[Yannick Duchêne (Hibou57)]

Le Wed, 01 Feb 2012 11:37:31 +0100, <stefan-lucks@see-the.signature> a  
écrit:
> Back to the original poster's question:
>
>>>  function Parsed (S : String) return Parsed_Type
>>>     with Post =>
>>>       (if S'Length not in Image_Length_Type then
>>>           Parsed'Result.Status = Format_Error);
>>>        -- There may be other failure conditions.
>
> What is special about that specific failure condition that singles it out
> from all other failure conditions?
Hard and tedious (very tedious) to define in the language of expressions  
in a postcondition, but still handily defined in a human language or other  
dedicated formal notations. The failure condition expressed here, is  
simply an easy and obvious one. That's also a useful one, because if the  
client don't know how much to read, based on this postcondition, it knowns  
that going above Image_Length_Type'Last is of no use. This is important  
for defining constraints for buffers and strings receiving inputs.


-- 
“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: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Wed, 1 Feb 2012 11:37:31 +0100, stefan-lucks@see-the.signature wrote:

> On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote:
> 
>> But that seems not bad enough. To make the disaster complete, it should
>> become undefined as well. Right?
> 
> This doesn't need to be a disaster. 
> 
> 1. For the purpose of proving program correctness,

Proving incorrectness, you mean, since the thing is partial.

>    If that is all what we need F for, why should we bother with any 
>    postcondition or even X? 

What about this:

   function Sine (X : Float) return Float is
   begin
      if X = 0.0 then
         return 0.0;
      end if;
   end Sine; 

> 2. Sometimes, it may hard to prove the entire contract. So we will try to 
>    prove the "important" requirements in the contract, and try to convince 
>    ourselves by conventional means (testing, code review, ...) that other
>    requirements are also satisfied.
[...]

No. In that case, and this was my point, the thing must be designed in a
way which clearly distinguished the provable/specified/defined part from
the rest. I proposed to introduce Length_Error to indicate a contracted
error case.

>>>  function Parsed (S : String) return Parsed_Type
>>>     with Post =>
>>>       (if S'Length not in Image_Length_Type then
>>>           Parsed'Result.Status = Format_Error);
>>>        -- There may be other failure conditions.
> 
> What is special about that specific failure condition that singles it out 
> from all other failure conditions?

For the reader it is unclear the statement the postcondition makes. Does it
define the meaning of Format_Error?

This does not look like a contract (provable or not, that is no matter).
The most close thing which comes into mind is a use case. But use ceases do
not belong to the code.

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

Re: Silly and stupid post-condition or not ?

[Adam Beneschan]

On Feb 1, 12:36 am, Stephen Leake <stephen_le...@stephe-leake.org>
wrote:
> "Yannick Duchêne (Hibou57)" <yannick_duch...@yahoo.fr> writes:
>
>
>
>
>
> >    type Parsed_Type (Status : Parsed_Status_Type) is record
> >       case Status is
> >          when Parsed =>
> >             Instance : Instance_Type;
> >          when Format_Error =>
> >             null;
> >       end case;
> >    end record; -- Parsed_Type
>
> >    function Parsed (S : String) return Parsed_Type
> >       with Post =>
> >         (if S'Length not in Image_Length_Type then
> >             Parsed'Result.Status = Format_Error);
> >          -- There may be other failure conditions.
>
> > Is such a post-condition a good or bad practice in your humble or
> > authoritative opinion ?
>
> > Keep in mind there may be many other cases where "Parsed'Result.Status
> > = Format_Error" could be True; the one in the Post is not the only
> > possible  one.
>
> That means the post condition is misleading, and therefore bad.

I don't see this.  It would be misleading to someone who doesn't
understand the fallacy of the converse, but I'd hope that computer
science students would be taught not to make this mistake by the end
of the first or second year.

                             -- Adam

Re: Silly and stupid post‑condition or not ?

[stefan-lucks]

On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote:

> On Wed, 1 Feb 2012 11:37:31 +0100, stefan-lucks@see-the.signature wrote:
> 
> > 1. For the purpose of proving program correctness,
> 
> Proving incorrectness, you mean, since the thing is partial.

With apologies to you and all the c.l.a readers, there was a really bad 
typo in my example. So here is the correct example

     function F(X: Natural) return Natural 
        with Post => (if (X mod 2) = 1 then ...); 

So any program, which's correctness depends on a statement such as 

     Y := F(X) * (X mod 2); -- not "F(X) * (F(X) mod 2)", as I wrote before

may be proven correct (there is nothing "partial" here), in spite of the 
incomplete postcondition for F. 

I.e., value of Y is predictable. If X is odd, one needs the postcondition 
to predict Y. If X is even, then Y is 0, regardless of the value of F(X). 
But note that I follow the SPARK-inspired assumption that for even X, F(X) 
can be any value of the given type, but computing F(X) must not propagate 
an exception!

I didn't actually try it, but I am sure that I could verify the 
correctness of a SPARK program with such a structure. Of course, SPARK 
would still force me to actually prove that F doesn't raise an exception, 
even for the case of X being even. Furthermore, the good thing about SPARK 
is that it would have thrown a bunch of unprovable verification conditions 
at me, had I tried to verify the example with the typo. 

Unfortunately, Ada 2012 lacks a way to specify a subprogram not to 
propagate an exception (*). Waiting for Ada 2020! 

> > 2. Sometimes, it may hard to prove the entire contract. So we will try to 
> >    prove the "important" requirements in the contract, and try to convince 
> >    ourselves by conventional means (testing, code review, ...) that other
> >    requirements are also satisfied.
> [...]
> 
> No. In that case, and this was my point, the thing must be designed in a
> way which clearly distinguished the provable/specified/defined part from
> the rest. I proposed to introduce Length_Error to indicate a contracted
> error case.

I see. However, I would claim that an incomplete postcondition actually 
"distinguishes the provable/specified/defined part from the rest", as you 
put it. E.g., specifying (or even better, proving)

  procedure Ask_Database(U: User; Q: Query; R: out Response)
    with post(if (not Authorized(U)) and (Asks_For_Secret_Stuff(Q)) 
              then R=Empty_Response);

for some applications would be a big deal, even though there are four 
different cases for the postcondition (any combination of the Booleans 
Authorized(U) and Asks_For_Secret_Stuff(Q), and only one of these four 
cases is formally specified. 

---- 
(*) Of course, by the language's own means, without gnatmem or some other 
    tool, one can actually be never really sure about Storage_Error ...

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html> 
------     I love the taste of Cryptanalysis in the morning!      ------

Re: Silly and stupid post�?'condition or not ?

[Randy Brukardt]

<stefan-lucks@see-the.signature> wrote in message 
news:Pine.LNX.4.64.1202011604270.29918@medsec1.medien.uni-weimar.de...
...
> Unfortunately, Ada 2012 lacks a way to specify a subprogram not to
> propagate an exception (*). Waiting for Ada 2020!

See AI12-0017-1 (not sure if this one is posted yet). That is, it's on the 
radar. But we have to finish Ada 2012 first.

                               Randy.

Re: Silly and stupid postâ?'condition or not ?

[Yannick Duchêne (Hibou57)]

Le Thu, 02 Feb 2012 02:50:58 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:

> <stefan-lucks@see-the.signature> wrote in message
> news:Pine.LNX.4.64.1202011604270.29918@medsec1.medien.uni-weimar.de...
> ...
>> Unfortunately, Ada 2012 lacks a way to specify a subprogram not to
>> propagate an exception (*). Waiting for Ada 2020!
>
> See AI12-0017-1 (not sure if this one is posted yet). That is, it's on  
> the
> radar. But we have to finish Ada 2012 first.
>
>                                Randy.
>
Gonna be useful with programs partially proved with SPARK (when one or  
some subprograms are proved to be exception‑free, while not all  
subprograms).

> radar. But we have to finish Ada 2012 first.
>
>                                Randy.
Do I have to update the reference I crawled a few months ago ? I don't  
know if changes are reported on the fly.

-- 
“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: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Wed, 1 Feb 2012 17:37:28 +0100, stefan-lucks@see-the.signature wrote:

> On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote:
> 
>> On Wed, 1 Feb 2012 11:37:31 +0100, stefan-lucks@see-the.signature wrote:
>> 
>>> 1. For the purpose of proving program correctness,
>> 
>> Proving incorrectness, you mean, since the thing is partial.
> 
> With apologies to you and all the c.l.a readers, there was a really bad 
> typo in my example. So here is the correct example
> 
>      function F(X: Natural) return Natural 
>         with Post => (if (X mod 2) = 1 then ...); 
> 
> So any program, which's correctness depends on a statement such as 
> 
>      Y := F(X) * (X mod 2); -- not "F(X) * (F(X) mod 2)", as I wrote before
> 
> may be proven correct (there is nothing "partial" here), in spite of the 
> incomplete postcondition for F. 

You could it have much simpler. Consider programs which do not call F at
all. That does the trick too.

The idea of pre-/postcondition is that it tells something about a set of
programs, of all legal programs actually. If you wanted to narrow that set,
then, well, you should at least specify that set.

>>> 2. Sometimes, it may hard to prove the entire contract. So we will try to 
>>>    prove the "important" requirements in the contract, and try to convince 
>>>    ourselves by conventional means (testing, code review, ...) that other
>>>    requirements are also satisfied.
>> [...]
>> 
>> No. In that case, and this was my point, the thing must be designed in a
>> way which clearly distinguished the provable/specified/defined part from
>> the rest. I proposed to introduce Length_Error to indicate a contracted
>> error case.
> 
> I see. However, I would claim that an incomplete postcondition actually 
> "distinguishes the provable/specified/defined part from the rest", as you 
> put it.

It is a cart before the horse. In Ada we believe that specifications come
first. Yes, for each given program there exists a specification wich would
fit it. Bad design.

>   procedure Ask_Database(U: User; Q: Query; R: out Response)
>     with post(if (not Authorized(U)) and (Asks_For_Secret_Stuff(Q)) 
>               then R=Empty_Response);

BTW, contracts to be stated in terms of equivalence rather than
implications. I.e.

   R=Empty_Response <=> not Authorized(U)) or ...

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

Re: Silly and stupid post‑condition or not ?

[stefan-lucks]

On Thu, 2 Feb 2012, Dmitry A. Kazakov wrote:

> The idea of pre-/postcondition is that it tells something about a set of
> programs, of all legal programs actually. If you wanted to narrow that set,
> then, well, you should at least specify that set.

Fine. An incomplete postcondition does give you that. 


-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: Silly and stupid post‑condition or not ?

[stefan-lucks]

On Thu, 2 Feb 2012, Dmitry A. Kazakov wrote:

> >   procedure Ask_Database(U: User; Q: Query; R: out Response)
> >     with post(if (not Authorized(U)) and (Asks_For_Secret_Stuff(Q)) 
> >               then R=Empty_Response);
> 
> BTW, contracts to be stated in terms of equivalence rather than
> implications. I.e.
> 
>    R=Empty_Response <=> not Authorized(U)) or ...

Why?

These implications are what you would typically find in a security 
requirements specification. (In human-readable way, such as "if an 
unauthorized user asks for any confidential data, no answer is provided by 
the XY system.")

What is the point of rewriting this in terms of equivalence? You run the 
trouble of proving that your rewritten contract is logically equivalent to 
the requirements specification. (Or you risk proving your program correct 
with respect to an incorrect spec.)

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: Silly and stupid post-condition or not ?

[Stephen Leake]

Adam Beneschan <adam@irvine.com> writes:

> On Feb 1, 12:36 am, Stephen Leake <stephen_le...@stephe-leake.org>
> wrote:
>> "Yannick Duchêne (Hibou57)" <yannick_duch...@yahoo.fr> writes:
>>
>>
>>
>>
>>
>> >    type Parsed_Type (Status : Parsed_Status_Type) is record
>> >       case Status is
>> >          when Parsed =>
>> >             Instance : Instance_Type;
>> >          when Format_Error =>
>> >             null;
>> >       end case;
>> >    end record; -- Parsed_Type
>>
>> >    function Parsed (S : String) return Parsed_Type
>> >       with Post =>
>> >         (if S'Length not in Image_Length_Type then
>> >             Parsed'Result.Status = Format_Error);
>> >          -- There may be other failure conditions.
>>
>> > Is such a post-condition a good or bad practice in your humble or
>> > authoritative opinion ?
>>
>> > Keep in mind there may be many other cases where "Parsed'Result.Status
>> > = Format_Error" could be True; the one in the Post is not the only
>> > possible  one.
>>
>> That means the post condition is misleading, and therefore bad.
>
> I don't see this.  It would be misleading to someone who doesn't
> understand the fallacy of the converse, but I'd hope that computer
> science students would be taught not to make this mistake by the end
> of the first or second year.

It is true that this post condition leaves open the possibility of other
causes of failure. But they should be documented as well; why is only
this one singled out?

I agree with Dmitry; post conditions should be _complete_. If the Ada
post condition language is not strong enough to be complete, don't use
it; use natural language comments.

-- 
-- Stephe

Re: Silly and stupid post‑condition or not ?

[Dmitry A. Kazakov]

On Thu, 2 Feb 2012 10:18:03 +0100, stefan-lucks@see-the.signature wrote:

> On Thu, 2 Feb 2012, Dmitry A. Kazakov wrote:
> 
>>>   procedure Ask_Database(U: User; Q: Query; R: out Response)
>>>     with post(if (not Authorized(U)) and (Asks_For_Secret_Stuff(Q)) 
>>>               then R=Empty_Response);
>> 
>> BTW, contracts to be stated in terms of equivalence rather than
>> implications. I.e.
>> 
>>    R=Empty_Response <=> not Authorized(U)) or ...
> 
> Why?
> 
> These implications are what you would typically find in a security 
> requirements specification. (In human-readable way, such as "if an 
> unauthorized user asks for any confidential data, no answer is provided by 
> the XY system.")

And conversely, if no answer is provided, then the user was not authorized
to get it. And furthermore, the data the user gets is the data he asked for
and so on.

> What is the point of rewriting this in terms of equivalence? You run the 
> trouble of proving that your rewritten contract is logically equivalent to 
> the requirements specification. (Or you risk proving your program correct 
> with respect to an incorrect spec.)

You must translate the above into some specifications of some modules
anyway.

If a module has an output, the meaning of that output is the set of
propositions provable with the output value:

   Get_Line = 'a' |= the user typed 'a'

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

Re: Silly and stupid post-condition or not ?

[Georg Bauhaus]

On 02.02.12 10:40, Stephen Leake wrote:

> post conditions should be _complete_. If the Ada
> post condition language is not strong enough to be complete, don't use
> it; use natural language comments.

First, there is no completeness in most real program systems
product; it seems honest, then, to not assume we could manage
to even potentially achieve it is Post aspects, IMHO.
Yet, program system products use formal language.  The use
of formal language means best effort, not completeness of
all kinds, I think.

Post aspects can help being productive:

If programmers know something about the possible outcomes
of a subprogram, they can act accordingly. If there is a
specification that says: the result is such that if P1(Result)
then also P2(Result), they can act accordingly.

A postcondition gives programmers something to work with.
Since natural language does not change the correspondence of
postcondition and programmers writing based on assumptions
about the postcondition, formal language addressing some
results still produce an informed state of mind, a better
one, I think.

As another example,

   type Match (Found: Boolean) is record
      case Found is
          when True =>
             Value : Big_Natural;
          when False =>
             null;
      end case;
   end record;

   procedure Goldbach (A, B: Big_Natural; Result: Match)
     with Post =>
     (if A + B < Highest_Known_Sum then
       (if Result.Found then
               Is_Prime (A)
           and Is_Prime (B)
           and Result.Value mod 2 = 0)
     else  -- larger
       (if Result.Found then
	 Result.Value mod 2 = 0));

Post says that whenever there is a result and it is larger
than some state-of-the-art value, go look and see whether
A and B are prime. If not Result.Found, then data would be thrown
away in any case. Thus, precisely because there is some
kind of formal incompleteness here, the Post aspect tells
something about the results that will not get thrown away.

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Thu, 02 Feb 2012 14:20:55 +0100, Georg Bauhaus  
<rm.dash-bauhaus@futureapps.de> a écrit:
> If not Result.Found, then data would be thrown
> away in any case. Thus, precisely because there is some
> kind of formal incompleteness here, the Post aspect tells
> something about the results that will not get thrown away.

Perfectly worded :-)


-- 
“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: Silly and stupid post�?'condition or not ?

[Randy Brukardt]

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

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.v803oovnule2fv@douda-yannick...
...
>Do I have to update the reference I crawled a few months ago ? I don't 
>know if changes are reported on the fly.

I update the site about once a month or so, mostly depending on the schedule 
for ARG meetings and the like. I try to crawl it every couple of months, 
updating the search indexes for the site:
http://www.ada-auth.org/search.html
and there are also separate searches for each set of AIs. For instance, the 
Ada 2005 AIs can be searched using:
http://www.ada-auth.org/search-ai05s.html

The changes themselves occur almost every day on my local machine, but I 
don't usually copy them to the server immediately.

                                              Randy.

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"Stephen Leake" <stephen_leake@stephe-leake.org> wrote in message 
news:82k445fu9n.fsf@stephe-leake.org...
...
> I agree with Dmitry; post conditions should be _complete_. If the Ada
> post condition language is not strong enough to be complete, don't use
> it; use natural language comments.

That's a pretty silly position, it essentially says that everything that 
makes Ada great is not worthwhile because it only can detect a portion of 
the problems. If you really believe this, you might as well be programming 
in a dynamically typed language, because then there is essentially no 
benefit to what Ada provides.

For instance, if you have an object

           Dart_Score : Natural range 1 .. 60; -- Holds the score for a 
single dart.

The range 1 .. 60 is not a complete specification of the possible scores. 
(For instance, 58 is not a possible score, but it is allowed by the range.) 
But even so, this specification still catches a lot of errors. Your comment 
above denies this and says that it is better to just have the comment rather 
than the range (because it is not "complete" in some sense).

[Aside: Ada 2012 has a way to make this complete, but of course there are 
many other things that are too hard to describe.]

My philosophy is that it is always preferable to at least be able to tell 
the compiler what you (the programmer) knows about a program entity. That 
allows the compiler and other tools to make checks (both compile-time and 
run-time) about that information -- and my years of experience shows me that 
those checks catch a lot of bugs (but by no means all). Moreover, as tools 
and compilers get better, they get able to do more with the information they 
are given, so you want to give them as much information as you can now --  
it's a lot harder to retrofit that information in after the fact.

So I want to describe as much as I can in terms of contracts (preconditions, 
postconditions, predicates, constraints, exclusions, and invariants for Ada 
2012, hopefully exception and data contracts in the future), but not to the 
extent of necessarily requiring completeness. At some point it just gets too 
hard.

I've always hated the emphasis on completeness of these things, because it 
is *exactly* the wrong approach to getting something in wide-spread use 
(even in the Ada community). Something like SPARC, that requires an 
all-or-nothing approach, very often ends up with nothing.

OTOH, an approach that just applies the easiest contracts first sets up a 
positive feedback loop for newcomers to Ada. They'll add a few range 
constraints and discover that those have detected some bugs early (possibly 
even at compile time). Which encourages them to add more contracts, which 
discovers more bugs early, and so on. That's how *I* learned the real 
benefits of Ada years ago - and I find it hard to believe that I'm unusual.

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.)

                                                    Randy.

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Fri, 03 Feb 2012 04:13:04 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> (even in the Ada community). Something like SPARC, that requires an 
> all-or-nothing approach, very often ends up with nothing.
You meant SPAR*K*, didn't you ? :-D

-- 
“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: Silly and stupid post-condition or not ?

[J-P. Rosen]

Le 02/02/2012 10:40, Stephen Leake a écrit :
> I agree with Dmitry; post conditions should be _complete_. If the Ada
> post condition language is not strong enough to be complete, don't use
> it; use natural language comments.
> 
I don't agree with that. Imagine you need (pre-2012) a type for even
numbers between 0 and 100.
Would you declare:
   type My_Int is range 0..100;

or would you use Integer, on the ground that since you cannot express
all of your requirements, you express none?

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Silly and stupid post-condition or not ?

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> 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.)

(SPARK)

Strong agreement here. I don't think I'd have started on any of my own
projects if I'd had to use SPARK. Businesses will, iff they're in an
area where the purchaser requires it (avionics, for example). Does
anywone know what software standards Toyota use? MISRA C?

Re: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Thu, 2 Feb 2012 21:13:04 -0600, Randy Brukardt wrote:

> I've always hated the emphasis on completeness of these things, because it 
> is *exactly* the wrong approach to getting something in wide-spread use 
> (even in the Ada community).

Putting my hat of logicians on: you can't get anywhere without
completeness. This is how logical inference rules work. Sorry for that, but
there is no other way.

The approach should be of course to have clear boundaries between provable
and non-provable parts and letting the programmer to "give his word" for
the gaps to be filled. I.e. to have *conditional* proofs.

It is very sad to see how Ada 2012 messes things up, alas.

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

Re: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Fri, 03 Feb 2012 07:26:00 +0100, J-P. Rosen wrote:

> Le 02/02/2012 10:40, Stephen Leake a �crit :
>> I agree with Dmitry; post conditions should be _complete_. If the Ada
>> post condition language is not strong enough to be complete, don't use
>> it; use natural language comments.
>> 
> I don't agree with that. Imagine you need (pre-2012) a type for even
> numbers between 0 and 100.
> Would you declare:
>    type My_Int is range 0..100;
> 
> or would you use Integer, on the ground that since you cannot express
> all of your requirements, you express none?

This example has nothing to do with the issue. Either of these type
declarations is complete. They define the whole set of type values and
operations.

You and Randy confuse a generalized semantics with an undefined one. The
key question is the relation of the variance of the generalized/unspecified
part to the program's behavior. In your example odd values like 1,3 are not
used by the program, or at least supposed to be unused. In the OP example,
Format_Error of unspecified semantics is to be used heavily.

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

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Fri, 03 Feb 2012 10:12:25 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> In the OP example,
> Format_Error of unspecified semantics is to be used heavily.

Format_Error as a specified semantic: Error. Which turns to disallow any  
access to any parsed Instance. It means that no instance could be parsed  
and the image is to be rejected for that use. It makes the function,  
“partial”.

Or may be you are expecting some unspecified behavior or semantic ? ;)  
(teasing)

To get back to the topic as a whole, it seems clear to me now, the  
postcondition discussed here is finally legitimate.

-- 
“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: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Fri, 03 Feb 2012 10:48:34 +0100, Yannick Duch�ne (Hibou57) wrote:

> Le Fri, 03 Feb 2012 10:12:25 +0100, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
>> In the OP example,
>> Format_Error of unspecified semantics is to be used heavily.
> 
> Format_Error as a specified semantic: Error. Which turns to disallow any  
> access to any parsed Instance.

If that is *the semantics* then the prostcondition is

   Result.Status = Format_Error => Result.Instance raise Constraint_Error

which is of Ada's variant record type. Are you designing compiler tests?

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

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Fri, 03 Feb 2012 12:09:10 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Fri, 03 Feb 2012 10:48:34 +0100, Yannick Duchêne (Hibou57) wrote:
>
>> Le Fri, 03 Feb 2012 10:12:25 +0100, Dmitry A. Kazakov
>> <mailbox@dmitry-kazakov.de> a écrit:
>>> In the OP example,
>>> Format_Error of unspecified semantics is to be used heavily.
>>
>> Format_Error as a specified semantic: Error. Which turns to disallow any
>> access to any parsed Instance.
>
> If that is *the semantics* then the prostcondition is
>
>    Result.Status = Format_Error => Result.Instance raise Constraint_Error

Format_Error is a possible value of a discriminant. The postcondition  
applies to the Image function. I see no way to drift from the latter to  
the former. I understood you asked me what is the meaning of the value  
Format_Error, not what is the meaning of the postcondition.

> which is of Ada's variant record type. Are you designing compiler tests?
Excuse me, I don't understand.


-- 
“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: Silly and stupid post-condition or not ?

[Phil Thornley]

On Feb 3, 3:13 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:

> .... Something like SPARC, that requires an
> all-or-nothing approach, very often ends up with nothing.

I think this misrepresents the range of options available with SPARK.
Proofs can be anywhere in the range from fully formal from first
principles, through less formal proofs with user supplied rules (which
can themselves be supported by more or less formal justifications) to
the fully informal (proof by review).

I have always adopted "as formal as is reasonably practicable" and it
hasn't failed me yet.

> 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 nice to have some examples of what you have in mind here.

Cheers,

Phil

Re: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Fri, 03 Feb 2012 12:40:36 +0100, Yannick Duch�ne (Hibou57) wrote:

> Le Fri, 03 Feb 2012 12:09:10 +0100, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
> 
>> On Fri, 03 Feb 2012 10:48:34 +0100, Yannick Duch�ne (Hibou57) wrote:
>>
>>> Le Fri, 03 Feb 2012 10:12:25 +0100, Dmitry A. Kazakov
>>> <mailbox@dmitry-kazakov.de> a �crit:
>>>> In the OP example,
>>>> Format_Error of unspecified semantics is to be used heavily.
>>>
>>> Format_Error as a specified semantic: Error. Which turns to disallow any
>>> access to any parsed Instance.
>>
>> If that is *the semantics* then the prostcondition is
>>
>>    Result.Status = Format_Error => Result.Instance raise Constraint_Error
> 
> Format_Error is a possible value of a discriminant. The postcondition  
> applies to the Image function. I see no way to drift from the latter to  
> the former. I understood you asked me what is the meaning of the value  
> Format_Error, not what is the meaning of the postcondition.

Supposed to specify the semantics of the operation in terms of the
parameter and result values. Not in Ada 2012, of course...

>> which is of Ada's variant record type. Are you designing compiler tests?
> Excuse me, I don't understand.

You are confusing the semantics of the language types with the problem
domain. In the problem domain Format_Error should tell something about the
image object, rather than to disallow anything. Your postcondition is not
to deliver that message.

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

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Fri, 03 Feb 2012 14:18:40 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> Supposed to specify the semantics of the operation in terms of the
> parameter and result values. Not in Ada 2012, of course...
It do: the postcondition refers to both F'Result and its parameter, and  
relate both.

> You are confusing the semantics of the language types with the problem
> domain. In the problem domain Format_Error should tell something about  
> the image object, rather than to disallow anything. Your postcondition  
> is not
> to deliver that message.

The type definition for Parsed_Type express the problem domain. Returning  
an access to value and Null when nothing is available was not an option  
(excluded on purpose), and was preferred the SML way to do and defined a  
discriminated record.

The function may returns an instance which was parsed, and will not return  
an instance if the input image is erroneously formated. This is not so  
randomly, the result is always the same for each same input.

Parsed_Type express what the function result can be: either an instance or  
nothing (kind of Null).

Format_Error has nothing to tell except nothing was parsed. If Null was  
not an Ada reserved word, I would have name it simply Null. Its purpose is  
indeed to disallow access to an instance which does not exist. It's there  
in place of any instance, because there is no instance. Just like you  
cannot access any data referred to by a null access: there is no data;  
Null has nothing to tell more, except there is nothing there.

The postcondition act as an indirect precondition. This is not a  
precondition because, first, you cannot refer to F'Result in a  
precondition (would not make sens), second, the function returns in any  
case and never raise an exception.

 From the returned type definition, you have an implicit postcondition: you  
either get an instance or nothing. As Georg explained better than I  
previously did, whatever is the reason for the failure to return a  
non‑null instance, a result meaning nothing was returned is to be dropped  
(the program won't fix any erroneous input, it just can drop). What ever  
the program will know about why there was a failure, this would always be  
the same. A complete postcondition (a complex and long one) could tell  
more, but this, first, would be useless as still resulting in always the  
same behavior, second, as useless this would just be bloat.

But there is still something the postcondition tells, and that's where it  
acts as an indirect pseudo‑precondition: if image's length is out of  
bounds, the program is assured Image will return a kind of Null result  
(but will not raise an exception). Knowledge of this property, is useful  
for any program using this function.

-- 
“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: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Fri, 03 Feb 2012 15:14:46 +0100, Yannick Duch�ne (Hibou57) wrote:

> Le Fri, 03 Feb 2012 14:18:40 +0100, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
>> Supposed to specify the semantics of the operation in terms of the
>> parameter and result values. Not in Ada 2012, of course...
> It do: the postcondition refers to both F'Result and its parameter, and  
> relate both.

You forgot the word "semantics."

[...]

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

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1q29nqwr7e7u4.1qrz4gd6twxim.dlg@40tude.net...
...
> You and Randy confuse a generalized semantics with an undefined one. The
> key question is the relation of the variance of the 
> generalized/unspecified
> part to the program's behavior. In your example odd values like 1,3 are 
> not
> used by the program, or at least supposed to be unused. In the OP example,
> Format_Error of unspecified semantics is to be used heavily.

In practice, they're the same thing. It will never be practical to fully 
describe the semantics a real program (like, say, an Ada compiler). Even if 
someone invents a far more descriptive formalism than plain Ada expressions 
to describe such things, it's going to be far too complex to use. 
(Personally, I get confused when people start going beyond basic boolean 
logic; I'd rather people didn't even bother to go beyond that because it's 
worthless to the majority of programmers.)

Beyond that, there is not such thing as "I don't intend to use something". 
Unless the program somehow prevents it, *it* will get used and will happen. 
You will get odd values in the data type that J-P described -- it does not 
matter how they happened. And you will be happy (or at least ought to be) 
that some bugs are detected even if not all.

But to claim that just because it's practically impossible to describe the 
complete behavior of real systems does not mean that there is no benefit to 
describing the easy part. And that is exactly what you are arguing -- and it 
should be clear to any Ada programmer that that is a fallicy.

Similarly, describing *part* of the semantics of a subprogram with a 
postcondition, and part with comments is perfectly valid and possibly 
useful. (That's especially true as checking many of the requirements might 
be too expensive at runtime, and thus they practically have to be omitted 
from the formal postcondition.)

                                          Randy.

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:143dxzgfasd4o$.a7lekw80xee2$.dlg@40tude.net...
> On Thu, 2 Feb 2012 21:13:04 -0600, Randy Brukardt wrote:
>
>> I've always hated the emphasis on completeness of these things, because 
>> it
>> is *exactly* the wrong approach to getting something in wide-spread use
>> (even in the Ada community).
>
> Putting my hat of logicians on: you can't get anywhere without
> completeness. This is how logical inference rules work. Sorry for that, 
> but
> there is no other way.

That's complete and utter bunk. As a compiler writer, I know that a compiler 
can prove all kinds of useful things knowing very little about the program 
in question. And moreover, any information that the compiler can gain is 
helpful; it does not have to be complete in any sense.

The problem here is that people have allowed themselves to be tied in knots 
by formal theories, when it's obvious that you can do plenty with nothing 
but some computing power and a bit of Boolean logic. Formal theories are 
hardly worth the paper they're written on.

Can I prove correctness? No, but that is not now and never will be a useful 
goal. If it was possible, it would just cause an infinite regress anyway. 
Specifically, if you can specify the behavior of a program well enough that 
you can prove 100% of its semantics, then the effort to write the actual 
program was wasted (at least in the vast majority of programming tasks) --  
you would have been better off directly executing the specification. And 
pretty soon, people will be doing that, and we'll be back to having no 
proofs of any kind. (And a much harder to understand specification on top of 
it.)

What I can prove is the presence of some bugs and the absence of other 
behaviors (like raising an exception). And for almost all uses, that's 
enough.

Formal completeness is *always* the wrong goal.

                                                   Randy.

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Sat, 04 Feb 2012 04:16:34 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> But to claim that just because it's practically impossible to describe  
> the complete behavior of real systems does not mean that there is no  
> benefit to describing the easy part. And that is exactly what you are  
> arguing -- and it should be clear to any Ada programmer that that is a  
> fallicy.
At least an Ada practice was always there, even far prior it integrated  
DbC™: express as much validity constraints as you can with the type system.

The type system cannot express every constraint (and that's clear to  
everyone), but it still useful. The same with DbC. Moreover, with DbC, you  
may indeed have to care about efficiency. Anyway, if one want very strict  
proof and cases coverage, there are other tools or languages: SPARK & Cie.  
There is no way to impose such things to every application and every Ada  
source author. On the opposite, this would even prevent authors from  
keeping Ada in mind as an option.

98% is not 100%, but better what you can really and practically get than  
any promise you will not ever access to, and which will turn a something  
far below 98% or to simply nothing.

Time to recall safety and proof level is not to be the same for every Ada  
applications, and to recall this level is to be defined by the  
application's specifications. No need to design an application outside of  
its specifications (except as a game, challenge or other experiments).

-- 
“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: Silly and stupid post-condition or not ?

[Phil Thornley]

[Second attempt to post, my apologies if this is a duplicate but I haven't seen the first post appear anywhere after 24 hours.]
On Friday, 3 February 2012 03:13:04 UTC, Randy Brukardt  wrote:
> .... Something like SPARC, that requires an 
> all-or-nothing approach, very often ends up with nothing.

This misrepresents the options available with the proof features of SPARK, which range from full formal proof, through lower formality proofs using user rules (which can have justifications with a range of formalities) to completely informal, using review proofs.

My experience is that using "as formal as practically possible" has always worked well.

> 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.

Cheers,

Phil 

Re: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Fri, 3 Feb 2012 21:27:40 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:143dxzgfasd4o$.a7lekw80xee2$.dlg@40tude.net...
>> On Thu, 2 Feb 2012 21:13:04 -0600, Randy Brukardt wrote:
>>
>>> I've always hated the emphasis on completeness of these things, because it
>>> is *exactly* the wrong approach to getting something in wide-spread use
>>> (even in the Ada community).
>>
>> Putting my hat of logicians on: you can't get anywhere without
>> completeness. This is how logical inference rules work. Sorry for that, 
>> but there is no other way.
> 
> That's complete and utter bunk. As a compiler writer, I know that a compiler 
> can prove all kinds of useful things knowing very little about the program 
> in question. And moreover, any information that the compiler can gain is 
> helpful; it does not have to be complete in any sense.

No, you don't need all information, but each piece you get must be complete
in itself. Informally, completeness is just about knowing the choices to
make.

> The problem here is that people have allowed themselves to be tied in knots 
> by formal theories, when it's obvious that you can do plenty with nothing 
> but some computing power and a bit of Boolean logic. Formal theories are 
> hardly worth the paper they're written on.

Quite so, but there still exist hard facts, which cannot be ignored without
being punished. 2x2=4, function is not a constructor (:-))

> Can I prove correctness? No, but that is not now and never will be a useful 
> goal.

I don't think so. As the amount and complexity of the software grows the
traditional means of ensuring software quality stop working both
technically and economically.

I see it on the example of GNAT compiler. Probably most experienced and
talented people in the world cannot get it right for about 20 years. 20
years is the age of one generation.

> If it was possible, it would just cause an infinite regress anyway.

True. You always need to take some things for granted. That is no problem
to me. This seems to be a problem to people from your camp: we cannot check
for Strorage_Error! Why? Of course you can, just let the programmer fill
the gaps, let proofs be conditionals. Any proof is conditional because of
that infinite regress. Why throwing everything away?

> Specifically, if you can specify the behavior of a program well enough that 
> you can prove 100% of its semantics, then the effort to write the actual 
> program was wasted (at least in the vast majority of programming tasks) --  
> you would have been better off directly executing the specification. And 
> pretty soon, people will be doing that, and we'll be back to having no 
> proofs of any kind. (And a much harder to understand specification on top of 
> it.)

And again, this is what you get. If you refuse to integrate formal stuff
into the language, then, inevitably, an ugly modeling tool to come. And one
uglier on top of it and so on. Tools prey and feed on weak languages.

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

Re: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Fri, 3 Feb 2012 21:16:34 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1q29nqwr7e7u4.1qrz4gd6twxim.dlg@40tude.net...
> ...
>> You and Randy confuse a generalized semantics with an undefined one. The
>> key question is the relation of the variance of the generalized/unspecified
>> part to the program's behavior. In your example odd values like 1,3 are not
>> used by the program, or at least supposed to be unused. In the OP example,
>> Format_Error of unspecified semantics is to be used heavily.
> 
> In practice, they're the same thing. It will never be practical to fully 
> describe the semantics a real program (like, say, an Ada compiler). Even if 
> someone invents a far more descriptive formalism than plain Ada expressions 
> to describe such things, it's going to be far too complex to use.

Sure, but this is a fault of your (read: ARG) approach.

Look, you are trying to describe the semantics of a program written in the 
language (Ada expression) in the same language (Ada expression), though in 
the form of "pre-"/"post-" conditions. That would not work. No need to even 
try! Isn't it obvious, that there is no value added? It is the same 
language of same power. Why do you expect it work any better by merely 
moving code from bodies to the declarations?

> Beyond that, there is not such thing as "I don't intend to use something". 
> Unless the program somehow prevents it, *it* will get used and will happen.

Absolutely. But that does not imply that a dynamic check could magically 
make unusable usable.

> You will get odd values in the data type that J-P described -- it does not 
> matter how they happened. And you will be happy (or at least ought to be) 
> that some bugs are detected even if not all.

No, I am very unhappy when the original appearance of a bug is modified by 
some middleman (e.g. exception propagation).

That is assuming absence of false positives. But as we learned from the 
history accessibility checks, false positives are very likely to happen. 
When highly qualified Ada designers failed to design a check properly, what 
to expect from a layman programmer adding fancy pre-/postconditions in his 
program?

> But to claim that just because it's practically impossible to describe the 
> complete behavior of real systems does not mean that there is no benefit to 
> describing the easy part.

No, if that description is incomplete;
No, if that is a dynamic check, rather than a description;
No, if the remaining part cannot be implemented because of the choice made;
No, if the easy part is unimportant to the goal at hand.

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

Re: Silly and stupid post-condition or not ?

[Phil Thornley]

[Third attempt to reply, so I apologise for any duplicates, but posts 
via Google Groups aren't emerging.]

In article <jgfjc4$u4b$1@munin.nbi.dk>, randy@rrsoftware.com says...
> ... Something like SPARC, that requires an 
> all-or-nothing approach, very often ends up with nothing.

This misrepresents the options available with the proof features of 
SPARK, which range from full formal proof, through lower formality 
proofs using user rules (which can have justifications with a range of 
formalities) to completely informal proof, using review proofs.

My experience is that using "as formal as practically possible" has 
always worked well. 

...
> 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. 

Cheers, 

Phil 

Re: Silly and stupid post-condition or not ?

[Stephen Leake]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> "Stephen Leake" <stephen_leake@stephe-leake.org> wrote in message 
> news:82k445fu9n.fsf@stephe-leake.org...
> ...
>> I agree with Dmitry; post conditions should be _complete_. If the Ada
>> post condition language is not strong enough to be complete, don't use
>> it; use natural language comments.
>
> That's a pretty silly position, it essentially says that everything that 
> makes Ada great is not worthwhile because it only can detect a portion of 
> the problems. 

That's pretty silly as well; I use Ada for everything, and have said so
many times here. 

But I'll try to keep an open mind and find something useful to say.

> For instance, if you have an object
>
>            Dart_Score : Natural range 1 .. 60; -- Holds the score for a 
> single dart.

Nothing in this declaration says it's a _valid_ dart_score. But it would
be helpful for the comment to include the notion of invalid scores:

    Dart_Score : Natural range 1 .. 60; 
    -- Holds the score for a single dart. Note that not all scores in
    -- this range are possible on a standard dart board.

So this uses part Ada and part natural language to specify the
actual constraints.

The original post condition was:

   function Parsed (S : String) return Parsed_Type
      with Post =>
        (if S'Length not in Image_Length_Type then
            Parsed'Result.Status = Format_Error);
         -- There may be other failure conditions.

I was ignoring the comment; it's pretty weak. I would improve it:

   function Parsed (S : String) return Parsed_Type
      with Post =>
        (if S'Length not in Image_Length_Type then
            Parsed'Result.Status = Format_Error);
   -- There are other failure conditions indicated by
   -- Parsed'Result.Status = Format_Error.

I still find this less satisfying than in the Dart_Score case. But maybe
that's just because I'm used to range constraints, and not used to post
conditions.

> My philosophy is that it is always preferable to at least be able to tell 
> the compiler what you (the programmer) knows about a program entity.

The compiler knows the body; why is the post condition better than that?

> That allows the compiler and other tools to make checks (both
> compile-time and run-time) about that information -- and my years of
> experience shows me that those checks catch a lot of bugs (but by no
> means all). Moreover, as tools and compilers get better, they get able
> to do more with the information they are given, so you want to give
> them as much information as you can now -- it's a lot harder to
> retrofit that information in after the fact.

The post condition also specifies a run-time check; that will catch
bugs. But I don't consider that "telling the compiler something"; I
consider it a way of specifing what checks to perform.

If assertions are enabled, the compiler can assume post conditions are
satisfied after a call (since otherwise an exception will be raised).
That does give the compile information it can act on.

In the particular case of Parsed, the information is not useful after
the function returns, since it is actually a precondition.

> So I want to describe as much as I can in terms of contracts (preconditions, 
> postconditions, predicates, constraints, exclusions, and invariants for Ada 
> 2012, hopefully exception and data contracts in the future), but not to the 
> extent of necessarily requiring completeness. At some point it just gets too 
> hard.

Ok, as long as there is a comment saying what's left out, when it is
significant (as it is in the Parsed case; less so in the Dart_Score case).

> I've always hated the emphasis on completeness of these things, because it 
> is *exactly* the wrong approach to getting something in wide-spread use 
> (even in the Ada community). 

That makes sense; I had not considered that aspect.

-- 
-- Stephe

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Sun, 05 Feb 2012 00:07:31 +0100, Stephen Leake  
<stephen_leake@stephe-leake.org> a écrit:
> Nothing in this declaration says it's a _valid_ dart_score. But it would
> be helpful for the comment to include the notion of invalid scores:
>
>     Dart_Score : Natural range 1 .. 60;
>     -- Holds the score for a single dart. Note that not all scores in
>     -- this range are possible on a standard dart board.
>
> So this uses part Ada and part natural language to specify the
> actual constraints.
>
> The original post condition was:
>
>    function Parsed (S : String) return Parsed_Type
>       with Post =>
>         (if S'Length not in Image_Length_Type then
>             Parsed'Result.Status = Format_Error);
>          -- There may be other failure conditions.
>
> I was ignoring the comment; it's pretty weak. I would improve it:
>
>    function Parsed (S : String) return Parsed_Type
>       with Post =>
>         (if S'Length not in Image_Length_Type then
>             Parsed'Result.Status = Format_Error);
>    -- There are other failure conditions indicated by
>    -- Parsed'Result.Status = Format_Error.
>

I feel you are right about the comment, it was too easy to miss. I tend to  
like conciseness, but may be to much conciseness disallow the expected  
emphasis in some cases.

-- 
“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: Silly and stupid post-condition or not ?

[Randy Brukardt]

"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. 

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"Stephen Leake" <stephen_leake@stephe-leake.org> wrote in message 
news:82ty36urik.fsf@stephe-leake.org...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
...
>> My philosophy is that it is always preferable to at least be able to tell
>> the compiler what you (the programmer) knows about a program entity.
>
> The compiler knows the body; why is the post condition better than that?

No, the compiler does *not* know the body (in general). Ada separates 
specifications and bodies after all. The specification can be compiled long 
before the body is created, and calls written and compiled against that 
specification.

A large part of the problem that I see with proof tools is that they often 
require peeking into the body to verify calls. This is just plain wrong, 
because it means that the proof has to be redone if the body changes. And it 
also means that the body has to exist (and in a near-final form) before the 
proof can be valuable.

An Ada compiler knows even less; when it generates a call it probably knows 
nothing about the body. (Janus/Ada was designed so that the compiler 
literally knows nothing about the body, and cannot get access to any 
information about the body even if it wanted to [other than the one being 
compiled, of course]. That's why Janus/Ada doesn't do any inlining [at 
compile time], as that requires breaking that absolute separation of 
specifications and bodies.) And an Ada compiler cannot presume to know 
anything about the body when compiling a call (as noted, the body may not 
have been written yet).

The postcondition (and precondition) moves this "contract" information to 
where it belongs (on the specification). That allows the compiler to take 
advantage of that information, and in many cases completely eliminate the 
associated checks (just like the compiler can eliminate a large proportion 
of constraint checks). Like constraint checks, well-written contracts should 
never need to be turned off (as always, it's like taking off the seatbelts 
when you leave the garage...).

                                              Randy.

Re: Silly and stupid post-condition or not ?

[Phil Thornley]

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

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Sun, 05 Feb 2012 11:23:06 +0100, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> 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).
That's an example case where SPARK could be made more widely usable, if it  
could automatically translate some of the constructs it rejects in the  
terms of the constructs it accept. Another quick example could be  
named‑block‑statement, which SPARK does not allow (if my mind is right),  
but which could be interpreted as a subrprogram defined somewhere and  
invoked from a single location.


-- 
“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: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Sun, 05 Feb 2012 07:18:44 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> 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.

While analysis is running, some known properties can be used to exclude  
some states. I mean as analysis goes, the set of possible states can go  
smaller, thus potentially avoiding any explosion.

This may not go this way, but at least this can go this way.

-- 
“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: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Sun, 05 Feb 2012 07:29:21 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> A large part of the problem that I see with proof tools is that they  
> often
> require peeking into the body to verify calls. This is just plain wrong,
> because it means that the proof has to be redone if the body changes.  
> And it
> also means that the body has to exist (and in a near-final form) before  
> the proof can be valuable.

Seems strange assertion.

With SPARK, you prove the implementation is conforming to its  
specification. So, obviously, if the implementation changes, then you have  
to prove it again, but just like you have to recompile it again.

No implementation is required to refer to a signature. SPARK will relies  
on the annotations associated with the signature every where a given  
subprogram is invoked. Just like Janus/Ada seems to compile, after what  
you explained elsewhere.

Or else I did not understand what you meant.

Were you thinking about automated and à‑posteriori analysis tools? This  
are not proof‑tools.

-- 
“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: Silly and stupid post-condition or not ?

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> People forget that Ada uses "access types" rather than "pointers", 

A rose by any other name...

>...and the 
> reason for that is that access types are type-safe (in the absence of 
> erroneous execution, anyway).

That's like saying, "Drunk driving is safe so long as you don't crash."

Type safety means "can't cause erroneous (unpredictable, undefined)
execution".

- Bob

Re: Silly and stupid post-condition or not ?

[Robert A Duff]

Phil Thornley <phil.jpthornley@gmail.com> writes:

> 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."

Yes, aliasing makes analysis very difficult.  But...

> 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).

Yes, you can simulate pointers (access values) using arrays and
indices.  This introduces the same aliasing issues, and the same
dangling pointer (dangling index) issues.  A(X) can in general
alias A(Y), and a compiler or analysis tool would like to prove
X=Y, or prove X/=Y.

It seems like the aliasing issue is harder with indices, because you
can do arithmetic one them, whereas you can't do arithmetic
on pointers (in Ada).

(I don't see why this has anything to do with having names.
And not "everything" must have a name, but I know what you mean.)

>... 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.

I'm not sure what you mean by that.  Could you give an example?

> "Of course, the extent to which Ada must be simplified for high-
> integrity programming will be a matter of opinion: ...

Indeed.  

SPARK may be great for certain types of systems, but I wouldn't
want to write (say) a compiler in SPARK.

- Bob

Re: Silly and stupid post-condition or not ?

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> The postcondition (and precondition) moves this "contract" information to 
> where it belongs (on the specification).

Right.  That's what makes a precondition better than simply putting
a pragma Assert at the start of the procedure body.

>... That allows the compiler to take 
> advantage of that information, and in many cases completely eliminate the 
> associated checks (just like the compiler can eliminate a large proportion 
> of constraint checks). Like constraint checks, well-written contracts should 
> never need to be turned off...

I don't agree.  There are definitely cases when constraint checks
should be turned off.  Likewise preconditions.  If you say
"Never turn off checks", you're really saying "Never write
an assertion that is too expensive in production, even
though it might be helpful in testing and debugging",
which is clearly counter-productive.

>...(as always, it's like taking off the seatbelts 
> when you leave the garage...).

I don't buy this analogy (nor the similar one about life jackets and
sailboats).  Seatbelts often save lives and reduce injuries
when something goes wrong.  Preconditions (etc) don't cause
programs to give correct answers when something goes wrong
-- they just detect the wrongness.

By the way, I find that when I (at first) think I want a
pre/post, it's usually better expressed as a subtype predicate.
My favorite new feature of Ada 2012.

- Bob

Re: Silly and stupid post-condition or not ?

[Phil Thornley]

In article <wccsjipfhlb.fsf@shell01.TheWorld.com>, 
bobduff@shell01.TheWorld.com says...
> 
> Phil Thornley <phil.jpthornley@gmail.com> writes:
> 
> > 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."
> 
> Yes, aliasing makes analysis very difficult.  But...
> 
> > 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).
> 
> Yes, you can simulate pointers (access values) using arrays and
> indices.  This introduces the same aliasing issues, and the same
> dangling pointer (dangling index) issues.  A(X) can in general
> alias A(Y), and a compiler or analysis tool would like to prove
> X=Y, or prove X/=Y.

Yes - that's exactly what you *have* to do (not like) when you update 
two or more elements of an array (or prove your conclusion for either 
possibility of course).

> It seems like the aliasing issue is harder with indices, because you
> can do arithmetic one them, whereas you can't do arithmetic
> on pointers (in Ada).

I don't think that's a substantial point, the X and the Y can be 
expressions and that doesn't change anything.

>
> (I don't see why this has anything to do with having names.
> And not "everything" must have a name, but I know what you mean.)
>
> >... 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.
>
> I'm not sure what you mean by that.  Could you give an example?

My code is managing the list of free elements, as well as the elements 
in the data structure, so I need to show that every array element that 
should be in the free list is there and that there isn't any element in 
the free list that is also in the data structure. If I'm using access 
values then I'm relying on the correctness of the compiled code/Ada run-
time handling of a storage pool, which probably has a lower level of 
integrity than I'm claiming for my code.

But the main point I was making is that there doesn't seem to be any 
major benefits to the SPARK user from adding access values to the 
language.

>
> ...
> SPARK may be great for certain types of systems, but I wouldn't
> want to write (say) a compiler in SPARK.

(Personally I wouldn't want to write a compiler at all .....)

Phil

Re: Silly and stupid post-condition or not ?

[Robert A Duff]

Phil Thornley <phil.jpthornley@gmail.com> writes:

> In article <wccsjipfhlb.fsf@shell01.TheWorld.com>, 
> bobduff@shell01.TheWorld.com says...
>> It seems like the aliasing issue is harder with indices, because you
>> can do arithmetic one them, whereas you can't do arithmetic
>> on pointers (in Ada).
>
> I don't think that's a substantial point, the X and the Y can be 
> expressions and that doesn't change anything.

I meant that things like "X := X + 1;" changes what X points at.
That's allowed for indices, but not for pointers.

Suppose you want to know what might be modified by procedure P,
and P takes a parameter X that's a (pointer to a) linked list.
I'm not necessarily talking about SPARK, here.  I (or some tool)
can reason that P can only modify what X points at (transitively).
But if X is an index, and we're using some array as a hand-made
"heap", it's as if every heap object points to every other heap
object (including ones on the free list!), because P can say
X+1, X+2, X-1, etc.  OTOH, I suppose making it a private type helps.

>> I'm not sure what you mean by that.  Could you give an example?
>
> My code is managing the list of free elements, as well as the elements 
> in the data structure, so I need to show that every array element that 
> should be in the free list is there and that there isn't any element in 
> the free list that is also in the data structure.

I see.  Thanks.

>...If I'm using access 
> values then I'm relying on the correctness of the compiled code/Ada run-
> time handling of a storage pool, which probably has a lower level of 
> integrity than I'm claiming for my code.

True, although there are user-defined storage pools in Ada
(not in SPARK).

> (Personally I wouldn't want to write a compiler at all .....)

Writing a bootstrapped compiler is the coolest thing in
the world.  ;-)

- Bob

Re: Silly and stupid post-condition or not ?

[Phil Thornley]

In article <wccliohots1.fsf@shell01.TheWorld.com>, 
bobduff@shell01.TheWorld.com says...
> 
> Phil Thornley <phil.jpthornley@gmail.com> writes:
> 
> > In article <wccsjipfhlb.fsf@shell01.TheWorld.com>, 
> > bobduff@shell01.TheWorld.com says...
> >> It seems like the aliasing issue is harder with indices, because you
> >> can do arithmetic one them, whereas you can't do arithmetic
> >> on pointers (in Ada).
> >
> > I don't think that's a substantial point, the X and the Y can be 
> > expressions and that doesn't change anything.
> 
> I meant that things like "X := X + 1;" changes what X points at.
> That's allowed for indices, but not for pointers.
> 
> Suppose you want to know what might be modified by procedure P,
> and P takes a parameter X that's a (pointer to a) linked list.
> I'm not necessarily talking about SPARK, here.  I (or some tool)
> can reason that P can only modify what X points at (transitively).
> But if X is an index, and we're using some array as a hand-made
> "heap", it's as if every heap object points to every other heap
> object (including ones on the free list!), because P can say
> X+1, X+2, X-1, etc.  OTOH, I suppose making it a private type helps.
> 

Proofs don't really know anything about variables, only values. If a 
particular variable can take multiple values along a single execution 
path then either those values are defined by their expressions (which 
therefore replace the variable in the verification conditions) or if the 
expressions aren't known (usually because the variable is exported by 
one or more procedures) then the values are given different names, x__1, 
x__2, ...

Phil

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Sun, 05 Feb 2012 16:16:26 +0100, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:
> By the way, I find that when I (at first) think I want a
> pre/post, it's usually better expressed as a subtype predicate.
> My favorite new feature of Ada 2012.
>
> - Bob

Seems nice, but given this…

    subtype Image_Type is String
       with Static_Predicate => Image_Type'Length in Length_Type;

    function Image (Instance : Instance_Type) return Image_Type
       with Post =>
         (Parsed (Image'Result).Status = Parsed) and
         (Parsed (Image'Result).Instance = Instance);
       -- Result can always be successfully parsed and the resulting
       -- instance is always equal to the one whose image is returned.

…how do I move Image's Post predicate to an Image_Type's dynamic predicate  
? I could not figure the syntax nor if it's at least possible.

-- 
“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: Silly and stupid post-condition or not ?

[Robert A Duff]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

> Seems nice, but given this…
>
>    subtype Image_Type is String
>       with Static_Predicate => Image_Type'Length in Length_Type;
>
>    function Image (Instance : Instance_Type) return Image_Type
>       with Post =>
>         (Parsed (Image'Result).Status = Parsed) and
>         (Parsed (Image'Result).Instance = Instance);
>       -- Result can always be successfully parsed and the resulting
>       -- instance is always equal to the one whose image is returned.
>
> …how do I move Image's Post predicate to an Image_Type's dynamic
> predicate  ? I could not figure the syntax nor if it's at least possible.

Not possible.  Predicates can only express a property of a single
thing, but here you're trying to express a relationship
between two things (parameter and result).

- Bob

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Mon, 06 Feb 2012 15:39:14 +0100, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:

> "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:
>
>> Seems nice, but given this…
>>
>>    subtype Image_Type is String
>>       with Static_Predicate => Image_Type'Length in Length_Type;
>>
>>    function Image (Instance : Instance_Type) return Image_Type
>>       with Post =>
>>         (Parsed (Image'Result).Status = Parsed) and
>>         (Parsed (Image'Result).Instance = Instance);
>>       -- Result can always be successfully parsed and the resulting
>>       -- instance is always equal to the one whose image is returned.
>>
>> …how do I move Image's Post predicate to an Image_Type's dynamic
>> predicate  ? I could not figure the syntax nor if it's at least  
>> possible.
>
> Not possible.  Predicates can only express a property of a single
> thing, but here you're trying to express a relationship
> between two things (parameter and result).
>
> - Bob


Sorry, my wording was unclear. Here is what I wanted, and it works:

    subtype Image_Type is String
       with Dynamic_Predicate =>
         (Image_Type'Length in Length_Type) and
         (Parsed (Image_Type).Status = Parsed);

(don't know why it first failed, may be a syntax error)

The predicate “Parsed (Image_Type).Status = Parsed” is better on  
Image_Type than on Image.

So thanks for your prior message which gave me this idea. Since now, will  
better think about moving predicates on types as much as possible. Indeed  
better.


-- 
“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: Silly and stupid post-condition or not ?

[Randy Brukardt]

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

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.v87eozlaule2fv@douda-yannick...
Le Sun, 05 Feb 2012 07:29:21 +0100, Randy Brukardt <randy@rrsoftware.com>  a 
�crit:
>> A large part of the problem that I see with proof tools is that they 
>> often
>> require peeking into the body to verify calls. This is just plain wrong,
>> because it means that the proof has to be redone if the body changes. And 
>> it
>> also means that the body has to exist (and in a near-final form) before 
>> the proof can be valuable.
>
>Seems strange assertion.
>
>With SPARK, you prove the implementation is conforming to its

Sorry, I was talking about "some" proof tools, not any specific one. And 
recall that I was specifically answering a query about why seeing the body 
was not good enough. SPARK is *not* seeing the body, so none of what I said 
applies to it. But there are a lot of "correctness" tools out there that 
only work with complete source code.

                                 Randy.

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wccobtdfgz9.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> The postcondition (and precondition) moves this "contract" information to
>> where it belongs (on the specification).
>
> Right.  That's what makes a precondition better than simply putting
> a pragma Assert at the start of the procedure body.
>
>>... That allows the compiler to take
>> advantage of that information, and in many cases completely eliminate the
>> associated checks (just like the compiler can eliminate a large 
>> proportion
>> of constraint checks). Like constraint checks, well-written contracts 
>> should
>> never need to be turned off...
>
> I don't agree.  There are definitely cases when constraint checks
> should be turned off.  Likewise preconditions.  If you say
> "Never turn off checks", you're really saying "Never write
> an assertion that is too expensive in production, even
> though it might be helpful in testing and debugging",
> which is clearly counter-productive.

I would indeed argue that. More accurately, what I would argue is that any 
assertion that is too expensive to "use in production" be kept completely 
separate from the rest, and I'd suggest that it generally be turned off 
(unless absolutely needed).

I've done this in my programs by simply commenting them out; they're only 
inserted when the problem that they are intended to detect shows up a second 
time. (That doesn't happen much.) I could see using some other mechanism to 
keep them separate; possibly going so far as to using a dynamic method to 
turn them on or off.

This has always been one of my biggest complaints with Assertions; all or 
nothing is insufficient control; it's bad enough that I've never seen any 
real value to pragma Assert. (I'd rather use if statements controlled from a 
global package than to use a single compiler switch for such detection.)

>>...(as always, it's like taking off the seatbelts
>> when you leave the garage...).
>
> I don't buy this analogy (nor the similar one about life jackets and
> sailboats).  Seatbelts often save lives and reduce injuries
> when something goes wrong.  Preconditions (etc) don't cause
> programs to give correct answers when something goes wrong
> -- they just detect the wrongness.

Turning off constraint checks make a program erroneous, and thus the program 
can return wrong answers without any notice. Back in the CP/M/MS-DOS-1 days, 
we used to have this problem a lot, especially by accessing non-existent 
variants. And a lot of those problems only showed up in production.

Today, this sort of thing is a security problem - constraint checks at least 
bound the problem to at worse a denial-of-service problem, much less of a 
problem than allowing a buffer overflow that allows anything to be executed.

I admit that is less of a problem for preconditions and the like, but I 
think the same holds true -- particular if the correctness checks were 
removed from the code in favor of the preconditions.

> By the way, I find that when I (at first) think I want a
> pre/post, it's usually better expressed as a subtype predicate.
> My favorite new feature of Ada 2012.

I agree. I originally thought that predicates were a better solution to the 
problem than pre/post/invariants. I still do for most uses, but of course 
whenever multiple parameters are involved you have to use a precondition 
instead.

                                                 Randy.

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"Phil Thornley" <phil.jpthornley@gmail.com> wrote in message 
news:MPG.299868e7ebbd43b1989683@news.zen.co.uk...
> In article <jgl70g$l9i$1@munin.nbi.dk>, randy@rrsoftware.com says...
...
> The original SPARK Rationale says:

I don't much care why SPARK is the way it is -- it's obvious that it makes 
sense for a certain set of customers, and that's great.

I want a tool that would be useful for typical Ada programs, and these are 
going to have dispatching and access types and exceptions and tasks ...

There is no way that SPARK is ever going to be that tool, it would destroy 
its purpose.

But I don't necessarily want complete proofs, and as I noted last week, I 
don't think that there is much value to complete proofs as a goal, because 
if you have a language that can describe the specifications well enough that 
you can prove the result, you no longer need the Ada code that's being 
proved (just execute the specification). We need "enough" proof, but not too 
much.

I'm much more interested in proving that a subprogram meets its 
postconditions (including exception postconditions) given its parameter 
types and preconditions.

SPARK insists that you go back to the bad old days of using essentially 
untyped arrays for data storage rather than typed pointers, using error 
codes and piles of exceptional logic rather than exceptions, and the like --  
all of the reasons that I moved to Ada in the first place. It eliminates 
virtually everything that makes Ada better than "just another programming 
language", which is not a step forward for my uses. (Obviously, other 
people's experiences and needs will vary.)

Yes, aliasing analysis is hard. That's the point -- if the typing of the 
underlying system is correct, it rarely could matter to a proof, and it 
would be fairly easy to point out the rare exceptions.

Yes, you could write a case statement instead of using dispatching. Your 
program maintenance costs will skyrocket (having to rewrite all of those 
cases and reprove everything every time a new object type is added). Unless 
your program never changes after it's constructed, which is not remotely the 
case for anything I work on.

> (Personally I wouldn't want to write a compiler at all .....)

Well, there's the problem. :-) Real programmers always want to write a 
compiler (and already have written several). [Not necessarily for a language 
the size of Ada, though. That requires a form of insanity. ;-)]

                                        Randy.

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wccwr81fi7a.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> People forget that Ada uses "access types" rather than "pointers",
>
> A rose by any other name...
>
>>...and the
>> reason for that is that access types are type-safe (in the absence of
>> erroneous execution, anyway).
>
> That's like saying, "Drunk driving is safe so long as you don't crash."
>
> Type safety means "can't cause erroneous (unpredictable, undefined)
> execution".

Are you claiming that Ada is never type-safe? Since there are lots of ways 
to create erroneous execution in Ada, there is nothing in Ada that is 
remotely safe from it. (All real Ada programs are erroneous, after all.)

In any case, my point was about *outside* erroneous execution. Access types 
themselves are type-safe. If you start using Unchecked_ programming or 
address overlays or foreign language interfaces, you're outside of the box, 
but you can't blame that on the access types and values. (And please keep in 
mind that I was specifically postulating that the program was using a custom 
storage pool; the idea being that it could detect/prevent dangling pointers 
and thus eliminate that particular problem from causing erroneousness.)

                                          Randy.

Re: Silly and stupid post-condition or not ?

[BrianG]

On 02/03/2012 03:12 AM, Simon Wright wrote:
> "Randy Brukardt"<randy@rrsoftware.com>  writes:
>
>> 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.)
>
> (SPARK)
>
> Strong agreement here. I don't think I'd have started on any of my own
> projects if I'd had to use SPARK. Businesses will, iff they're in an
> area where the purchaser requires it (avionics, for example). Does
> anywone know what software standards Toyota use? MISRA C?
According to Embedded Systems Design (I'd have to find the ref's), they 
use none - they farm out the job.

-- 
---
BrianG
000
@[Google's email domain]
.com

Re: Silly and stupid post-condition or not ?

[BrianG]

On 02/05/2012 01:18 AM, Randy Brukardt wrote:
> "Phil Thornley"<phil.jpthornley@gmail.com>  wrote in message
> news:MPG.29972ec7befb6ae9989682@news.zen.co.uk...
>>> ... (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.
>
>
It sounds like you don't want SPARK (as it is now, at least), but 
something like an Ada equivalent to LINT.  (Not an Ada version of lint, 
but something that does for Ada what lint does for C - covers Ada's 
needs, rather than C's.)

-- 
---
BrianG
000
@[Google's email domain]
.com

Re: Silly and stupid post-condition or not ?

[Yannick Duchêne (Hibou57)]

Le Tue, 07 Feb 2012 03:34:08 +0100, BrianG <me@null.email> a écrit:
> It sounds like you don't want SPARK (as it is now, at least), but  
> something like an Ada equivalent to LINT.  (Not an Ada version of lint,  
> but something that does for Ada what lint does for C - covers Ada's  
> needs, rather than C's.)

There already is something even better :-)
http://www.adalog.fr/adacontrol2.htm (english page)
http://www.adalog.fr/adacontrol1.htm (french page)


-- 
“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: Silly and stupid post-condition or not ?

[Dmitry A. Kazakov]

On Mon, 6 Feb 2012 20:05:04 -0600, Randy Brukardt wrote:

>> (Personally I wouldn't want to write a compiler at all .....)
> 
> Well, there's the problem. :-) Real programmers always want to write a 
> compiler (and already have written several). [Not necessarily for a language 
> the size of Ada, though. That requires a form of insanity. ;-)]

Actually it would be very interesting to be able to write a compiler using
proofs.

Due to combinatorial explosion of variants, it is impossible to test a
compiler properly, especially its back-end with regard to optimization and
other switches influencing the outcome. Showing equivalence of programs
would also be extremely useful here.

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

Re: Silly and stupid post-condition or not ?

[Simon Wright]

BrianG <me@null.email> writes:

> On 02/03/2012 03:12 AM, Simon Wright wrote:

>> Does anywone know what software standards Toyota use? MISRA C?

> According to Embedded Systems Design (I'd have to find the ref's),
> they use none - they farm out the job.

They would then be the customer, and would impose whatever standards
they think appropriate on the contractor.

I was talking to someone whose business made a locator system for people
who get lost in foul weather; he didn't worry about external standards,
he just did his best to get it right (and, I gathered, kept his fingers
crossed).

Re: Silly and stupid post-condition or not ?

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> I've done this in my programs by simply commenting them out; ...

Well, that's one way to "turn off" assertions.

I agree it would be good to have more control over
super-expensive assertions.  GNAT has some features like that.

>>>...(as always, it's like taking off the seatbelts
>>> when you leave the garage...).
>>
>> I don't buy this analogy (nor the similar one about life jackets and
>> sailboats).  Seatbelts often save lives and reduce injuries
>> when something goes wrong.  Preconditions (etc) don't cause
>> programs to give correct answers when something goes wrong
>> -- they just detect the wrongness.
>
> Turning off constraint checks make a program erroneous, and thus the program 
> can return wrong answers without any notice.

Yes, of course.  But that's got nothing to do with seatbelts!

> Today, this sort of thing is a security problem...

Yes, for programs that accept untrusted inputs.
A compiler, for example, doesn't have that problem
(unless you hook it up to the internet!).

>... - constraint checks at least 
> bound the problem to at worse a denial-of-service problem, much less of a 
> problem than allowing a buffer overflow that allows anything to be executed.

Yes, DoS are less of a problem than stealing the credit-card database.
So I suppose I must admit this has a bit of "seatbelt" flavor to it
(analogous to "reduce injuries").

> I admit that is less of a problem for preconditions and the like, but I 
> think the same holds true -- particular if the correctness checks were 
> removed from the code in favor of the preconditions.
>
>> By the way, I find that when I (at first) think I want a
>> pre/post, it's usually better expressed as a subtype predicate.
>> My favorite new feature of Ada 2012.
>
> I agree. I originally thought that predicates were a better solution to the 
> problem than pre/post/invariants. I still do for most uses, but of course 
> whenever multiple parameters are involved you have to use a precondition 
> instead.

Right.

- Bob

Re: Silly and stupid post-condition or not ?

[Robert A Duff]

BrianG <me@null.email> writes:

> On 02/03/2012 03:12 AM, Simon Wright wrote:
>> anywone know what software standards Toyota use? MISRA C?
> According to Embedded Systems Design (I'd have to find the ref's), they
> use none - they farm out the job.

For a long time, GM and maybe others were using Modula-2.
I don't know if they still do.

- Bob

Re: Silly and stupid post-condition or not ?

[BrianG]

On 02/07/2012 05:43 AM, Simon Wright wrote:
> BrianG<me@null.email>  writes:
>
>> On 02/03/2012 03:12 AM, Simon Wright wrote:
>
>>> Does anywone know what software standards Toyota use? MISRA C?
>
>> According to Embedded Systems Design (I'd have to find the ref's),
>> they use none - they farm out the job.
>
> They would then be the customer, and would impose whatever standards
> they think appropriate on the contractor.
Then they would specify a standard, not use one.  If I remember 
correctly, what was reviewed was MISRA Bull, I mean MISRA C.
>
> I was talking to someone whose business made a locator system for people
> who get lost in foul weather; he didn't worry about external standards,
> he just did his best to get it right (and, I gathered, kept his fingers
> crossed).
But did he use his own products?  When he gets really lost?
Maybe I should forgo his product and just cross my fingers - cut out one 
step.

-- 
---
BrianG
000
@[Google's email domain]
.com

Re: Silly and stupid post-condition or not ?

[Randy Brukardt]

"BrianG" <me@null.email> wrote in message news:jgq2j2$g67$1@dont-email.me...
...
> It sounds like you don't want SPARK (as it is now, at least), but 
> something like an Ada equivalent to LINT.  (Not an Ada version of lint, 
> but something that does for Ada what lint does for C - covers Ada's needs, 
> rather than C's.)

It's not "Lint" really, it's really something to find errors of omission. 
(Errors of commission are many times easier to find and fix, like using the 
wrong algorithm or subtracting rather than adding.)

And usually this boils down to proving the absence of and/or proper handling 
of exceptions. 90% of the interesting cases have something to do with 
exceptions: either exceptions that are raised when they're not expected or 
not handled when they are expected.

I also want to do this in the context of normal compilation, so that (a) 
there is immediate feedback about problems and (b) there is no temptation to 
skip the step and (c) because I'm not in a position to build another large 
tool. ;-)

OK, the last probably isn't that important, but finding out about the 
problems as early as possible is important.

                                            Randy.