Re: about the new Ada 2012 pre/post conditions

[Shark8 <onewingedshark@gmail.com>]

On Thursday, July 5, 2012 1:24:57 AM UTC-6, Dmitry A. Kazakov wrote:
> On Wed, 4 Jul 2012 19:58:31 -0700 (PDT), Shark8 wrote:
> 
> > Also, I don't know where you got the idea that pre- and post-conditions
> > must not implement anything.
> 
> Trivial:
> 
> IF pre-/post-condition is contract THEN they are not implementation
> [POV #2]
> ELSE ... [POV #1]

Now you're just restating what you said. If you mean something like "I take that to be axiomaatic" or "by definition [...]" there'd be something to discuss.

As is though you're just throwing out the assertion that pre- and post-conditions must not have an implementation. {Otherwise they're not *real*, *contracted* pre- post-conditions.} this strikes me as a bit... off, considering things from the other direction: how to implement [for lack of a better word] pre- and post-conditions most of the method you seem to be advocating is impossible (just like any user-input cannot be guaranteed correct w/o either having all user-input as permissible, or otherwise validating it) or difficult on the compile-time/static-analysis level.

> (Historically, pre-/post-conditions were invented by Dijkstra for the
> purpose of proving correctness. Later they were used for types to analyze
> substitutability issues etc.)

And isn't the idea with Ada's constructs to at least aid proving the correctness of a program? Furthermore, wouldn't it be preferable to throw an exception when the condition is violated? That seems to fit perfectly with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no?
 
> > If that was the case then, strictly speaking
> > JavaDoc's pre and postcondition annotating comments are superior to Ada's
> > pre and post condition because they don't implement anything and are, in
> > fact, just comments having no actual impact on the program text.
> 
> Not if condition proof fault makes the program illegal.

It does nothing, insofar as I know, regarding nprogram correctness. http://en.wikipedia.org/wiki/Java_annotation has as an example the "override" annotation which when violated only provides a warning.