Eiffel-like Invariants

I've been thinking about Eiffel lately and how useful class invariants were. In Eiffel, an invariant clause sets conditions that must remain true throughout the lifetime of an object. These conditions (assertions really) are bound to instance variables.

Playing around with Tcl, we can come up with a useful(?) fascimile (*hack*) in just a few lines of code:

 proc invariant {var {expression ""} {msg "Illegal value"}} {
    uplevel trace add variable $var write \[list invariant_check \{$expression\} \{$msg\}]
 
 }

 proc invariant_check {expression msg v1 v2 mode} {
    if {$expression == ""} {
        error "Cannot modify!"
    }
    if {![uplevel expr \{$expression\}]} {
        error $msg
    }
 }

This could be very useful for Itcl (contrived example alert!):

 package require Itcl

 itcl::class Person {
    variable age
    variable sex
    public variable full_name

    constructor {name i_age i_sex} {set full_name $name} {
        invariant age {$age >= 0 && $age < 120} {Must be between 0 and 120.}
        invariant sex {$sex == "M" || $sex == "F"} {Must be M or F.}
        invariant full_name ;# Can never be changed!!

        set age $i_age
        set sex $i_sex
    }

    method set_age {years} {
        set age $years
    }

    method change_sex {mf} {
        set sex $mf
    }
 }

So that,

 Person bob "Bobby Tester" 5 M
 bob change_sex Female ; # this will raise an error
 bob set_age 134 ; # this will raise an error
 bob configure -name "Sue" ; # this will raise an error

The errors are quite useful too (for example):

 can't set "sex": Must be M or F.
    while executing
 "set sex $mf"
    (object "::bob" method "::Person::change_sex" body line 2)
    invoked from within
 "bob change_sex Female"
  ...

Note that the 3 invariants hold across all methods in this class. The real usefulness would be in deeply complex classes where you could not guarentee that an instance variable maintains correctness through usage in derived classes.

The major difference between my hack and Eiffel is that in Eiffel the variable can break the invariant clause temporarily. The clause is only checked at the end of a method's invocation. (Which we could hack here too in Tcl -- left as a later exercise).

Of course, for those who don't use Itcl, this all works in plain old Tcl too...

-- Todd Coram

XOTcl offers built-in invariants and assertions (pre- and postassertions). Here some samples taken from XOTcl Tutorial.

 ClassName instinvar invariantList

 objName invar invariantList

And Assertions

  Class Sensor -parameter {{value 1}}
  Sensor instinvar {
    {[regexp {^[0-9]$} [my value]] == 1}
  }
  Sensor instproc incrValue {} {
    my incr value
  } {
    {# pre-condition:} 
    {[my value] > 0}
  } {
    {# post-condition:} 
    {[my value] > 1}
  }

The example above could see in XOTcl as follow

 Class Person -parameter {age sex fullName}
 Person instinvar {{[my age]>=0 && [my age]< 120} {[my sex]=="M" || [my sex]=="F"}}

 Person create myPerson -fullName {Bobby Tester} -age 5 -sex M
 myPerson check all

 myPerson age 5

XOTcl allow also to set the checking temporary off (with check command) and also to set object and class checking. (In XOTcl classes are also objects).

There is a small semantic difference to ITcl code. In this the invariants do not prevent setting of wrong values. The invariants are checked before and after every method call but not permanent by using variable traces. It means every method are understood as small transaction on object. In this trasactions in invariats can be idle. Invariants must be also checked only after method calls. I am not very sure what kind of insertions are more practicable.

Artur Trzewik, Category XOTcl Code

See also Constants - Constraining variables