Commit 1d94aac3 authored by MARCHE Claude's avatar MARCHE Claude

demo updated

parent e55d8f29
......@@ -59,7 +59,11 @@ let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers gconfig.config
let cont =
Session_user_interface.cont_from_files spec usage_str gconfig.env files provers
try
Session_user_interface.cont_from_files spec usage_str gconfig.env files provers
with e ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let () =
Debug.dprintf debug "[GUI] Init the GTK interface...@?";
......
......@@ -9,17 +9,11 @@ module Power
axiom power_s : forall x n:int. n >= 0 ->
power x (n+1) = x * power x n
(* turn the following lemma into a lemma function : *)
lemma power_1 : forall x:int. power x 1 = x
(* idem *)
lemma sqrt4_256 : exists x:int. power x 4 = 256
(* idem *)
lemma power_sum : forall x n m: int.
lemma power_sum : forall x n m: int.
0 <= n /\ 0 <= m ->
power x (n+m) = power x n * power x m
......@@ -27,22 +21,19 @@ module Power
lemma power_0_left : forall n. n >= 1 -> power 0 n = 0
(*
lemma power_3 : forall x. x >= 1 ->
power (x-1) 3 = power x 3 - 3 * x * x + 3 * x - 1
*)
let rec ghost little_fermat_3 (x : int) : int
requires { x >= 0 }
variant { x }
ensures { power x 3 - x = 3 * result }
= if x = 0 then 0
else let r = little_fermat_3 (x-1) in
r + x * x - x
lemma little_fermat_3 :
forall x : int. x >= 0 -> exists y : int. power x 3 - x = 3 * y
end
(*
Local Variables:
compile-command: "why3 ide lemma_functions.mlw"
compile-command: "why3 ide demo-itp.mlw"
End:
*)
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