Hi,
Le 11/09/2017 à 16:55, Ziqing Luo a écrit :
> But how to let Why3 check the context ?
Let me add a few things about that question.
1) Indeed, Why3 does not offer any *automatic* process to check if the
context is consistent. As said by others before, there is no way for an
automatic prover to guarantee consistency for sure.
2) Yet, there is a first and indeed easy way for being sure of
consistency of your specifications :
*do not use any axioms*
The logic of Why3 is such that if you don't use any axiom, there is a
model. So do not use axioms if you can do without.
The majority of cases where axioms are needed is when one wants to
define a logic function that is not total (e.g division) or one that has
no simple structurally recursive definition. The next major release of
Why3 will provide new ways of defining such functions: logic functions
may be given pre-conditions, and non-structural recursive definitions
will be allowed (generating VCs for proving the termination).
3) Third: in the standard library of Why3, we indeed had to use quite a
lot of axioms. How can we ensure consistency then? Fortunately, there is
still another possibility offered by Why3: writing a model of the
theories using an interactive prover, Coq, Isabelle/HOL or PVS. This is
the process called "realization". If you cannot write your spec without
axioms, but you are strongly concern with consistency, then you should
build realizations. We did that for a majority of the theories of the
standard library. (We should do it for all of them, it is only a matter
of time available...)
Hope this helps,
- Claude
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex |
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
