Ian, This is a bittersweet review for this old hand at reasoning over program assertions. There's more to the PIP-condition assertions than Contract programming. Similar annotations can be used for program proof of correctness.
I'm probably one of the few programmers you'll meet that's actually more than once proven a program correct in anger at $DayJob. (There are others, I'm sure, but most are classified, so if you meet them they can't tell the war story -- but one of mine was live on the WWW in our MedLine search's ad-server function: http://web.archive.org/web/19970126214107/www.avicenna.com/tour/etour4.h tm ) I was trained on Ottawa Euclid for mythical A2 level security, with software proof assistance, but my "in anger" usages were in C, using comments and a #2 pencil for proof. Once a decade I find a loop that will be too nasty to debug by usual techniques and really needs to be coded right the first time ... so I do a Dijkstra/Hoare loop invariant analysis to compute the post-condition from the pre-condition and the invariant behavior. Note that my practical use is the reasoning *over* the assertions, not the checking of them at run-time. This does not need to involve class invariants or function/method precondition/postcondition, but rather the loop-invariant/pre/post. As far as I can tell, your Class::Agreement while supporting functional agreements in addition to OO does not support loop pre/inv/post unless I switch to recursion? When doing the real code-to-spec proof as I've done, you don't need to run the assertions in production forever. The assertions should be checked in test to verify that the code really does agree with the assertions, but the reasoning over the assertions is the real validation of the algorithm. When the invariant of interest is on each pass of the inner loop, you really do want it OFF in production. An object invariant that I've seen in vendor-supplied framework code (and we saw it assert, too) is the equivalent of invariant { is_sorted( $self->data ) } which is a little expensive (*merely* O(N)) to call twice around each method call and prohibitive (O(N**2)) on recursive method calls. Part of the behavior of operations maintaining a linked list or balanced tree is that the list/tree stays sorted if it starts sorted. If there isn't a way to shut off contract enforcement efficiently, can it really be applied to interesting ordered datastructures of the sort that really need assertions? As I mentioned in reply to a question/comment last night, examples like the postcondition for a factoring routine ( product(@$result)==$input) and the above invariant on an ordered list/tree, might help show that postconditions aren't just re-doing the implementation in general, but checking the visible behavior of it without doing the full implementation (when interesting enough that there is a difference). Cheers, -- Bill / N1VUX _______________________________________________ Boston-pm mailing list Boston-pm@mail.pm.org http://mail.pm.org/mailman/listinfo/boston-pm
