Re: Silly and stupid post‑condition or not ?

[stefan-lucks@see-the.signature]

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 

     function F(X: Natural) return Natural 
        with Post => (if (X mod 2) = 1 then ...); 

   We don't have any precondition. For even X, we don't even have a 
   postcondition. But using the partial postcondition we have, we can 
   completely define the semantic behavior of 

     Y := F(X) * (F(X) mod 2); 

   If that is all what we need F for, why should we bother with any 
   postcondition or even X? 

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. E.g., for a database with confidential 
   and non-confidential data, we be very happy to prove that any response 
   to a query from an unauthorized entity will be derived from 
   non-confidential data only. You have proven your system to be secure!

   A system may be secure but still be not quite functional. E.g., you may 
   further like to prove that the response to a query from an authorized 
   entity will be derived from all data, the confidential and the 
   non-confidential ones. If you can, fine! Otherwise, apply conventional 
   means ... 

   In fact, some relevant contract requirements may actually be hard to 
   specify. What is the "correct" answer in some informational retrieval 
   setting (e.g., when you google for "Dmitry A. Kazakov")? Do you really 
   propose not to formally specify anything, just because we cannot specify 
   everything?

   This is pretty much the same in the real world. When you go to a 
   restaurant and order a meal, you expect a tasty meal. But the end, 
   being "tasty" is ... a matter of taste. If you have no other complaints 
   than "it wasn't to my taste", you still have to pay the bill. Thus, 
   being "tasty" is expected by the customer, but not part of the 
   postcondition. On the other hand, certain  hygienic standards are 
   defined binding laws for all restaurants (in a given country or state). 
   This is actually a postcondition, inherited from the abstract class of 
   "all restaurants in my country". Would you claim that hygienic 
   standards are useless, because you cannot define tasty Ness?

Back to the original poster's question:

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

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