Menu
▾
▴
#213 False invariant not caught b provers
Hello:
Attached is a model based on this paper:
http://deploy-eprints.ecs.soton.ac.uk/22/
In machine FMCH00, invariant 102 is:
svr_root ∈ svr_objects ∧ svr_root ∉ svr_objects
It evaluates to true in INITIALIZATION/INV102 (when it
shouldn't) in Rodin 0.8.2 with all provers (including
B4Free) moved to the used (right) list in the
Auto-Tactic and Post-Tactic configuration screens.
The attached model has been cut down to a more manageable
size and archived from within Rodin. (FMCH00.bpr had to
be excluded, as it was to large to be uploaded.)
If you have any questions, I can be contacted at:
david.kelk@gmail.com
Thank you,
David.
Rodin project showing prover bug
Logged In: YES
user_id=1041912
Originator: NO
David,
thank you very much for taking the time for reporting this bug, especially as it seems an important issue.
However, your false invariant is indeed discharged by the ML theorem prover because there is a contradiction in the axioms of context FCTX, where you've written:
axm3 : objrel = OBJECT ↔ OBJECT
axm103 : svr_objrel = OBJECT ↔ OBJECT
axm104 : svr_tcl ∈ svr_objrel → svr_objrel ∧ svr_tcl ∉ objrel → objrel
The last axiom thus states that svr_tcl is both in and not in the same set.
We know that this problem of contradiction in axioms is currently very difficult to detect. Our plans in the Deploy project is to provide means for instantiating a context, thus providing a model of it. This will allow users to ensure that axioms are not contradictory, if the provided model is simple enough.
Laurent.