On Wed, 6 May 2015, Randy Brukardt wrote:

> If that's all Ada is going to be used for, it's completely irrelevant what
> features it has. I would never have used Ada personally if that was the
> case. Ada (IMHO) is a language to write (more) correct programs, no matter
> what kind of programs you write.

Good point!

> The basic idea behind the preconditions in Ada 2012 is to give a way for
> people (and implementations and tools as well) to ease into using additional
> checking and proof.

Actually, the first thing is to ease writing and maintaining proper 
specifications, disregarding either run-time checks or proofs. One could 
see them as enhanced comments. Quite often I have seen something like

   function Divide(Dividend, Divisor: Numeric_Type) return Numeric_Type;
   -- requires Y /= 0.0

This is a simplistic example, where one can easily guess that someone has 
changed the name of the parameter "Y" into "Divisor". But in reality, this 
is not always so obvious.

> Almost no one is willing to submit to the horrors of complete 
> description of entities as required by SPARK.

Actually, you don't need *complete* descriptions for SPARK. Often, 
verifying incomplete descriptions can be useful. Of course, the static 
verification will only verify the properties you describe.

> But (almost?) everyone using Ada would be interested in improving the 
> correctness of their programs, one assertion at a time.

That is the point.

> By extending those mechanisms (via predicates and preconditions) to
> arbitrary expressions, we allow much more such error detection to occur.

Agreed!

> I don't believe that checks in Ada (of any kind) should ever be turned off.

Here, I heavily disagree. Often, checking relevant properties is much to 
expensive to perform the checks them in production code.

A simple example is binary search over a sorted array. The precondition 
requires the array to be sorted. If the compiler succeeds in optimising 
the test away, it is equivalent to a static program verifier proving the 
precondition holds when the binary search is called. If the compiler fails 
to optimise the check away, the execution time goes up from logarithmic to 
linear. If you can live with that, you don't need binary search!

Actually, one thing I am missing from Ada 2012 is a convenient and 
fine-grained way to tell the compiler which pre- and postconditions and 
invariants are to be checked, and which checks are to be skipped.

Most urgently, I would expect an option to skip checking ordinary pre- and 
postconditions, without skipping those that explicitly raise some 
exceptions. The point is, these two forms of precondition are semantically 
totally different:

The semantic of a plain precondition is essentially:

   * If I a True, the postcondition will hold.
     Never call the subprogram if I am false!!!
     Otherwise, the subprogram might do anything.

This is a precondition in the "Design by Contract" sense.

A typical example for this would be "the array is sorted" when calling 
binary search. If you call a binary search routine with an unsorted array,
you will likely get false results. And you deserve the blame!

The semantic of a precondition with something like "else raise 
This_Exception" is

   * If I am True, the postcondition will hold
     when the subprogram terminates.
     If I am False, the subprogram will not do anything,
     except for raising This_Exception.

A typical example for this kind of precondition would be "the file exists" 
when trying to open a file. (BTW, I would prefer a phrase different from 
"precondition" for this kind of thing, but that appears to be too late for 
Ada, now.)

Maybe, Ada 202X could include something like

   with Pre => ... -- plain precondition, can be turned off
        Pre'Check => ... -- must be checked at run time

> I also don't believe in separate proof tools. That's something that should
> be a basic part of the compiler (it has to be to do optimization, check
> elimination, and the like anyway). The difficult question is how to feed
> information about those things (particular checks known to fail) back to the
> programmer (as optimization phases tend to run without messages, and the
> messages that they do give are rather non-specific). In order for proof to
> be part of the compiler, the proof language has to be part of the language.

Did you try out SPARK 2014? The proof language is part of the language, 
and with a proper usage of gnat project files, calling the prover becomes 
as much part of the compilation process as calling the syntax checker.

Stefan


------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--