Re: Silly and stupid post‑condition or not ?

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

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