Re: Silly and stupid post‑condition or not ?

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

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