Re: Silly and stupid post‑condition or not ?

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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