Skip to content
sellout edited this page Apr 28, 2011 · 5 revisions

Quid Pro Quo is a contract programming library for Common Lisp in the style of Eiffel’s Design by Contract™.

Usage

(defclass stack ()
  ((size :initform 0 :reader size :type (integer 0))
   (capacity :initarg :capacity :reader capacity :type (integer 0))
   representation)
  (:documentation "A simple stack implementation for a contract example.")
  (:metaclass quid-pro-quo:contracted-class)
  (:invariants (lambda (object) (<= (size object) (capacity object)))
               (lambda (object) (eq (emptyp object) (= (size object) 0)))))

The preceding class definition illustrates some parts of the interface. First, notice the :metaclass option. This tells the compiler that this class has a contract attached to it. Second, note the :invariants option. This is a list of functions to execute whenever an accessor is called, both before and after the accessor runs. The third thing to note is the :type slot options. These are part of a normal defclass, of course, but depending on your compiler and optimize declarations, they may or not be checked already. Quid Pro Quo will check them whenever invariants are enabled.

(defgeneric unput (object)
  (:method-combination quid-pro-quo:contract)
  (:method :require "stack not empty" ((object stack))
    (not (emptyp object)))
  (:method ((object stack))
    (decf (slot-value object 'size)))
  (:method :ensure "size decreased & stack not full" ((object stack))
    (and (= (size object) (1- (quid-pro-quo:old (size object))))
         (not (fullp object)))))

Here is an example of contracts on a function. Note the :method-combination option. Much like :metaclass above, this tells the compiler there is a contract attached. The contract is compatible with the standard method combination, so you can have :around, :before, and :after methods, just like always. There are some new method qualifiers here, though. The first is :require. This indicates a test to be run before any of the standard methods. It should return true or false. You'll notice that after :require there is a string. This is used in the condition report in case the method fails (and in the function documentation in the future). The other new qualifier is :ensure, this works the same as :require except that it is run after the standard methods. It has a couple special features that don't exist elsewhere. The one you see in the example above is (old ⟦expression⟧). This is a macro that is only available in postconditions. It evaluates to the value of the contained expression from before the standard methods were called. This is useful for comparing a new value to the previous value.

NOTE: old is currently quite fragile. If you use it, try to put it as early in your postcondition as possible, so that exceptions and conditional evaluation don't prevent it from executing properly.

The other special feature in postconditions is (results). This evaluates to the values returned by the standard methods. You can see an example of that below.

(defmethod fullp :ensure "result matches definition" ((object stack))
  (eq (quid-pro-quo:results) (= (size object) (capacity object))))

Turning Off and On

Currently, you don't have that much control as to whether contracts are enabled or disabled. There are three features

  • :qpq-precondition-checks,
  • :qpq-postcondition-checks, and
  • :qpq-invariant-checks.

If these are not in *FEATURES* when Quid Pro Quo is loaded, no contract checking will happen at all. I recommend that you only do this when creating production images.

You can also specify which checks you want to perform on specific functions, like so

(defgeneric fullp (object)
  (:method-combination quid-pro-quo:contract :postcondition-check nil))

That function will not check preconditions. However, we really want to be able to specify which systems should be checked which ways. There is a tradeoff between contract checking and performance, so even in development you may not want to check everything.

A common setup is to

  1. check everything on your own code,
  2. check everything except postconditions on third-party code (postconditions are the most heavy-weight because of the special features like old, but mostly you disable these because a postcondition failure implies an error in the third-party library, and you might expect them to already be well-tested), and
  3. throw the big *FEATURES* switch in production, after everything is tested and performance is paramount.

We don’t currently have any way to specify this that integrates well with ASDF, but

(quid-pro-quo:enable-contracts (:invariants t :preconditions t :postconditions nil)
  (asdf:load-system :some-third-party-system)
  ...)

will do the right thing, and then you can load your own system, which may have dependencies specified on the systems loaded manually in ENABLE-CONTRACTS.

Clone this wiki locally