Opened 16 years ago
Closed 16 years ago
#151 closed defect (fixed)
Fib example gets wrong answer
| Reported by: | Stephen Siegel | Owned by: | ywei |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | verify | Version: | 1.0 |
| Keywords: | loop fib co-invariant | Cc: |
Description
The Fibonacci example has a "bad" implementation which is not functionally equivalent to the spec, but the loop method comparator says it is functionally equivalent.
The problem seems to occur at State 20, where the Enabler seems to say there are no outgoing transitions, even though there are.
What is supposed to happen is that when the spec hits the branch "if (tmp>=p)" it must explore both the true and false branches. When it explores the false branch it sets err=p-tmp then continues until it gets back to location l. Then the impl proceeds and gets to its location l. Then we check that the co-invariant holds, but it should not hold, because it will not be true that err==spec.err (they are off by a minus sign).
Change History (2)
comment:1 by , 16 years ago
| Status: | new → accepted |
|---|
comment:2 by , 16 years ago
| Resolution: | → fixed |
|---|---|
| Status: | accepted → closed |
Bug fixed. The enabler can generate correct transitions now.