Re: about the new Ada 2012 pre/post conditions

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

On Tue, 26 Jun 2012 16:54:45 +0200, stefan-lucks@see-the.signature wrote:

> On Tue, 26 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> 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...
> 
> It is even worse! An Ada program is either legal or not.

It is an old problem. Not every legal program is compilable:

   X : constant := 2**(2**<compiler-dependent>);

> It would be a 
> fatal mistake to make legality depend on the theorem prover one is using. 

You cannot avoid this. The problem is to find right balance by moving most
variations out of the sensitive area.

> That is precisely the reason for checked contracts: Within the language, 
> we cannot prove them. With additional tools, we may be able to prove at 
> least some of them. The tools will improve over time -- hopefully faster 
> than new Ada standards arrive. In the mean time, we can do our best to 
> figure out contract violations by testing. That means, dynamic checks in 
> the test cases.

I don't believe in tools. A full integration of the prover would open a
completely new level of engineering, when amount of static checks could be
adjusted by the programmer incrementally as the project matures by adding
or removing goals to prove.

>>>> 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.
> 
> Yes, indeed. With respect to borrowing ideas from Java, the ARG has 
> learned!

Nope, they just switched to Eiffel.

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