Re: Silly and stupid post‑condition or not ?

[stefan-lucks@see-the.signature]

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. 

I.e., value of Y is predictable. If X is odd, one needs the postcondition 
to predict Y. If X is even, then Y is 0, regardless of the value of F(X). 
But note that I follow the SPARK-inspired assumption that for even X, F(X) 
can be any value of the given type, but computing F(X) must not propagate 
an exception!

I didn't actually try it, but I am sure that I could verify the 
correctness of a SPARK program with such a structure. Of course, SPARK 
would still force me to actually prove that F doesn't raise an exception, 
even for the case of X being even. Furthermore, the good thing about SPARK 
is that it would have thrown a bunch of unprovable verification conditions 
at me, had I tried to verify the example with the typo. 

Unfortunately, Ada 2012 lacks a way to specify a subprogram not to 
propagate an exception (*). Waiting for Ada 2020! 

> > 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. E.g., specifying (or even better, proving)

  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);

for some applications would be a big deal, even though there are four 
different cases for the postcondition (any combination of the Booleans 
Authorized(U) and Asks_For_Secret_Stuff(Q), and only one of these four 
cases is formally specified. 

---- 
(*) Of course, by the language's own means, without gnatmem or some other 
    tool, one can actually be never really sure about Storage_Error ...

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