Difference between revisions of "Side-effect sensitive invariant checking"

Latest revision as of 01:19, 11 April 2007

Author: Matthias Konrad

Warning: Article in development and will most probably be skipped

Invariants are a very powerful technique for giving meaning to programs. They reveal mission critical information about the behaviour of an object. When invariants are violated something in the system went (terribly) wrong.

Definition invariant violation

Status quo of invariant detection

At first thought it seems to be sufficient to check the invariants of an object at the end of every feature call that was initiated through a qualified call. Exactly as it is done with postcondition checks. Unfortunately, such a scheme would not detect invariants that contain side effects. The invariant of the following class A depends on an object that may be modified (through aliasing) by other classes (in the example this is done by class B):

class A
create
   make
feature
   make 
      do 
         create {LINKED_LIST [ANY]}l.make 
      end
 
   l: LIST [ANY]
invariant
   l.count = 0
end

class
   B
feature
   f
      local
         a: A
      do
         create a.make
         a.l.put ("hello")
         a.l.put ("hello")
      end
end

Out of this reason, EiffelStudio tests invariants not only on feature exit but also on feature entrance. The invariant violation in the above example would still not be detected. In practice the fact that not all the violations are detected is not the real problem, since most are. Invariant violation are often detected too late. It is not only important to detect an invariant violation but also to know who (by which I mean which line of code) is to blame for it.

Side-effect sensitive invariant checking SESIC

SESIC goes one step further. It not only aims to detect all possible invariant violations, it detects them right when they occur.