From 1025f2f68f8c083a8c5a6ca0525d6777f10e13b8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 1 Dec 2023 16:52:24 +0100
Subject: [PATCH] [wp] no more axiom in Qed Why3 theory
---
src/plugins/wp/share/why3/frama_c_wp/qed.mlw | 24 +++++++-------------
1 file changed, 8 insertions(+), 16 deletions(-)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
index 1404e517aad..4b428b179ee 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
@@ -31,23 +31,14 @@ theory Qed
(** The definitions are in comment because its not useful for coq
(no if-then-else on formula) and not tested on automatic provers *)
- function eqb (x y : 'a) : bool (*= if x = y then True else False*)
- axiom eqb : forall x:'a, y:'a. eqb x y = True <-> x = y
+ function eqb (x y : 'a) : bool = if x = y then True else False
+ function neqb (x y : 'a) : bool = if x <> y then True else False
- function neqb (x y : 'a) : bool(* = if x <> y then True else False*)
- axiom neqb : forall x:'a, y:'a. neqb x y = True <-> x <> y
+ function zlt (x y : int) : bool = if x < y then True else False
+ function zleq (x y : int) : bool = if x <= y then True else False
- function zlt (x y : int) : bool(* = if x < y then True else False*)
- function zleq (x y : int) : bool(* = if x <= y then True else False*)
-
- axiom zlt : forall x:int, y:int. zlt x y = True <-> x < y
- axiom zleq : forall x:int, y:int. zleq x y = True <-> x <= y
-
- function rlt (x y : real) : bool(* = if x <. y then True else False*)
- function rleq (x y : real) : bool(* = if x <=. y then True else False*)
-
- axiom rlt : forall x:real, y:real. rlt x y = True <-> x <. y
- axiom rleq : forall x:real, y:real. rleq x y = True <-> x <=. y
+ function rlt (x y : real) : bool = if x <. y then True else False
+ function rleq (x y : real) : bool = if x <=. y then True else False
function real_of_int (x:int) : real = FromInt.from_int x
meta "inline:no" function real_of_int
@@ -68,5 +59,6 @@ theory Qed
forall a,b,n:int.
0 <= a -> 0 <= b -> 0 <= b-a < n ->
CD.mod a n = CD.mod b n -> a = b
-
+ by b - a = n * (CD.div (b - a) n) + CD.mod (b - a) n
+ so (CD.div b n) - (CD.div a n) = CD.div (b - a) n
end
--
GitLab