Re: Silly and stupid post‑condition or not ?

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

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