Re: about the new Ada 2012 pre/post conditions

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

On Mon, 25 Jun 2012 18:26:18 +0200, stefan-lucks@see-the.signature wrote:

> On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> Hilbert's program by no means was intended to justify logic or mathematics
>> themselves. This is outright wrong.
> 
> Hilbert's program was an attempt to re-build the very foundations of 
> Mathematics. No more, no less. See 
> <http://en.wikipedia.org/wiki/Hilbert%27s_program>. 

Right, and this had nothing to do with justification either logic or
mathematics by means of themselves. Such an epic task would rather be a job
for baron Muenchausen. Just scroll through the Hilbert's program list of
problems:

http://en.wikipedia.org/wiki/Hilbert_problems

>> If Ada precondition is neither implementation (#1) nor
>> specification/contract (#2) then what is it? 
> 
> A syntax for specifications. 

Syntax only?

>>> *Secondly*, you seem to overlook that there are three semantical options, 
>>> rather than the two you mention:
>>> 
>>>   1 ignore the conditions 
>>> 
>>>   2 check them dynamically at run time 
>>> 
>>>   3 prove them statically at compile time
>> 
>> I didn't:
>> 
>> Assuming #1, only no.2 is possible. #1 <=> no.2
>> 
>> Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or
>> no.2.
>> 
>> One *cannot* mix no.1/3 with no.2, that is what upsets me.
> 
> But you are not locked into either option 1, 2, or 3, you can choose, 
> without having to change the language, or to rewrite a single character 
> of your program source. 

Same syntax for things which are far more apart than just semantically
different. What a bizzare idea! You would be switching between contract
specification and implementation per compiler switch! Is this C
preprocessor or Ada?

>> That clearly precludes no.2: handling is within the checker, checker is
>> outside the testee.
> 
> Well, this separation is ideal. But most of the time, a testee that 
> discovers itself being in a faulty state (and that is, what a failed 
> dynamic check actually reveals), the testee is still able to write some 
> information to a log file. Sure, you can construct or find the odd 
> counterexample -- but in practice almost all the time this approach works.
> (OK, I am assuming your system allows to write some log output at all.) 

Tracing is OK, but what happens afterwards? If continuation is possible,
that requires some cleanup, rollback, retry etc, which has the goal of
putting the system into some definite state. This is not over before over.

>> And, very importantly, we want to contract exceptions some day, don't we?
> 
> Sure! So what? 

How are going to marry exceptions propagating from contracts with contracts
on exceptions? Some exceptions are more exceptional than others? Aren't we
fed up with Program_Error?
 
> Ada.Assertions.Assertion_Error is one exception like Constraint_Error or 
> the like. Either, you prove that this or that exception will not be 
> raised. Or you claim that such an exception is not raised. If it is 
> actually raised this is a violation of the contract. Which is a big deal 
> for, say, Constraint_Error, but not for Ada.Assertions.Assertion_Error ... 
> the exception that indicates the violation of a contract, anyway. (Assuming 
> that Ada.Assertions.Assertion_Error is not raised manually -- but no sane 
> programmer would do that.)
> 
> Actually, there is one exception that is difficult to specify. It is our
> old fellow 
> 
>     Storage_Error. 
> 
> On the level of source code analysis, you 
> actually cannot prove that this exception will not be raised.

Firstly, you if you don't want to prove anything about a certain exception,
you would add this exception to all contracts involved and take care about
exceptions of interest.

Secondly, you would rather prove conditionals, like: Storage_Error is not
propagated when given amount of memory is available in the specified pools.
This is good enough for most cases, which are not about any exact bound,
but about existence of such bound, i.e. about memory leak detection.

Thirdly, you would be able to provide axioms. E.g. for some complex
recursive operation, you could just specify the upper memory consumption
bound known to you from other sources, and let the prover to go with that
(the oracle).

I think conservative Storage_Errror proof is pretty doable. If you move the
upper bound a pair Kbytes upward it would eliminate most of problems.

We certainly could learn from Java mistakes rather than repeating them
(e.g. interfaces).

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