Re: about the new Ada 2012 pre/post conditions

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote:
...
> They are contracts when checked statically and implementations when 
> checked
> dynamically.

No, they're always contracts. They certainly aren't "implementation", 
because they do *not* belong to the subprogram; they're checked *before* the 
subprogram is called. (The check, if any, belongs to caller, not the 
callee.)

Besides, I don't understand why it is such a disaster to have precondition 
contracts be dynamically evaluated in some cases, while it is OK to have a 
postcondition be dynamically evaluated in some cases -- it too is a contract 
(one that is evaluated *after* the subprogram finishes).

In any case, you want to prevent the any mechanism for specifying these 
things in code rather than in comments are currently. It should never be 
necessary for anyone to look into the body ("implementation") of a routine 
to see the contract (static or dynamic); tools that have to see within 
bodies (that is, only operate on all of the source) are close to useless 
(since they can only be used at the end of the development cycle when fixing 
bugs is at its most expensive).

...
>> So you just add "can raise Storage_Error" to any contract? (Maybe
>> implicitly.)
>
> Contracts will be inheritable. I don't know how it goes with aspects, 
> never
> understood what they are good for, but true contracts are inherited while
> possibly weakening pre- and strengthening post-conditions (LSP).

Yes, of course. Class-wide preconditions are inherited (potentially with 
weakening, although that's almost never useful), as are class-wide 
postconditions (with strengthening). (Don't use specific preconditions and 
postconditions if you care about inheritance.)

> Another necessary contract mechanism is composition. That is when you pass
> a downward closure to an operation, that could say: I raise what the
> argument does. Note that this will require proper procedural types to have
> interfaces to carry the contract with. E.g. you would be able to limit the
> closure operation to what it is allowed to raise.

I agree with the need for composition; we had that in the never-finished 
"global in/out" contracts. But that doesn't require "procedural types" 
per-se; it can be done quite easily with the existing facilities. (Whether 
the result really would be any good, I can't say, but I'm pretty sure that 
the existence of "procedural types" would make no difference in how useful 
is is.)

...
> The real problem lies elsewhere. Prover to tell program legality is thin
> ice. Depending on the technique used the same program could be legal (good
> prover) or illegal (poor prover). I don't know how to address this, though
> nobody cares anyway...

I think some of us care, the problem is assuming that the prover can prove 
everything important (that will never, ever happen). For me, the biggest 
impediment is coming up with rules that would allow proving what they can 
without (a) requiring too much of all compilers and (b) bounding what an 
implementation can do. There's clearly a portability problem here -- it's 
quite possible that that problem will prevent ever implementing exception 
contracts in the Ada language (as opposed to specific implementations).

                      Randy.