From: Rainer Joswig
Subject: Re: DBC in Lisp (was: Stepanov *does* want OOP?)
Date: Sat, 10 Oct 1998 00:00:00 +0000
Message-ID: <joswig-1010981937490001@194.163.195.67> In article <·················@gauss.muc.de>, ··@gauss.muc.de (Matthias
H�lzl) wrote:
> style by most authors.) I have appended a simple DBC-library for CLOS
Good work.
I have changed it a bit. It now has its own package
and uses DEFCLASS.
Looks clean.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Design by Contract in Common Lisp
(cl:defpackage "DESIGN-BY-CONTRACT"
(:use "COMMON-LISP")
(:nicknames "DBC")
(:shadow cl:defclass)
(:export "DBC" "DEFCLASS"))
(in-package "DBC")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; the method combination DBC
(define-method-combination dbc ()
((precondition (:precondition))
(around (:around))
(invariant (:invariant))
(before (:before))
(primary () :required t)
(after (:after))
(postcondition (:postcondition)))
(flet ((call-methods (methods)
(mapcar #'(lambda (method)
`(call-method ,method nil))
methods)))
(let* ((form (if (or before after (rest primary))
`(multiple-value-prog1
(progn ,@(call-methods before)
(call-method ,(first primary)
,(rest primary)))
,@(call-methods (reverse after)))
`(call-method ,(first primary) nil)))
(around-form (if around
`(call-method ,(first around)
(,@(rest around)
(make-method ,form)))
form))
(inv-form (if invariant
`(multiple-value-prog1
(progn
,@(call-methods (reverse invariant))
,around-form)
,@(call-methods invariant))
around-form))
(pre-form (if precondition
`(progn
,@(call-methods (reverse precondition))
,inv-form)
inv-form))
(post-form (if postcondition
`(multiple-value-prog1
,pre-form
,@(call-methods postcondition))
pre-form)))
post-form)))
(defun getf-and-remove (name list &optional acc)
(if (null list)
(values nil (reverse acc))
(if (eql (caar list) name)
(values (cadar list) (append (reverse acc) (rest list)))
(getf-and-remove name (rest list) (cons (first list) acc)))))
(defun define-slot-generics (slot)
(let ((accessor (getf (rest slot) :accessor)))
(let ((reader (or (getf (rest slot) :reader)
accessor))
(writer (or (getf (rest slot) :writer)
(when accessor
`(setf ,accessor)))))
(list (when reader
`(ensure-generic-function
',reader
:lambda-list '(object)
:method-combination #-mcl '(dbc:dbc)
#+mcl (ccl::%find-method-combination nil 'dbc nil)))
(when writer
`(ensure-generic-function
',writer
:lambda-list '(new-value object)
:method-combination #-mcl'(dbc:dbc)
#+mcl (ccl::%find-method-combination nil 'dbc nil)))))))
(defun define-slot-accessor-invariants (class slot)
(let ((accessor (getf (rest slot) :accessor)))
(let ((reader (or (getf (rest slot) :reader)
accessor))
(writer (or (getf (rest slot) :writer)
(when accessor
`(setf ,accessor)))))
(list (when reader
`(defmethod ,reader :invariant ((object ,class))
(check-invariant object)))
(when writer
`(defmethod ,writer :invariant (value (object ,class))
(declare (ignore value))
(check-invariant object)))))))
(defun define-check-invariant-method (invariant class)
`((ensure-generic-function 'check-invariant
:lambda-list '(object)
:method-combination #-mcl '(dbc)
#+mcl (ccl::%find-method-combination nil 'dbc nil))
(defmethod check-invariant ((object ,class))
(funcall ,invariant object))))
(defmacro defclass (&body body)
(destructuring-bind (name supers &optional slots &rest options)
body
(multiple-value-bind (invariant new-options)
(getf-and-remove :invariant options)
`(progn
,@(if slots
(apply #'append
(mapcar (lambda (slot)
(define-slot-generics slot))
slots))
'())
(cl:defclass ,name ,supers ,slots
,@new-options)
,@(when invariant
(define-check-invariant-method invariant name))
,@(when slots
(apply #'append
(mapcar (lambda (slot)
(define-slot-accessor-invariants
name slot))
slots)))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; End Of File
; Example use:
(cl:defpackage "DBC-TEST"
(:use "DBC" "CL")
(:shadowing-import-from "DBC"
"DEFCLASS" "DBC"))
(in-package "DBC-TEST")
(defclass foo0 ()
())
(defclass foo1 (foo0)
((a :accessor foo-a :initform 3)
(b :accessor foo-b :initform 4))
(:invariant (lambda (object)
(with-slots (a b) object
(assert (< a b) (a b))))))
(let ((foo (make-instance 'foo1)))
(setf (foo-a foo) 3))
(defgeneric bar (foo)
(:method-combination dbc))
(defmethod bar :precondition ((foo foo1))
(with-slots (a) foo
(assert (< a -1) (a))))
(defmethod bar :precondition ((foo foo0))
(with-slots (a) foo
(assert (< a 0) (a))))
(defmethod bar ((foo foo1))
(princ foo))
(let ((foo (make-instance 'foo1)))
(setf (foo-a foo) -2)
(bar foo))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
--
http://www.lavielle.com/~joswig From: Matthias H�lzl
Subject: Re: DBC in Lisp (was: Stepanov *does* want OOP?)
Date: Sun, 11 Oct 1998 00:00:00 +0000
Message-ID: <864stbopva.fsf@gauss.muc.de> [comp.object and comp.eiffel removed since this is no longer relevant]
······@lavielle.com (Rainer Joswig) writes:
> In article <·················@gauss.muc.de>, ··@gauss.muc.de (Matthias
> H�lzl) wrote:
>
> > style by most authors.) I have appended a simple DBC-library for CLOS
> I have changed it a bit. It now has its own package
> and uses DEFCLASS.
I have reworked it some more and added a tiny amount of documentation
so that others might find it more useful. The main improvements are
that now weakening of preconditions is handled correctly without
having to manually build the disjunction, furthermore
pre-/postconditions and invariants can now be defined as predicates
and an error will be signalled if they evaluate to false.
Matthias
;;; dbc.lisp
;;; Design by Contract in Common Lisp.
;;; =================================
;;; One of the outstanding features of the Eiffel language is that it
;;; supports a concept called Design by Contract. A comprehensive
;;; description is given in
;;;
;;; Object Oriented Software Construction, 2nd ed.
;;; Bertrand Meyer
;;; Prentice Hall PTR, 1997
;;; ISBN 0-13-629155-4
;;;
;;; but the key point of DBC is that the relationship between a class
;;; and its clients is specified by a contract: There are certain
;;; conditions that the caller of a method specialized on a class has
;;; to fulfill so that the method can do its job (the preconditions)
;;; and the method guarantees certain things after its completion (the
;;; postconditions). Furthermore a class may have certain properties
;;; that are always true about that class; these properties are called
;;; invariants.
;;;
;;; This file contains an implementation of DBC for CLOS. Pre- and
;;; postconditions as well as invariants are specified by qualified
;;; methods of type dbc; the usual before, after and around method
;;; combinations are available for these methods as well.
;;;
;;; The code was written by Matthias H�lzl (··@gauss.muc.de) and is
;;; placed in the public domain. Rainer Joswig added the package
;;; definition and MCL patches. The most recent version of this file
;;; should be available at <http://www.muc.de/~hoelzl>.
;;;
;;; Have fun,
;;; Matthias
;;;
;;;
;;; Change Log.
;;; ==========
;;;
;;; 1998-10-07 Matthias H�lzl <··@gauss.muc.de>
;;; * Initial version.
;;; * Changed handling of pre-/postconditions and invariants to
;;; match Eiffel's behavior more closely. Errors are now signalled
;;; by the method combination.
;;;
;;; 1998-10-11 Rainer Joswig
;;;
;;; * Added package definition.
;;; * Added MCL patches.
;;;
;;; 1998-10-11 Matthias H�lzl <··@gauss.muc.de>
;;; * Added default method for `check-invariant'.
;;; * Removed `(ensure-generic-function 'check-invariant)' from
;;; `define-check-invariant-method'.
;;; * Changed method combination type of `check-invariant' to
;;; standard method combination.
(cl:defpackage "DESIGN-BY-CONTRACT"
(:use "COMMON-LISP")
(:nicknames "DBC")
(:shadow cl:defclass cl:make-instance)
(:export "DBC" "DEFCLASS" "MAKE-INSTANCE"))
(in-package "DBC")
;;; The method combination DBC.
;;; ==========================
(define-method-combination dbc ()
((precondition (:precondition))
(around (:around))
(invariant (:invariant))
(before (:before))
(primary () :required t)
(after (:after))
(postcondition (:postcondition)))
(flet ((call-methods (methods)
(mapcar #'(lambda (method)
`(call-method ,method))
methods)))
(let* ((form (if (or before after (rest primary))
`(multiple-value-prog1
(progn ,@(call-methods before)
(call-method ,(first primary)
,(rest primary)))
,@(call-methods (reverse after)))
`(call-method ,(first primary))))
(around-form (if around
`(call-method ,(first around)
(,@(rest around)
(make-method ,form)))
form))
(pre-form (if precondition
`(if (or ,@(call-methods precondition))
,around-form
(error "Precondition failure."))
around-form))
(post-form (if postcondition
`(multiple-value-prog1
,pre-form
(unless (and ,@(call-methods postcondition))
(error "Postcondition failure.")))
pre-form))
(inv-form (if invariant
`(multiple-value-prog1
(progn
(unless (and ,@(call-methods
invariant))
(error
"Invariant violation before method call."))
,post-form)
(unless (and ,@(call-methods invariant))
(error
"Invariant violation after method call.")))
post-form)))
inv-form)))
(defun getf-and-remove (name list &optional acc)
"Find NAME in the alist LIST. Returns nil as first value if NAME is
not found, the valus associated with NAME otherwise. The second value
returned is LIST with the first occurence of pair (NAME value)
removed."
(if (null list)
(values nil (reverse acc))
(if (eql (caar list) name)
(values (cadar list) (append (reverse acc) (rest list)))
(getf-and-remove name (rest list) (cons (first list) acc)))))
(defun define-slot-generics (slot)
"Returns a list with the reader and writer generic functions for a slot.
The generic functions have method combination type `dbc'."
(let ((accessor (getf (rest slot) :accessor)))
(let ((reader (or (getf (rest slot) :reader)
accessor))
(writer (or (getf (rest slot) :writer)
(when accessor
`(setf ,accessor)))))
(list (when reader
`(ensure-generic-function
',reader
:lambda-list '(object)
:method-combination #-mcl '(dbc:dbc)
#+mcl (ccl::%find-method-combination nil 'dbc nil)))
(when writer
`(ensure-generic-function
',writer
:lambda-list '(new-value object)
:method-combination #-mcl'(dbc:dbc)
#+mcl (ccl::%find-method-combination nil 'dbc nil)))))))
(defun define-slot-accessor-invariants (class slot)
"Returns a list with method definitions for reader and writer
invariants."
(let ((accessor (getf (rest slot) :accessor)))
(let ((reader (or (getf (rest slot) :reader)
accessor))
(writer (or (getf (rest slot) :writer)
(when accessor
`(setf ,accessor)))))
(list (when reader
`(defmethod ,reader :invariant ((object ,class))
(check-invariant object)))
(when writer
`(defmethod ,writer :invariant (value (object ,class))
(declare (ignore value))
(check-invariant object)))))))
(defun define-check-invariant-method (invariant class)
"Returns a list containing the method on CHECK-INVARIANT specialized
for CLASS and executing INVARIANT."
`((defmethod check-invariant ((class ,class))
(when (funcall ,invariant class)
(call-next-method)))))
(defmacro defclass (&body body)
(destructuring-bind (name supers &optional slots &rest options)
body
(multiple-value-bind (invariant new-options)
(getf-and-remove :invariant options)
`(progn
,@(if slots
(apply #'append
(mapcar (lambda (slot)
(define-slot-generics slot))
slots))
'())
(cl:defclass ,name ,supers ,slots
,@new-options)
,@(when invariant
(define-check-invariant-method invariant name))
,@(when slots
(apply #'append
(mapcar (lambda (slot)
(define-slot-accessor-invariants
name slot))
slots)))))))
(eval-when (:compile-toplevel :load-toplevel :execute)
(defgeneric check-invariant (object)
(:documentation
"Methods on the generic `check-invariant' are used by the dbc
method combination to perform the invariant check and should not
directly be defined by the user."))
) ; eval-when
(defmethod check-invariant (object)
"Default invariant, always true."
(declare (ignore object))
t)
(defmethod make-instance (class &rest initargs)
(let ((class (apply #'cl:make-instance class initargs)))
(unless (check-invariant class)
(error "Invariant failure after class creation."))
class))
;;; End of file dbc.lisp
;;; dbc-test.lisp
;;;
;;; Tests for the dbc package.
(cl:defpackage "DBC-TEST"
(:use "DBC" "CL")
(:shadowing-import-from "DBC"
"DEFCLASS" "MAKE-INSTANCE" "DBC"))
(in-package "DBC-TEST")
(eval-when (:compile-toplevel :load-toplevel :execute)
(defgeneric test-dbc (arg1 arg2) (:method-combination dbc))
) ;; eval-when
(defmethod test-dbc ((m integer) (n integer))
(print " >> test-dbc (integer integer)")
(list m n))
(defmethod test-dbc :around ((m integer) (n integer))
(print " >> test-dbc (around)")
(call-next-method))
(defmethod test-dbc :precondition ((m fixnum) (n integer))
(print " >> precondition (fixnum integer)")
(> m 123))
(defmethod test-dbc :precondition ((m integer) (n fixnum))
(print " >> precondition (integer fixnum)")
(< n 100))
(defmethod test-dbc :precondition ((m integer) (n integer))
(print " >> precondition (integer integer)")
(= m 12345678900987654321))
(defmethod test-dbc :postcondition ((m integer) (n fixnum))
(print " >> postcondition (integer fixnum)")
999)
(defmethod test-dbc :postcondition ((m integer) (n integer))
(print " >> postcondition (integer integer)")
t)
(defmethod test-dbc :invariant ((m integer) (n integer))
(print " >> invariant (integer integer)")
'foo)
(defmethod test-dbc :invariant ((m fixnum) (n integer))
(print " >> invariant (fixnum integer)")
'foo)
(defmethod test-dbc :invariant ((m integer) (n fixnum))
(print " >> invariant (integer fixnum)")
'foo)
(defmethod test-dbc :before ((m integer) (n integer))
(print " >> before (integer integer)")
(list (- m 1) (- n 1)))
(defmethod test-dbc :after ((m integer) (n integer))
(print " >> after (integer integer)")
(list (+ m 1) (+ n 1)))
#| Example:
(test-dbc 1 2)
|#
(eval-when (:compile-toplevel :load-toplevel :execute)
(defclass foo ()
((my-slot :accessor my-slot :initform nil)
(your-slot :accessor your-slot :initform t))
(:invariant (lambda (class)
(format t "~& >> Invariant check for class ~A~%"
class)
t)))
(defclass bar (foo)
((yet-another-slot :accessor yet-another-slot :initform 'yas))
(:invariant
(lambda (class)
(declare (ignore class))
(format t " ++ Additional invariant (bar)~%")
t)))
) ;; eval-when
(defmethod my-slot :precondition ((bar bar))
(format t " ++ Additional precondition (my-slot bar)~%")
t)
(defmethod my-slot :postcondition ((bar bar))
(format t " ++ Additional postcondition (my-slot bar)~%")
t)
(eval-when (:compile-toplevel :load-toplevel :execute)
(defclass bar-2 (foo)
()
(:invariant (lambda (class)
(declare (ignorable class))
(format t "~& >> Strengthened invariant.~%")
t)))
) ;; eval-when
#| Example:
(let* ((my-foo (make-instance 'foo))
(a-slot (progn (format t " !! Accessing my-slot.~%")
(my-slot my-foo))))
(setf (my-slot my-foo) (progn (format t " !! Setting my-slot.~%")
9999))
(list (my-slot my-foo) a-slot (your-slot my-foo)))
(let* ((my-bar (make-instance 'bar))
(a-slot (progn (format t " !! Accessing my-slot.~%")
(my-slot my-bar))))
(setf (my-slot my-bar) (progn (format t " !! Setting my-slot.~%")
9999))
(list (my-slot my-bar) a-slot (your-slot my-bar)))
(let* ((my-bar-2 (make-instance 'bar-2))
(a-slot (progn (format t " !! Accessing my-slot.~%")
(my-slot my-bar-2))))
(setf (my-slot my-bar-2) (progn (format t " !! Setting my-slot.~%")
9999))
(list (my-slot my-bar-2) a-slot (your-slot my-bar-2)))
(my-slot (make-instance 'bar))
(yet-another-slot (make-instance 'bar))
(my-slot (make-instance 'bar2))
|#
(eval-when (:compile-toplevel :load-toplevel :execute)
(defclass test ()
((my-slot :accessor my-slot :initarg :my-slot :initform 0))
(:invariant (lambda (class)
(numberp (slot-value class 'my-slot)))))
(defclass test-2 (test)
((another-slot :accessor another-slot :initarg :another-slot
:initform nil))
(:invariant (lambda (class)
(< (length (slot-value class 'another-slot))
4))))
);
(defmethod test-dbc :around ((m test) (n test))
(print " >> test-dbc (around)")
(call-next-method))
(defmethod test-dbc ((m test) (n test))
(print " >> test-dbc (test test)")
(list m n))
(defmethod test-dbc :before ((m test) (n test))
(print " >> before (test test)")
(list m n 'before))
(defmethod test-dbc :after ((m test) (n test))
(print " >> after (test test)")
(list m n 'after))
;; Preconditions:
(defmethod test-dbc :precondition ((m test-2) (n test))
(print " >> precondition (test-2 test)")
(< (my-slot m) 123))
(defmethod test-dbc :precondition ((m test) (n test-2))
(print " >> precondition (test test-2)")
(null (another-slot n)))
(defmethod test-dbc :precondition ((m test) (n test))
(print " >> precondition (test test)")
(not (zerop (my-slot m))))
;; Postconditions:
(defmethod test-dbc :postcondition ((m test) (n test-2))
(print " >> postcondition (test test-2)")
(null (another-slot n)))
(defmethod test-dbc :postcondition ((m test) (n test))
(print " >> postcondition (test test)")
(or (zerop (my-slot m)) (zerop (my-slot n))))
#| Examples:
(test-dbc (make-instance 'test :my-slot 1) (make-instance 'test))
;;; Fail (precondition violation)
;;;
(test-dbc (make-instance 'test) (make-instance 'test))
;;; The next call succeeds because the method TEST-DBC has a weakened
;;; precondition for first arguments of type TEST-2.
;;;
(test-dbc (make-instance 'test-2) (make-instance 'test))
;;; Fail (postcondition violation)
;;;
(test-dbc (make-instance 'test :my-slot 1)
(make-instance 'test :my-slot 1))
;;; The weakened postcondition for second argument of class TEST-2
;;; does not cause the method to succeed.
(test-dbc (make-instance 'test :my-slot 1)
(make-instance 'test-2 :my-slot 1))
|#
;;; End of file dbc-test.lisp From: Howard R. Stearns
Subject: Re: DBC in Lisp (was: Stepanov *does* want OOP?)
Date: Mon, 12 Oct 1998 00:00:00 +0000
Message-ID: <3622305E.45F36A50@elwood.com> If someone wants to keep this on the web in some relatively stable
place, we can put a link to it in the ALU tools listing
(http://www.elwood.com/alu/table/tools.htm)
Matthias H�lzl wrote:
>
> [comp.object and comp.eiffel removed since this is no longer relevant]
>
> ······@lavielle.com (Rainer Joswig) writes:
>
> > In article <·················@gauss.muc.de>, ··@gauss.muc.de (Matthias
> > H�lzl) wrote:
> >
> > > style by most authors.) I have appended a simple DBC-library for CLOS
>
> > I have changed it a bit. It now has its own package
> > and uses DEFCLASS.
>
> I have reworked it some more and added a tiny amount of documentation
> so that others might find it more useful. The main improvements are
> that now weakening of preconditions is handled correctly without
> having to manually build the disjunction, furthermore
> pre-/postconditions and invariants can now be defined as predicates
> and an error will be signalled if they evaluate to false.
>
> Matthias
>
> ;;; dbc.lisp
>
> ;;; Design by Contract in Common Lisp.
> ;;; =================================
>
> ;;; One of the outstanding features of the Eiffel language is that it
> ;;; supports a concept called Design by Contract. A comprehensive
> ;;; description is given in
> ;;;
> ;;; Object Oriented Software Construction, 2nd ed.
> ;;; Bertrand Meyer
> ;;; Prentice Hall PTR, 1997
> ;;; ISBN 0-13-629155-4
> ;;;
> ;;; but the key point of DBC is that the relationship between a class
> ;;; and its clients is specified by a contract: There are certain
> ;;; conditions that the caller of a method specialized on a class has
> ;;; to fulfill so that the method can do its job (the preconditions)
> ;;; and the method guarantees certain things after its completion (the
> ;;; postconditions). Furthermore a class may have certain properties
> ;;; that are always true about that class; these properties are called
> ;;; invariants.
> ;;;
> ;;; This file contains an implementation of DBC for CLOS. Pre- and
> ;;; postconditions as well as invariants are specified by qualified
> ;;; methods of type dbc; the usual before, after and around method
> ;;; combinations are available for these methods as well.
> ;;;
> ;;; The code was written by Matthias H�lzl (··@gauss.muc.de) and is
> ;;; placed in the public domain. Rainer Joswig added the package
> ;;; definition and MCL patches. The most recent version of this file
> ;;; should be available at <http://www.muc.de/~hoelzl>.
> ;;;
> ;;; Have fun,
> ;;; Matthias
> ;;;
> ;;;
> ;;; Change Log.
> ;;; ==========
> ;;;
> ;;; 1998-10-07 Matthias H�lzl <··@gauss.muc.de>
> ;;; * Initial version.
> ;;; * Changed handling of pre-/postconditions and invariants to
> ;;; match Eiffel's behavior more closely. Errors are now signalled
> ;;; by the method combination.
> ;;;
> ;;; 1998-10-11 Rainer Joswig
> ;;;
> ;;; * Added package definition.
> ;;; * Added MCL patches.
> ;;;
> ;;; 1998-10-11 Matthias H�lzl <··@gauss.muc.de>
> ;;; * Added default method for `check-invariant'.
> ;;; * Removed `(ensure-generic-function 'check-invariant)' from
> ;;; `define-check-invariant-method'.
> ;;; * Changed method combination type of `check-invariant' to
> ;;; standard method combination.
>
> (cl:defpackage "DESIGN-BY-CONTRACT"
> (:use "COMMON-LISP")
> (:nicknames "DBC")
> (:shadow cl:defclass cl:make-instance)
> (:export "DBC" "DEFCLASS" "MAKE-INSTANCE"))
>
> (in-package "DBC")
>
> ;;; The method combination DBC.
> ;;; ==========================
>
> (define-method-combination dbc ()
> ((precondition (:precondition))
> (around (:around))
> (invariant (:invariant))
> (before (:before))
> (primary () :required t)
> (after (:after))
> (postcondition (:postcondition)))
> (flet ((call-methods (methods)
> (mapcar #'(lambda (method)
> `(call-method ,method))
> methods)))
> (let* ((form (if (or before after (rest primary))
> `(multiple-value-prog1
> (progn ,@(call-methods before)
> (call-method ,(first primary)
> ,(rest primary)))
> ,@(call-methods (reverse after)))
> `(call-method ,(first primary))))
> (around-form (if around
> `(call-method ,(first around)
> (,@(rest around)
> (make-method ,form)))
> form))
> (pre-form (if precondition
> `(if (or ,@(call-methods precondition))
> ,around-form
> (error "Precondition failure."))
> around-form))
> (post-form (if postcondition
> `(multiple-value-prog1
> ,pre-form
> (unless (and ,@(call-methods postcondition))
> (error "Postcondition failure.")))
> pre-form))
> (inv-form (if invariant
> `(multiple-value-prog1
> (progn
> (unless (and ,@(call-methods
> invariant))
> (error
> "Invariant violation before method call."))
> ,post-form)
> (unless (and ,@(call-methods invariant))
> (error
> "Invariant violation after method call.")))
> post-form)))
> inv-form)))
>
> (defun getf-and-remove (name list &optional acc)
> "Find NAME in the alist LIST. Returns nil as first value if NAME is
> not found, the valus associated with NAME otherwise. The second value
> returned is LIST with the first occurence of pair (NAME value)
> removed."
> (if (null list)
> (values nil (reverse acc))
> (if (eql (caar list) name)
> (values (cadar list) (append (reverse acc) (rest list)))
> (getf-and-remove name (rest list) (cons (first list) acc)))))
>
> (defun define-slot-generics (slot)
> "Returns a list with the reader and writer generic functions for a slot.
> The generic functions have method combination type `dbc'."
> (let ((accessor (getf (rest slot) :accessor)))
> (let ((reader (or (getf (rest slot) :reader)
> accessor))
> (writer (or (getf (rest slot) :writer)
> (when accessor
> `(setf ,accessor)))))
> (list (when reader
> `(ensure-generic-function
> ',reader
> :lambda-list '(object)
> :method-combination #-mcl '(dbc:dbc)
> #+mcl (ccl::%find-method-combination nil 'dbc nil)))
> (when writer
> `(ensure-generic-function
> ',writer
> :lambda-list '(new-value object)
> :method-combination #-mcl'(dbc:dbc)
> #+mcl (ccl::%find-method-combination nil 'dbc nil)))))))
>
> (defun define-slot-accessor-invariants (class slot)
> "Returns a list with method definitions for reader and writer
> invariants."
> (let ((accessor (getf (rest slot) :accessor)))
> (let ((reader (or (getf (rest slot) :reader)
> accessor))
> (writer (or (getf (rest slot) :writer)
> (when accessor
> `(setf ,accessor)))))
> (list (when reader
> `(defmethod ,reader :invariant ((object ,class))
> (check-invariant object)))
> (when writer
> `(defmethod ,writer :invariant (value (object ,class))
> (declare (ignore value))
> (check-invariant object)))))))
>
> (defun define-check-invariant-method (invariant class)
> "Returns a list containing the method on CHECK-INVARIANT specialized
> for CLASS and executing INVARIANT."
> `((defmethod check-invariant ((class ,class))
> (when (funcall ,invariant class)
> (call-next-method)))))
>
> (defmacro defclass (&body body)
> (destructuring-bind (name supers &optional slots &rest options)
> body
> (multiple-value-bind (invariant new-options)
> (getf-and-remove :invariant options)
> `(progn
> ,@(if slots
> (apply #'append
> (mapcar (lambda (slot)
> (define-slot-generics slot))
> slots))
> '())
> (cl:defclass ,name ,supers ,slots
> ,@new-options)
> ,@(when invariant
> (define-check-invariant-method invariant name))
> ,@(when slots
> (apply #'append
> (mapcar (lambda (slot)
> (define-slot-accessor-invariants
> name slot))
> slots)))))))
>
> (eval-when (:compile-toplevel :load-toplevel :execute)
> (defgeneric check-invariant (object)
> (:documentation
> "Methods on the generic `check-invariant' are used by the dbc
> method combination to perform the invariant check and should not
> directly be defined by the user."))
> ) ; eval-when
>
> (defmethod check-invariant (object)
> "Default invariant, always true."
> (declare (ignore object))
> t)
>
> (defmethod make-instance (class &rest initargs)
> (let ((class (apply #'cl:make-instance class initargs)))
> (unless (check-invariant class)
> (error "Invariant failure after class creation."))
> class))
>
> ;;; End of file dbc.lisp
>
> ;;; dbc-test.lisp
> ;;;
> ;;; Tests for the dbc package.
>
> (cl:defpackage "DBC-TEST"
> (:use "DBC" "CL")
> (:shadowing-import-from "DBC"
> "DEFCLASS" "MAKE-INSTANCE" "DBC"))
>
> (in-package "DBC-TEST")
>
> (eval-when (:compile-toplevel :load-toplevel :execute)
> (defgeneric test-dbc (arg1 arg2) (:method-combination dbc))
> ) ;; eval-when
>
> (defmethod test-dbc ((m integer) (n integer))
> (print " >> test-dbc (integer integer)")
> (list m n))
>
> (defmethod test-dbc :around ((m integer) (n integer))
> (print " >> test-dbc (around)")
> (call-next-method))
>
> (defmethod test-dbc :precondition ((m fixnum) (n integer))
> (print " >> precondition (fixnum integer)")
> (> m 123))
>
> (defmethod test-dbc :precondition ((m integer) (n fixnum))
> (print " >> precondition (integer fixnum)")
> (< n 100))
>
> (defmethod test-dbc :precondition ((m integer) (n integer))
> (print " >> precondition (integer integer)")
> (= m 12345678900987654321))
>
> (defmethod test-dbc :postcondition ((m integer) (n fixnum))
> (print " >> postcondition (integer fixnum)")
> 999)
>
> (defmethod test-dbc :postcondition ((m integer) (n integer))
> (print " >> postcondition (integer integer)")
> t)
>
> (defmethod test-dbc :invariant ((m integer) (n integer))
> (print " >> invariant (integer integer)")
> 'foo)
>
> (defmethod test-dbc :invariant ((m fixnum) (n integer))
> (print " >> invariant (fixnum integer)")
> 'foo)
>
> (defmethod test-dbc :invariant ((m integer) (n fixnum))
> (print " >> invariant (integer fixnum)")
> 'foo)
>
> (defmethod test-dbc :before ((m integer) (n integer))
> (print " >> before (integer integer)")
> (list (- m 1) (- n 1)))
>
> (defmethod test-dbc :after ((m integer) (n integer))
> (print " >> after (integer integer)")
> (list (+ m 1) (+ n 1)))
>
> #| Example:
>
> (test-dbc 1 2)
> |#
>
> (eval-when (:compile-toplevel :load-toplevel :execute)
> (defclass foo ()
> ((my-slot :accessor my-slot :initform nil)
> (your-slot :accessor your-slot :initform t))
> (:invariant (lambda (class)
> (format t "~& >> Invariant check for class ~A~%"
> class)
> t)))
>
> (defclass bar (foo)
> ((yet-another-slot :accessor yet-another-slot :initform 'yas))
> (:invariant
> (lambda (class)
> (declare (ignore class))
> (format t " ++ Additional invariant (bar)~%")
> t)))
> ) ;; eval-when
>
> (defmethod my-slot :precondition ((bar bar))
> (format t " ++ Additional precondition (my-slot bar)~%")
> t)
>
> (defmethod my-slot :postcondition ((bar bar))
> (format t " ++ Additional postcondition (my-slot bar)~%")
> t)
>
> (eval-when (:compile-toplevel :load-toplevel :execute)
> (defclass bar-2 (foo)
> ()
> (:invariant (lambda (class)
> (declare (ignorable class))
> (format t "~& >> Strengthened invariant.~%")
> t)))
> ) ;; eval-when
>
> #| Example:
>
> (let* ((my-foo (make-instance 'foo))
> (a-slot (progn (format t " !! Accessing my-slot.~%")
> (my-slot my-foo))))
> (setf (my-slot my-foo) (progn (format t " !! Setting my-slot.~%")
> 9999))
> (list (my-slot my-foo) a-slot (your-slot my-foo)))
>
> (let* ((my-bar (make-instance 'bar))
> (a-slot (progn (format t " !! Accessing my-slot.~%")
> (my-slot my-bar))))
> (setf (my-slot my-bar) (progn (format t " !! Setting my-slot.~%")
> 9999))
> (list (my-slot my-bar) a-slot (your-slot my-bar)))
>
> (let* ((my-bar-2 (make-instance 'bar-2))
> (a-slot (progn (format t " !! Accessing my-slot.~%")
> (my-slot my-bar-2))))
> (setf (my-slot my-bar-2) (progn (format t " !! Setting my-slot.~%")
> 9999))
> (list (my-slot my-bar-2) a-slot (your-slot my-bar-2)))
>
> (my-slot (make-instance 'bar))
> (yet-another-slot (make-instance 'bar))
>
> (my-slot (make-instance 'bar2))
>
> |#
>
> (eval-when (:compile-toplevel :load-toplevel :execute)
> (defclass test ()
> ((my-slot :accessor my-slot :initarg :my-slot :initform 0))
> (:invariant (lambda (class)
> (numberp (slot-value class 'my-slot)))))
>
> (defclass test-2 (test)
> ((another-slot :accessor another-slot :initarg :another-slot
> :initform nil))
> (:invariant (lambda (class)
> (< (length (slot-value class 'another-slot))
> 4))))
> );
>
> (defmethod test-dbc :around ((m test) (n test))
> (print " >> test-dbc (around)")
> (call-next-method))
>
> (defmethod test-dbc ((m test) (n test))
> (print " >> test-dbc (test test)")
> (list m n))
>
> (defmethod test-dbc :before ((m test) (n test))
> (print " >> before (test test)")
> (list m n 'before))
>
> (defmethod test-dbc :after ((m test) (n test))
> (print " >> after (test test)")
> (list m n 'after))
>
> ;; Preconditions:
>
> (defmethod test-dbc :precondition ((m test-2) (n test))
> (print " >> precondition (test-2 test)")
> (< (my-slot m) 123))
>
> (defmethod test-dbc :precondition ((m test) (n test-2))
> (print " >> precondition (test test-2)")
> (null (another-slot n)))
>
> (defmethod test-dbc :precondition ((m test) (n test))
> (print " >> precondition (test test)")
> (not (zerop (my-slot m))))
>
> ;; Postconditions:
>
> (defmethod test-dbc :postcondition ((m test) (n test-2))
> (print " >> postcondition (test test-2)")
> (null (another-slot n)))
>
> (defmethod test-dbc :postcondition ((m test) (n test))
> (print " >> postcondition (test test)")
> (or (zerop (my-slot m)) (zerop (my-slot n))))
>
> #| Examples:
>
> (test-dbc (make-instance 'test :my-slot 1) (make-instance 'test))
>
> ;;; Fail (precondition violation)
> ;;;
> (test-dbc (make-instance 'test) (make-instance 'test))
>
> ;;; The next call succeeds because the method TEST-DBC has a weakened
> ;;; precondition for first arguments of type TEST-2.
> ;;;
> (test-dbc (make-instance 'test-2) (make-instance 'test))
>
> ;;; Fail (postcondition violation)
> ;;;
> (test-dbc (make-instance 'test :my-slot 1)
> (make-instance 'test :my-slot 1))
>
> ;;; The weakened postcondition for second argument of class TEST-2
> ;;; does not cause the method to succeed.
>
> (test-dbc (make-instance 'test :my-slot 1)
> (make-instance 'test-2 :my-slot 1))
>
> |#
>
> ;;; End of file dbc-test.lisp From: Matthias H�lzl
Subject: Re: DBC in Lisp (was: Stepanov *does* want OOP?)
Date: Wed, 14 Oct 1998 00:00:00 +0000
Message-ID: <86ww63jnjs.fsf@gauss.muc.de> "Howard R. Stearns" <······@elwood.com> writes about the dbc package:
> If someone wants to keep this on the web in some relatively stable
> place, we can put a link to it in the ALU tools listing
> (http://www.elwood.com/alu/table/tools.htm)
I keep the latest version of the sources at
<http://www.muc.de/~hoelzl/tools/dbc/dbc.lisp>
with a short (and mostly unfinished) intro to DBC at
<http://www.muc.de/~hoelzl/tools/dbc/dbc-intro.html>
These addresses should not go away any time soon. The latest version
is much better than the one I posted to comp.lang.lisp but it is still
quite far from being production code.
Matthias