Re: Silly and stupid post‑condition or not ?

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

On Wed, 1 Feb 2012 17:37:28 +0100, stefan-lucks@see-the.signature wrote:

> On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote:
> 
>> On Wed, 1 Feb 2012 11:37:31 +0100, stefan-lucks@see-the.signature wrote:
>> 
>>> 1. For the purpose of proving program correctness,
>> 
>> Proving incorrectness, you mean, since the thing is partial.
> 
> With apologies to you and all the c.l.a readers, there was a really bad 
> typo in my example. So here is the correct example
> 
>      function F(X: Natural) return Natural 
>         with Post => (if (X mod 2) = 1 then ...); 
> 
> So any program, which's correctness depends on a statement such as 
> 
>      Y := F(X) * (X mod 2); -- not "F(X) * (F(X) mod 2)", as I wrote before
> 
> may be proven correct (there is nothing "partial" here), in spite of the 
> incomplete postcondition for F. 

You could it have much simpler. Consider programs which do not call F at
all. That does the trick too.

The idea of pre-/postcondition is that it tells something about a set of
programs, of all legal programs actually. If you wanted to narrow that set,
then, well, you should at least specify that set.

>>> 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.
> 
> I see. However, I would claim that an incomplete postcondition actually 
> "distinguishes the provable/specified/defined part from the rest", as you 
> put it.

It is a cart before the horse. In Ada we believe that specifications come
first. Yes, for each given program there exists a specification wich would
fit it. Bad design.

>   procedure Ask_Database(U: User; Q: Query; R: out Response)
>     with post(if (not Authorized(U)) and (Asks_For_Secret_Stuff(Q)) 
>               then R=Empty_Response);

BTW, contracts to be stated in terms of equivalence rather than
implications. I.e.

   R=Empty_Response <=> not Authorized(U)) or ...

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de