Difference between revisions of "Side-effect sensitive invariant checking"
m |
Peter gummer (Talk | contribs) m |
||
Line 6: | Line 6: | ||
[[Category:Assertion checking]] | [[Category:Assertion checking]] | ||
− | Invariants are a very | + | 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== | ==Definition invariant violation== | ||
Line 47: | Line 47: | ||
|} | |} | ||
− | 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 | + | 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 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== | ==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. | SESIC goes one step further. It not only aims to detect all possible invariant violations, it detects them right when they occur. |
Revision as of 16:51, 12 March 2007
Author: Matthias Konrad
Warning: 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 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.