Commit b571760d authored by Mario Pereira's avatar Mario Pereira
parents 2d0eb69b 76c67c9c
......@@ -1032,7 +1032,7 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
$(SHOW) 'Coqdep $<'
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
all: $(COQVO) drivers/coq-realizations.aux
all: $(COQVO)
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
......@@ -1055,6 +1055,8 @@ drivers/coq-realizations.aux: Makefile
endif
all: drivers/coq-realizations.aux
install_no_local::
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
......
......@@ -216,7 +216,8 @@ The provers can give the following output:
\label{sec:proveoptions}
\begin{description}
\item[\texttt{-{}-get-ce}] activates the generation of a potential counter-example when a proof does not succeed (experimental).
\item[\texttt{-{}-get-ce}] activates the generation of a potential
counter-example when a proof does not succeed (experimental).
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}] specifies
\textsl{s} as an additional prefix for labels that denotes VC
explanations. The option can be used several times to specify
......@@ -470,7 +471,125 @@ are grouped together under several tabs.
decision by clicking on it.
\end{description}
% \subsection{Displaying Counterexamples}
\subsection{Displaying Counterexamples}
When the selected prover finds (counterexample) model, it is possible to
display parts of this model in the terms of the original Why3 input.
Currently, this is supported for CVC4 prover version 1.5 and newer.
To display the counterexample in Why3 IDE, the counterexample model generation
must be enabled in File -/> Preferences -/> get
counter-example.
After running the prover and clicking on the prover result in, the
counterexample can be displayed in the tab
Counter-example.
The counterexample is displayed with the original Why3 code in comments.
Counterexample values for Why3 source code elements at given line are
displayed in a comment at the line below.
An alternative way how to display a counterexample is to use the option
\texttt{-{}-get-ce} of the \texttt{prove} command.
Why3 source code elemets that should be a part of counterexample must be
explicitly marked with \texttt{"model"} label. The following example shows a
Why3 theory with some terms annotated with the \texttt{model} label and the
generated counterexample in comments:
\begin{whycode}
theory T
use import int.Int
goal g_no_lab_ex : forall x:int. x >= 42 -> x + 3 <= 50
goal g_lab_ex : forall x "model":int. ("model" x >= 42) ->
("model" "model_trace:x+3<=50" x + 3 <= 50)
goal computation_ex : forall x1 "model" x2 "model" x3 "model" .
(* x1 = 1; x2 = 1; x3 = 1 *)
("model" "model_trace: x1 + 1 = 2" x1 + 1 = 2) ->
(* x1 + 1 = 2 = true *)
("model" x2 + 1 = 2) ->
(* (= (+ x2 1) 2) = true *)
("model" x3 + 1 = 2) ->
(* (= (+ x3 1) 2) = true *)
("model" x1 + x2 + x3 = 5)
(* (= (+ (+ x1 x2) x3) 5) = false *)
\end{whycode}
To display counterexample values in assertions the term being asserted must be
labeled with the label \texttt{"model\_vc"}. To display counterexample values
in postconditions, the term in the postcondition must be labeled with the
label \texttt{"model\_vc\_post"}.
The following example shows a counterexample of a function with postcondition:
\begin{whycode}
let incr_ex ( x "model" : ref int ) (y "model" : ref int): unit
(* x = -2; y = -2 *)
ensures { !x = old !x + 2 + !y }
=
y := !y + 1;
(* y = -1 *)
x := !x + 1;
(* x = -1 *)
x := !x + 1
(* x = 0 *)
\end{whycode}
It is also possible to rename counterexample elements using the lable
\texttt{"model\_trace:"}. The following example shows the use of renaming a
counterexample element in order to print the counterexample in infix notation
instead of default prefix notation:
\begin{whycode}
goal g_lab_ex : forall x "model":int. ("model" x >= 42) ->
(* x = 48; (<= 42 x) = true *)
("model" "model_trace:x+3<=50" x + 3 <= 50)
(* x+3<=50 = false *)
\end{whycode}
Renaming counterexample elements is in particular useful when Why3 is used as
intermediate language and to show names of counterexample elements in the
source language instead of showing names of Why3 elements.
Note that if the counterexample element is of a record type, it is also
possible to rename names of the record fields by putting the label
\texttt{model\_trace:} to definitions of record fields. For example:
\begin{whycode}
type r = {f "model_trace:.F" :int; g "model_trace:G" :bool}
\end{whycode}
When a prover is queried for a counterexample value of a term of an abstract
type=, an internal representation of the value is get. To get the concrete
representation, the term must be marked with the label
\texttt{"model\_projected"} and a projection function from the abstract type
to a concrete type must be defined, marked as a projection using the meta
\texttt{"model\_projection"}, and inlining of this function must be disabled
using the meta \texttt{"inline : no"}. The following example shows a
counterexample of an abstract value:
\begin{whycode}
theory A
use import int.Int
type byte
function to_rep byte : int
predicate in_range (x : int) = -128 <= x <= 127
axiom range_axiom : forall x:byte.
in_range (to_rep x)
meta "model_projection" function to_rep
meta "inline : no" function to_rep
goal abstr : forall x "model_projected" :byte. to_rep x >= 42 -> to_rep x
+ 3 <= 50
(* x = 48 *)
\end{whycode}
More examples of using counterexample feature of Why3 can be found in the file
examples/tests/cvc4-models.mlw and examples/tests/cvc4-models.mlw.
More information how counterexamples in Why3 works can be found
in~\cite{sefm16}.
%
% how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
%
......
......@@ -232,3 +232,21 @@ Claude March\'e and Andrei Paskevich},
year = {2007}
}
@inproceedings{sefm16,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
booktitle = {Proceedings of the 8th Conference on Real Numbers and
Computers},
address = {Santiago de Compostela, Spain},
year = {2008},
pages = {93--102},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC},
topics = {team},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
}
\ No newline at end of file
......@@ -158,7 +158,7 @@ let print_prover_status fmt = function
| Unix.WEXITED n -> fprintf fmt "exited with status %d" n
let print_steps fmt s =
if s >= 0 then fprintf fmt ", %d steps)" s
if s >= 0 then fprintf fmt ", %d steps" s
let print_prover_result fmt {pr_answer = ans; pr_status = status;
pr_output = out; pr_time = t;
......
......@@ -45,16 +45,13 @@ let meta_projection = Theory.register_meta "model_projection" [Theory.MTlsymbol]
let intro_const_equal_to_term
~term
~const_label
~const_loc
~const_name
~id_new
~axiom_name
=
(* See documentation of the function in file intro_projections_counterexmp.mli. *)
(* Create declaration of new constant *)
(*let lab_new = Slab.add model_label labels in*)
let id_new = Ident.id_user ~label:const_label const_name const_loc in
let ls_new_constant = Term.create_lsymbol id_new [] term.t_ty in
let decl_new_constant = Decl.create_param_decl ls_new_constant in
let t_new_constant = Term.t_app ls_new_constant [] term.t_ty in
......@@ -98,7 +95,8 @@ let intro_proj_for_ls env map_projs ls_projected =
let const_loc = Opt.get ls_projected.ls_name.id_loc in
let const_name = ls_projected.ls_name.id_string^"_proj_constant_"^proj_name in
let axiom_name = ls_projected.ls_name.id_string^"_proj_axiom_"^proj_name in
intro_const_equal_to_term ~term:t_rhs ~const_label ~const_loc ~const_name ~axiom_name in
let id_new = Ident.id_user ~label:const_label const_name const_loc in
intro_const_equal_to_term ~term:t_rhs ~id_new:id_new ~axiom_name in
let rec projections_for_term term proj_name applied_projs map_projs =
(* Return declarations for projections of the term.
......
......@@ -55,18 +55,14 @@ val intro_projections_counterexmp : Env.env -> Task.task Trans.trans
val intro_const_equal_to_term :
term : Term.term ->
const_label : Ident.Slab.t ->
const_loc : Loc.position ->
const_name : string ->
id_new : Ident.preid ->
axiom_name : string ->
Decl.decl list
(** Creates declaration of new constant and declaration of axiom
stating that the constant is equal to given term.
@param term the term to which the new constant will be equal
@param const_label the label of the constant
@param const_loc the location of the constant
@param const_name the name of the constant
@param id_new the preid composed of the name, label and loc of the constant
@param axiom_name the name of the axiom about the constant
@return the definition of the constant and axiom about the constant
*)
This diff is collapsed.
......@@ -20,14 +20,9 @@ open Ty
open Term
open Decl
(* This label is used to stop the introduction transformation to introduce
variables past it. It is generated by software that uses why3 as a backend
such as SPARK (for counterexamples) *)
let stop_intro = Ident.create_label "stop_intro"
let rec intros pr f =
if Slab.mem stop_intro f.t_label then [create_prop_decl Pgoal pr f] else
match f.t_node with
(* (f2 \/ True) => _ *)
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },_)
when Slab.mem Term.asym_label f2.t_label ->
[create_prop_decl Pgoal pr f]
......
......@@ -32,11 +32,8 @@ let prepare_for_counterexmp2 env task =
(* Counter-example will be queried, prepare the task *)
Debug.dprintf debug "Get ce@.";
let comp_trans = Trans.compose
(Trans.goal Introduction.intros)
(Trans.compose
Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp
(Intro_projections_counterexmp.intro_projections_counterexmp env)
)
in
(Trans.apply comp_trans) task
end
......
......@@ -45,6 +45,8 @@ type value =
| Vcase of value * term_branch list
let array_cons_ls = ref ps_equ
let ls_true = ref ps_equ
let ls_false = ref ps_equ
let rec print_value fmt v =
match v with
......@@ -228,6 +230,9 @@ let rec matching env (t:value) p =
else
if ls2.ls_constr > 0 then raise NoMatch
else raise Undetermined
| Vbool b ->
let l = if b then !ls_true else !ls_false in
if ls_equal ls1 l then env else raise NoMatch
| _ -> raise Undetermined
......@@ -407,8 +412,8 @@ let eval_map_set ls_set l =
let built_in_theories =
[ ["bool"],"Bool", [],
[ "True", None, eval_true ;
"False", None, eval_false ;
[ "True", Some ls_true, eval_true ;
"False", Some ls_false, eval_false ;
] ;
["int"],"Int", [],
[ "infix +", None, eval_int_op BigInt.add;
......
......@@ -798,7 +798,7 @@ module Print = struct
print_lident info fmt ts
| Tapp (ts, [ty]) ->
fprintf fmt (protect_on paren "%a@ %a")
(print_ty info) ty (print_lident info) ts
(print_ty ~paren:true info) ty (print_lident info) ts
| Tapp (ts, tl) ->
fprintf fmt (protect_on paren "(%a)@ %a")
(print_list comma (print_ty info)) tl
......@@ -969,7 +969,7 @@ module Print = struct
fprintf fmt "%a.%a" (print_expr_p info) e (print_lident info) f
| Esetfield (e1, f, e2) ->
fprintf fmt (protect_on paren "%a.%a <- %a")
(print_expr info) e1 (print_lident info) f (print_expr info) e2
(print_expr_p info) e1 (print_lident info) f (print_expr info) e2
| Eblock [] ->
fprintf fmt "()"
| Eblock [e] ->
......@@ -1005,7 +1005,7 @@ module Print = struct
fprintf fmt (protect_on paren "raise %a") (print_uident info) id
| Eraise (Xident id, Some e1) ->
fprintf fmt (protect_on paren "raise (%a %a)")
(print_uident info) id (print_expr info) e1
(print_uident info) id (print_expr ~paren:true info) e1
| Etry (e1, bl) ->
fprintf fmt
"@[<v>@[<hv>@[<hov 2>begin@ try@ %a@]@ with@]@\n@[<hov>%a@]@\nend@]"
......@@ -1069,7 +1069,7 @@ module Print = struct
fprintf fmt "exception %a@\n@\n" (print_uident info) xs
| Dexn (xs, Some ty) ->
fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
(print_uident info) xs (print_ty info) ty
(print_uident info) xs (print_ty ~paren:true info) ty
end
......
......@@ -426,15 +426,15 @@ theory GenFloatSpecFull
/\
(is_infinite x /\ is_finite y -> is_infinite r /\ same_sign r x)
/\
(is_infinite x /\ is_infinite y /\ same_sign x y
-> is_infinite r /\ same_sign r x)
/\
(is_infinite x /\ is_infinite y /\ diff_sign x y -> is_NaN r)
(is_infinite x /\ is_infinite y ->
if same_sign x y then is_infinite r /\ same_sign r x
else is_NaN r)
/\
(is_finite x /\ is_finite y /\ no_overflow m (value x + value y)
-> is_finite r /\
value r = round m (value x + value y) /\
sign_zero_result m r)
(if same_sign x y then same_sign r x
else sign_zero_result m r))
/\
(is_finite x /\ is_finite y /\ not no_overflow m (value x + value y)
-> SpecialValues.same_sign_real (sign r) (value x + value y)
......@@ -449,15 +449,15 @@ theory GenFloatSpecFull
/\
(is_infinite x /\ is_finite y -> is_infinite r /\ same_sign r x)
/\
(is_infinite x /\ is_infinite y /\ same_sign x y -> is_NaN r)
/\
(is_infinite x /\ is_infinite y /\ diff_sign x y
-> is_infinite r /\ same_sign r x)
(is_infinite x /\ is_infinite y ->
if diff_sign x y then is_infinite r /\ same_sign r x
else is_NaN r)
/\
(is_finite x /\ is_finite y /\ no_overflow m (value x - value y)
-> is_finite r /\
value r = round m (value x - value y) /\
sign_zero_result m r)
(if diff_sign x y then same_sign r x
else sign_zero_result m r))
/\
(is_finite x /\ is_finite y /\ not no_overflow m (value x - value y)
-> SpecialValues.same_sign_real (sign r) (value x - value y)
......@@ -509,8 +509,8 @@ theory GenFloatSpecFull
-> is_infinite r)
/\(is_gen_zero x /\ is_gen_zero y -> is_NaN r)
/\ product_sign r x y
/\ exact r = exact x /exact y
/\ model r = model x /model y
/\ exact r = exact x / exact y
/\ model r = model x / model y
predicate of_real_exact_post (x:real) (r:t) =
is_finite r /\ value r = x /\ exact r = x /\ model r = x
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment