Re: about the new Ada 2012 pre/post conditions

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

On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote:

> On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> 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?
> 
> There is a well-defined syntax for contracts, and you can choose between 
> different ways to use them. But contracts are still contracts. No 
> relationship to the C preprocessor.

They are contracts when checked statically and implementations when checked
dynamically. It is like

   #define is :=

>>>> 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.
> 
> Don't do that! Emit your messages to to the log file and then terminate!

Contract violation => terminate. Exceptional state => recover.

> But then, what is more important:
> 
>   - Provide tools that support good software engineering practice?
> 
> or
>   
>   - Prohibit any tools that can be misused?
> 
> Dynamically checked contracts are such a tool. 

A wrench sold as shoe polish.

>>> 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.
> 
> So you just add "can raise Storage_Error" to any contract? (Maybe 
> implicitly.)

Contracts will be inheritable. I don't know how it goes with aspects, never
understood what they are good for, but true contracts are inherited while
possibly weakening pre- and strengthening post-conditions (LSP).

Another necessary contract mechanism is composition. That is when you pass
a downward closure to an operation, that could say: I raise what the
argument does. Note that this will require proper procedural types to have
interfaces to carry the contract with. E.g. you would be able to limit the
closure operation to what it is allowed to raise.

>> 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.
> 
> You are so violately against dynamically checked conditions ... and then 
> you propose some heuristic that you just claim to be "good enough for most 
> cases"?

Why does this surprise you? No contract can describe all semantics. It only
vaguely describes it. You may have all sorts of possible contracts with the
same implementation and conversely.

It is free choice how much of the semantics a contract to mandate: from few
in a trow away program to much for a mission critical one.

>> 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_Error proof is pretty doable. If you move the
>> upper bound a pair Kbytes upward it would eliminate most of problems.
> 
> Good luck with any recursive program.
> 
> And (I am sure you know this) any approach to really prove upper bounds 
> on the storage requirements would imply to solve the Halting Problem.

No problem. If you cannot prove it, that is compile error. It is a
conservative estimation, estimations have no halting problem issue, Boolean
values are bounded.

The real problem lies elsewhere. Prover to tell program legality is thin
ice. Depending on the technique used the same program could be legal (good
prover) or illegal (poor prover). I don't know how to address this, though
nobody cares anyway...

>> We certainly could learn from Java mistakes rather than repeating them
>> (e.g. interfaces).
> 
> Which is probably why Ada so far has no contracted exceptions. Not that 
> they cannot be done -- but nobody knows how to write such contracts that 
> they really become useful.

Huh, they didn't much hesitate to borrow flawed Java interfaces, although
the language already had abstract types.

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