View source for Side-effect sensitive invariant checking

← Side-effect sensitive invariant checking

You do not have permission to edit this page, for the following reasons:

The action you have requested is limited to users in one of the groups: Autoconfirmed users, emailconfirmed, editors.
You must confirm your email address before editing pages. Please set and validate your email address through your user preferences.

You can view and copy the source of this page:

Author: Matthias Konrad

{{Warning|'''Warning''': Article in development and will most probably be skipped}}


[[Category:Assertion checking]]

Invariants are a very powerfull 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):

{|border="0" cellpadding="2" cellspacing="0" align="center"
|-valign="top" -halign="center"
|<code>[eiffel, N]
class A
create
   make
feature
   make 
      do 
         create {LINKED_LIST [ANY]}l.make 
      end
   
   l: LIST [ANY]
invariant
   l.count = 0
end
</code>
|
<code>[eiffel, N]
class
   B
feature
   f
      local
         a: A
      do
         create a.make
         a.l.put ("hello")
         a.l.put ("hello")
      end
end
</code>
|}

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 violatioins are detected is not the real problem, since most are. Invariant violation are often detected to 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.

Template used on this page:

Template:Warning (view source)

Return to Side-effect sensitive invariant checking.

Retrieved from "https://dev.eiffel.com/Side-effect_sensitive_invariant_checking"

View source for Side-effect sensitive invariant checking

Navigation

Development

Wiki

Search

Tools