Difference between revisions of "Side-effect sensitive invariant checking"
m |
|||
| (6 intermediate revisions by 3 users not shown) | |||
| Line 1: | Line 1: | ||
| − | Invariants are a very | + | Author: Matthias Konrad |
| + | |||
| + | {{Warning|Article in development and will most probably be skipped}} | ||
| + | |||
| + | |||
| + | [[Category:Assertion checking]] | ||
| + | |||
| + | 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 33: | Line 40: | ||
do | do | ||
create a.make | create a.make | ||
| + | a.l.put ("hello") | ||
a.l.put ("hello") | a.l.put ("hello") | ||
end | end | ||
| Line 39: | 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 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== | ==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. | ||
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.
