Re: about the new Ada 2012 pre/post conditions

[stefan-lucks@see-the.signature]

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

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

A syntax for specifications. 

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

OK. 

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

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

That is a matter of taste. In any case, emacs rules. ;-)

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

I agree that dynamic accessibility checks have failed to become a good 
tool for reliable program development. But the standard requires no 
compiler switch to allow them turning on and off on demand -- in contrast 
to assertions and Ada 2012 conditions.I.e., the accessibility checks are 
really part of the language, the checks are a tool that you have the 
freedom to use or not to use!

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

Agreed. 

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

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

Sure! So what? 

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. 




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