Re: about the new Ada 2012 pre/post conditions

[stefan-lucks@see-the.signature]

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. ;-)

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. 

But back to the real topic. 

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

But actually, by choosing that axiom as your logical starting point, you 
have made several logical errors by yourself. 


*Firstly*, you don't seem to separate between syntax and semantic. 

Ada 2012 provides pre- and postconditions (and also invariants) allow to 
*specify* contracts. That is a great advantage over writing more or less 
informal contracts -- and even to SPARK's annotations inside Ada comments.

This is a syntax for specifications, no more, no less! What is wrong with 
that syntax? If you like SPARK, you should welcome it!

So much about syntax, now comes the semantic. 


*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

The language requires the compiler to support the first two, but the 
language allows the third one just as well. I anticipate that we will soon 
see tools to support proving Ada 2012 annotations statically. Even SPARK 
may soon support the Ada 2012 syntax for its annotations.


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

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. Which is what 
you try do do without dynamic checks, or by writing your 

  pragma Assert(...)

in current Ada, just as well!

Used that way, dynamic checks in Ada 2012 will ease testing and debugging. 
Which is good!



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