> 2. You must be able in the postcondition to access the values of
>    variables as they were on entry to the method. For example
>
> We know how to do (1) from within Ruby (that is by writing just Ruby
> code). We haven't worked out how to do (2) yet...

Well, I would have thought 1 was harder than 2. But the
method I am thinking of is pretty clunky.

Basically you have to call pre and post for every 
method (they in turn will call the class's pre- and
post-condition functions and the invariant). I think
this mostly takes care of inheritance, since each
method can call its parent method, up the chain.

This is the bad part, that it isn't "automatic."

The parameters at the end of the "pre" call are 
basically a list of named assertions. But among them
are expressions tagged with a reserved name "old" (to
preserve the value for comparison at the end). These
are just saved in a hash. They need not even be
simple variables (although they shouldn't have side
effects, of course).

  def some_method
     pre(binding, %w[ non_neg:x>=0 small:x<10 old:x old:y ])
     #...
     post(binding, retval, %w[ bigger:x>old(x) ])
  end


Scope of the hash is not quite trivial, since it has
to be visible to both pre and post... haven't thought
it through yet.

Of course, I would like to make the calling of pre
and post "automatic" -- when there are no local 
conditions, the inherited ones should still be checked.

I thought of some elaborate hare-brained Rube Goldberg
device whereby a method is aliased and renamed or
whatever, so that when you call the "bare" method
foobar, you really end up calling meta_foobar, which
calls pre, then foobar, then post. 

But even if I succeeded in doing that, I'm not sure I 
could sleep at night.  :)

Hal