In article <············@glitnir.ifi.uio.no>, ······@ifi.uio.no (Lars
Marius Garshol) wrote:
> ········@MCI2000.com wrote:
> >
> >Assertions allow the programmer to test for the correctness of the
> >software, as well as provide an actual *specification* or documentation of
> >what the software does through the use of such assertions. I am not aware
> >of any other language which provides a similar facility.
>
> Euclid does.
Common Lisp combines ASSERT with exception handling.
So your program can actually handle assertion failures.
Description Logics like Classic from AT&T makes it possible to detect
inconsistencies using a purely declarative approach.
Example:
(classic:cl-startup)
; relation has-child
(classic:cl-define-primitive-role 'has-child :attribute t)
; a person class
(classic:cl-define-disjoint-primitive-concept
'person 'classic:classic-thing 'stuff-type)
; a person can either be a woman or...
(classic:cl-define-disjoint-primitive-concept
'woman 'person 'person-type)
; ... a man
(classic:cl-define-disjoint-primitive-concept
'man 'person 'person-type)
; a mother has atleast one child. all children are persons.
(classic:cl-define-primitive-concept
'mother '(and woman
(at-least 1 has-child)
(all has-child person)))
; try to define a new subclass inheriting from mother and man
(classic:cl-define-primitive-concept
'does-not-work
'(and man mother))
This generates following error:
*WARNING*: Disjoint primitives: @tc{MAN}, @tc{WOMAN}.
*CLASSIC ERROR* while processing
(CLASSIC:CL-DEFINE-PRIMITIVE-CONCEPT DOES-NOT-WORK (AND MAN MOTHER))
occurred on object @c{DOES-NOT-WORK-*INCOHERENT*}:
Trying to combine disjoint primitives: @tc{MAN} and @tc{WOMAN}.
; try to define a class of mother with no children
(classic:cl-define-primitive-concept
'does-not-work2
'(and mother
(at-most 0 has-child)))
This generates following error:
*WARNING*: Inconsistent number restriction for role @r{HAS-CHILD} - at-least:
1; at-most: 0. Found along role-path (@r{HAS-CHILD}), while processing object
@tc{DOES-NOT-WORK2}.
*CLASSIC ERROR* while processing
(CLASSIC:CL-DEFINE-PRIMITIVE-CONCEPT DOES-NOT-WORK2 (AND MOTHER (AT-MOST 0
HAS-CHILD)))
occurred on object @c{DOES-NOT-WORK2-*INCOHERENT*}
along role-path (@r{HAS-CHILD}):
Inconsistent number restriction for role @r{HAS-CHILD} - at-least: 1;
at-most: 0.
Systems like Classic can find errors in inconsistent
concept (-> class) descriptions at compile time.
They also can check similar things about assertions
objects at runtime.
; define a class ship, which is disjoint with the above defined
; class person
(classic:cl-define-disjoint-primitive-concept
'ship
'classic:classic-thing
'stuff-type)
; an object of type ship
(classic:cl-create-ind 'titanic 'ship)
; an object of type mother which has titanic as a child
(classic:cl-create-ind 'kathy
'(and mother
(fills has-child titanic)))
This naturally generates an error:
*WARNING*: Disjoint primitives: @tc{SHIP}, @tc{PERSON}.
*WARNING*: Creation of individual KATHY failed.
*CLASSIC ERROR* while processing
(CLASSIC:CL-CREATE-IND KATHY (AND MOTHER (FILLS HAS-CHILD TITANIC)))
occurred on object @i{TITANIC-*INCOHERENT*}:
Trying to combine disjoint primitives: @tc{SHIP} and @tc{PERSON}.
And some guys keep telling us Lisp is not capable enough for large
systems design due to lack of strong typing. Sigh.
--
http://www.lavielle.com/~joswig/