Commit d4a7ad11 authored by MARCHE Claude's avatar MARCHE Claude

label to suppress the warning on axiom without local abstract symbol

parent 023ff858
(* Knuth's algorithm for prime numbers.
(** {1 Knuth's algorithm for prime numbers}
The Art of Computer Programming, vol 1, page 147.
The following code computes a table of the first m prime numbers.
The following code computes a table of the first [m] prime numbers.
Though there are more efficient ways of computing prime numbers,
the nice thing about this code is that it requires not less than
Bertrand's postulate (for n > 1, there is always a prime p such that
n < p < 2n) to be proved correct.
Bertrand's postulate (for [n > 1], there is always a prime [p] such that
[n < p < 2n]) to be proved correct.
This program had been proved correct using Coq and an early version of
Why back in 2003, by Laurent Théry (INRIA Sophia-Antipolis).
Laurent Théry.
Proving Pearl: Knuth's Algorithm for Prime Numbers.
TPHOLs 2003
Why back in 2003, by Laurent Théry (INRIA Sophia-Antipolis): Laurent Théry,
Proving Pearl: Knuth's Algorithm for Prime Numbers, TPHOLs 2003
Truly a tour de force, this proof includes the full proof of Bertrand's
postulate in Coq. Here, we simply focus on the program verification part,
posing Bertrand's postulate as a lemma that we do not prove.
Note: Knuth's code is entering the loop where a new prime number is
added, thus resulting into the immediate addition of 3 as prime[1].
It allows subsequent division tests to start at prime[1]=3, thus
saving the division by prime[0]=2. We did something similar in the
added, thus resulting into the immediate addition of 3 as [prime[1]].
It allows subsequent division tests to start at [prime[1]=3], thus
saving the division by [prime[0]=2]. We did something similar in the
code below, though the use of a while loop looks like we did a
special case for 3 as well. *)
......@@ -40,7 +38,7 @@ module PrimeNumbers
predicate no_prime_in (l u: int) =
forall x: int. l < x < u -> not (prime x)
(* p[0]...p[u-1] are the first u prime numbers *)
(** [p[0]..p[u-1]] are the first u prime numbers *)
predicate first_primes (p: array int) (u: int) =
p[0] = 2 /\
(* sorted *)
......@@ -55,11 +53,13 @@ module PrimeNumbers
forall d: int. 2 <= d <= p[u-1] -> prime d ->
exists i: int. 0 <= i < u /\ d = p[i]
lemma Bertrand_postulate:
(** Bertrand's postulate, admitted as an axiom
(the label is there to suppress the warning issued by Why3) *)
axiom Bertrand_postulate "W:conservative_extension:N" :
forall p: int. prime p -> not (no_prime_in p (2*p))
(* returns an array containing the first m prime numbers *)
(** [prime_numbers m] returns an array containing the first [m]
prime numbers *)
let prime_numbers (m: int)
requires { m >= 2 }
ensures { result.length = m }
......
......@@ -443,6 +443,8 @@ let warn_dubious_axiom uc k p syms =
p.id_string
with Exit -> ()
let lab_w_conservative_extension_no = Ident.create_label "W:conservative_extension:N"
let add_decl ?(warn=true) uc d =
check_decl_opacity d; (* we don't care about tasks *)
let uc = add_tdecl uc (create_decl d) in
......@@ -453,7 +455,9 @@ let add_decl ?(warn=true) uc d =
| Dlogic dl -> List.fold_left add_logic uc dl
| Dind (_, dl) -> List.fold_left add_ind uc dl
| Dprop ((k,pr,_) as p) ->
if warn then warn_dubious_axiom uc k pr.pr_name d.d_syms;
if warn &&
not (Slab.mem lab_w_conservative_extension_no pr.pr_name.id_label)
then warn_dubious_axiom uc k pr.pr_name d.d_syms;
add_prop uc p
(** Declaration constructors + add_decl *)
......
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