Re: about the new Ada 2012 pre/post conditions

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

On Mon, 25 Jun 2012 16:08:01 +0200, stefan-lucks@see-the.signature wrote:

> I am not sure if I can cool down this heated discussion, but I'll give it 
> a try. 
> 
> On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote:
>> 
>>> Indeed, it helps to remember that logicians and mathematicians
>>> have learned that logic and mathematics cannot justify themselves.
>> 
>> No, they never ever did that. From very beginning mathematicians used
>> axiomatic approach instead. What they did, was constructing frameworks
>> within which one could not deduce both A and not A.
> 
> A bit off topic -- but this is not quite true. 
> 
> Firstly, the axiomatic approach has become mathematical mainstream only 
> since about the times of David Hilbert. The "very beginning" of 
> Mathematics and Logic are quite a bit earlier. ;-)

Euclid

> Secondly, Hilbert's program was to construct frameworks being both 
> complete (all correct conclusions should be deducible) and one should not 
> be able to deduce both A and not A. Kurt Goedel eventually showed that 
> this is *logically* impossible. 

Hilbert's program by no means was intended to justify logic or mathematics
themselves. This is outright wrong.

>> Is SPARK nothing? Is strong typing nothing?
>>
>> But you seemingly did not read what I wrote earlier. There is either #1 or
>> #2. 
> 
> This the axiom that *you* choose to start with. Starting from there, your 
> reasoning may be logically correct.

If Ada precondition is neither implementation (#1) nor
specification/contract (#2) then what is it? Since nobody ever came with
#3, I considered only #1 and #2.
 
> *Firstly*, you don't seem to separate between syntax and semantic. 

I said nothing about the syntax. It could be better, but syntax is always
the most difficult part.

> *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.

> Even SPARK may soon support the Ada 2012 syntax for its annotations.

That is OK to me, however, considering syntax I wished a clearer separation
of pre-/post-conditions from other declarations. But since GPS rules, I
suppose it would not be much difficult to have a view cutting
pre-/post-conditions off and displaying them in a side-by-side window
scrolled upon mouse hovering etc.

> *Thirdly*, you seem to assume that a tool that can be used in a 
> destructive way cannot also be used properly.

In this particular case (#2 + no.3) we wave a very strong evidence:
accessibility checks. It was a disaster.

> The support for the second option is such a tool. I agree with you, any 
> program that claims some preconditions, postconditions and invariants 
> should stop and must be fixed when any such check fails. Silently handling 
> the exception and then continuing is 
> 
>   - a logical contradiction in itself, and also
> 
>   - the result from some lousy programming practice.
> 
> There is no justification for handling the exception instead of fixing the 
> flaw!
> 
> But the same tool can properly be used for debugging and testing -- if any 
> assertion fails, and you detect this at run time, write all relevant 
> details into a log file, stop the program, and fix the bug.

No objection whatsoever. I covered this case earlier. It is OK to check
dynamically under the condition that the checker is an *independent*
program. A debugger, checker, reasonably protected Ada run-time verifying
preconditions and *handling* failed checks is perfectly consistent and
advisable.

That clearly precludes no.2: handling is within the checker, checker is
outside the testee.

And, very importantly, we want to contract exceptions some day, don't we?
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de