A nice bug
This is a very nice bug that I stumbled into while running the great auto_test tool on some code I had written. It is a beautiful example of a bug, because it is a very small bug that is still nearly undetectable for the average developer. Also, I do not know about any formal verification tool that could reveal the bug. Finally, it is indeed a specification problem that cannot be expressed in Design by Contract.
I had following deferred class SET with a couple of features defined (I skipped other features, comments and contracts, because they are not relevant for the example):
For the deferred, I had to provide two effective implementations, called SET_A and SET_B. Being lazy, I implemented one of the features and described the other feature in terms of the first.
The first implementation looked like this:
For the second implementation, is_subset_of was actually easier to implement, so I wrote the following code:
Now, the code is broken. If you do not yet see how, think about what happens when I execute the following code:
local sa: SET_A sb: SET_B r: BOOLEAN do create sa create sb r := sa.is_superset_of (sb) end
My question: Who is to blame for the bug? Where exactly does the bug manifest in the code?