Re: Silly and stupid post‑condition or not ?

[stefan-lucks@see-the.signature]

On Thu, 2 Feb 2012, Dmitry A. Kazakov wrote:

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

Why?

These implications are what you would typically find in a security 
requirements specification. (In human-readable way, such as "if an 
unauthorized user asks for any confidential data, no answer is provided by 
the XY system.")

What is the point of rewriting this in terms of equivalence? You run the 
trouble of proving that your rewritten contract is logically equivalent to 
the requirements specification. (Or you risk proving your program correct 
with respect to an incorrect spec.)

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------