Re: Silly and stupid post‑condition or not ?

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

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