From: Andrew Hunt <andy@...>
Date: 2000-09-13T04:26:27+09:00
Subject: [ruby-talk:4909] Re: [TOY] FL

    > I've written this small module, just to play with ruby.
    >
    > It has probably many bugs and  probably work only with this example, this
    > is *really* only a toy :-)

Well now you've let the cat out of the bag :-)

I wrote a DBC implementation a few weeks ago, but was waiting until
we had our web site in better shape before I unleashed it to the
world.

Mine's pretty similar; but a bit more automatic.  It takes care of all the
necessary calls to super, arranges for "old" values to be set correctly,
and such.  In my scheme, the invariants and pre/post conditions must
return true; otherwise, an appropriate DBC exception is thrown.

You don't need to inherit from anything special (you do need to
require 'dbc'), and you can selectively turn on/off various levels
of error reporting.

Perhaps we should work together on this instead of duplicating
effort?

Here's an excerpt from the documentation, hastily edited from
the LaTeX source (and not proofread!)

-------------------------------------------------------------

The specific features added to Ruby include Pre- and Postconditions,
"old" expressions, Invariants, and a basic assertion check.
Assertions made in a superclass apply to all subclasses.

Ruby source files that participate in DBC need to require 'dbc'
to get the following features.

Pre- and Postconditions
----------------------

Immediately following a method declaration, a precondition and/or a
postcondition may optionally be defined:

  def someMethod
    pre {
      {a code block that must evaluate to true...}
    }
    post {
      {a code block that must evaluate to true...}
    }
    ...
    {normal method code...}
    ...
  end

Invariants and postconditions specified in one class will be checked
in all subclasses as well, preconditions in a subclass will override
any parent's precondition.  You are allowed to weaken
  preconditions in a subclass, but can only strengthen
  postconditions.

The pre- and postcondition clauses may span several lines or may be placed
on a single line each.

old expressions
--------------

Postconditions may refer to expressions as they existed before the
method call with the syntax:

  old(expr)

This syntax is only valid within a postcondition; the parentheses are
required.

Result
------

Often a postcondition may want to verify the return value of its
method:

  DBC.result

For example, the following method asserts that the result of
alpha times two equals the original argument, x.

  def alpha(x)
    post { DBC.result * 2 == x }
    x/2
  end

Invariant
---------

Any class may define a method called invariant, which will be
called at the conclusion of any public instance method within the class.
A class's invariant must evaluate to true any time a public method
returns (by any means).

When the invariant is checked, any invariants that exist in superclasses 
are checked automatically.

The invariant should be the last method defined in a class.

Check
-----

To simply check an assertion in-line within a method, we have the following
routine:

  check "Descriptive string" { code block }

The code block must evaluate to true.

implies
-------

Many times you want to check a particular condition, but only if some
other condition is true.  For this we have the method implies:

  implies(a,b)

If a is true, then the return value of implies is the value of b.
If a is false, then the return value is true.  That is, you
only will get a false if ``a implies b'' is false---when a is true
and b is not.

Exceptions
----------

If a check, invariant, pre- or postcondition is violated
(i.e., the assertion returns false), an exception is raised with
the name of the type of the violation (invariant, precondition, etc.)
and a user-supplied message (if available).

Once an exception has been raised from an object, that object should
not be considered viable any more.  In particular, it may not detect
further contract violations correctly (since the state of the object
is already inconsistent, it probably won't do anything else correctly
either!)

Enabling/Disabling
------------------

By default, DBC is enabled with full checking.  To change the checks
which are performed, call DBC.enable with one or more of the
following flags or-ed together:

  DBC::PRE Check Precondition assertions 
  DBC::POST Check Postcondition assertions 
  DBC::INV Check Invariant assertions 
  DBC::CHECK Check ``check'' assertions
  DBC::NONE Don't check any assertions

Limitations
------------

dbc.rb must be able to find and parse the source code, so you
cannot pipe the program source into ruby, nor can you specify
assertions in an eval.

Assertions are only recognized within the context of methods in user
defined classes.  Top-level methods (implicitly of class Object)
will not be examined for assertions.

Your program may run a bit slower with all the extra checking.  In
particular, if the invariant is computationally expensive, you may see 
a dramatic difference.