Commit ba8bd4b5 authored by Andrei Paskevich's avatar Andrei Paskevich

remove trailing whitespace, tabs, and latin1 characters

parent 37f06a22
......@@ -50,7 +50,9 @@
* choisir un logo
=== Roadmap for third release ==========================================
=== Roadmap for third release 0.70 =======================================
* increment the magic number in config (A)
* enlever les caracteres de tab des sources
et les caracteres latin1 (A)
......
......@@ -2,7 +2,7 @@ module M
use import module ref.Ref
let foo (x : ref int) (y : ref int) =
let foo (x : ref int) (y : ref int) =
x := 1;
y := 2
......
......@@ -2,7 +2,7 @@ module M
use import module ref.Ref
let foo (x : ref int) (y : ref int) =
let foo (x : ref int) (y : ref int) =
x := 1;
y := 2
......
......@@ -2,7 +2,7 @@ module M
use import module ref.Ref
let foo (x : ref int) (y : ref int) =
let foo (x : ref int) (y : ref int) =
x := 1;
y := 2
......
module M
use import module stdlib.Ref
use import list.List
val r : ref (list 'a)
end
......@@ -6,7 +6,7 @@ module M
(* missing variant *)
let rec even (x:int) : int variant {x} =
odd (x-1)
odd (x-1)
with odd (x:int) : int =
even (x-1)
......
......@@ -2,13 +2,13 @@
(* different relations *)
module M
use import int.Int
predicate rel int int
let rec even (x:int) : int variant {x} with rel =
odd (x-1)
odd (x-1)
with odd (x:int) : int variant {x} =
even (x-1)
......
......@@ -21,7 +21,7 @@ let f () =
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_1"
End:
End:
*)
......@@ -19,7 +19,7 @@ let test () =
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_2"
End:
End:
*)
......@@ -85,7 +85,7 @@ let test4d x =
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/for"
End:
End:
*)
......@@ -20,14 +20,14 @@ module M
let i = ref 2 in
while !i <= 10 do
invariant { 2 <= !i <= 11 /\ inv a /\
(* ghost *) !loop1 = !i - 2 /\ 2 * !loop2 <= (!i-2) * (!i-1) }
(* ghost *) !loop1 = !i - 2 /\ 2 * !loop2 <= (!i-2) * (!i-1) }
variant { 10 - !i }
(* ghost *) incr loop1;
let j = ref !i in
while a[!j] < a[!j - 1] do
invariant { 1 <= !j <= !i /\ inv a /\
(* ghost *) 2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) }
variant { !j }
(* ghost *) 2 * !loop2 <= (!i-2) * (!i-1) + 2*(!i - !j) }
variant { !j }
(* ghost *) incr loop2;
let temp = a[!j] in
a[!j] <- a[!j - 1];
......
......@@ -21,7 +21,7 @@ module M
let u = ref (length a - 1) in
while !l <= !u do
invariant {
0 <= !l /\ !u < length a /\
0 <= !l /\ !u < length a /\
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = !l + div (!u - !l) 2 in
......
......@@ -40,7 +40,7 @@ module M1
while !l <= !u do
invariant { 0 <= !l /\ !u <= n-1 /\
forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u }
variant { !u - !l }
variant { !u - !l }
let m = div (!l + !u) 2 in
if get !mem t m < v then l := m + 1
else if get !mem t m > v then u := m - 1
......@@ -94,7 +94,7 @@ module M2
while !l <= !u do
invariant { 0 <= !l /\ !u <= n-1 /\
forall k:int. 0 <= k < n -> get !mem t k = v -> !l <= k <= !u }
variant { !u - !l }
variant { !u - !l }
let m = div (!l + !u) 2 in
if get_ t m < v then l := m + 1
else if get_ t m > v then u := m - 1
......@@ -152,7 +152,7 @@ module M3
invariant { 0 <= to_int !l /\ to_int !u <= to_int n - 1 /\
forall k:int. 0 <= k < to_int n ->
to_int (get !mem t k) = to_int v -> to_int !l <= k <= to_int !u }
variant { to_int !u - to_int !l }
variant { to_int !u - to_int !l }
let m = of_int (to_int !l
+
to_int
......
......@@ -106,7 +106,7 @@ end
predicate invCourse (alloc:first_free_addr) (this:course) =
let (rStud,students,count,sum) = this in
count >= 0
/\
/\
valid_array alloc 0 (count - 1) students
/\
injective 0 (count - 1) students
......@@ -182,7 +182,7 @@ fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/course"
End:
End:
*)
......@@ -101,9 +101,9 @@ module M
(* paths and shortest paths
path x y d =
there is a path from x to y of length d
there is a path from x to y of length d
shortest_path x y d =
there is a path from x to y of length d, and no shorter path *)
there is a path from x to y of length d, and no shorter path *)
inductive path vertex vertex int =
| Path_nil :
......@@ -195,8 +195,8 @@ module M
let su = ref (g_succ u) in
while not (set_has_next su) do
invariant
{ S.subset !su (g_succ u) /\
inv src !visited !q !d /\ inv_succ2 src !visited !q u !su }
{ S.subset !su (g_succ u) /\
inv src !visited !q !d /\ inv_succ2 src !visited !q u !su }
variant { S.cardinal !su }
let v = set_next su in
relax u v
......
(* Correctness of a program computing the minimal distance between
two words (code by Claude Marché).
two words (code by Claude Marché).
This program computes a variant of the Levenshtein distance. Given
two strings [w1] and [w2] of respective lengths [n1] and [n2], it
......@@ -98,12 +98,12 @@ module Distance
/\ (forall k:int. 0 <= k <= j -> min_suffix w1 w2 (i+1) k t[k])
/\ min_suffix w1 w2 (i+1) (j+1) !o }
begin
let temp = !o in
let temp = !o in
o := t[j];
if w1[i] = w2[j] then
t[j] <- temp
else
t[j] <- (min t[j] t[j+1]) + 1
if w1[i] = w2[j] then
t[j] <- temp
else
t[j] <- (min t[j] t[j+1]) + 1
end
done
done;
......
......@@ -80,7 +80,7 @@ rewrite <- (Z_div_exact_full_2 n 3).
assert (h: (n mod 5 = 0 \/ n mod 5 <> 0)%Z) by omega.
destruct h.
rewrite Zdiv0.
Qed.
(* DO NOT EDIT BELOW *)
......
......@@ -43,7 +43,7 @@ theory FibSumEven "sum of even-valued Fibonacci numbers"
axiom SumTooLarge: forall m n:int.
n >= 0 -> (fib n) >= m -> fib_sum_even_lt_from m n = 0
(* Note: we take for granted that [fib] is an
increasing sequence *)
increasing sequence *)
axiom SumYes: forall n m s:int.
n >= 0 -> (fib n) < m -> mod (fib n) 2 = 0 ->
......
......@@ -59,14 +59,14 @@ rewrite fibn; auto with zarith.
rewrite Zplus_mod.
assert (h: (0 <= (n mod 3) < 3)%Z).
apply Z_mod_lt; auto with zarith.
assert (h':( n mod 3 = 0 \/ n mod 3 = 1 \/ n mod 3 = 2)%Z)
assert (h':( n mod 3 = 0 \/ n mod 3 = 1 \/ n mod 3 = 2)%Z)
by omega.
clear h.
clear h.
destruct h' as [h0|[h1|h2]].
split; auto with zarith.
SearchAbout Zmod.
assert
assert
Qed.
(* DO NOT EDIT BELOW *)
......
......@@ -29,11 +29,11 @@ module Flag
label Init:
while !i < !r do
invariant { 0 <= !b <= !i <= !r <= n /\
monochrome a 0 !b Blue /\
monochrome a !b !i White /\
monochrome a !r n Red /\
length a = n /\
permut_sub a (at a Init) 0 n }
monochrome a 0 !b Blue /\
monochrome a !b !i White /\
monochrome a !r n Red /\
length a = n /\
permut_sub a (at a Init) 0 n }
variant { !r - !i }
match a[!i] with
| Blue ->
......
......@@ -82,10 +82,10 @@ Parameter atan: R -> R.
Axiom Tan_atan : forall (x:R), ((Rtrigo.tan (atan x)) = x).
Inductive mode :=
| NearestTiesToEven : mode
| ToZero : mode
| Up : mode
| Down : mode
| NearestTiesToEven : mode
| ToZero : mode
| Up : mode
| Down : mode
| NearTiesToAway : mode .
Parameter single : Type.
......
......@@ -37,7 +37,7 @@ module M
interpretation on the left (or on the right); requires induction *)
lemma Interp_eq:
forall x1 x2 : M.map int int, i j : int.
(forall k : int. i <= k < j -> M.get x1 k = M.get x2 k) ->
(forall k : int. i <= k < j -> M.get x1 k = M.get x2 k) ->
interp x1 i j = interp x2 i j
(* the sum of the elements of x[i..j[ *)
......@@ -93,11 +93,11 @@ let search_safety () =
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
x[d] <- c;
let k = div delta 9 in
let k = div delta 9 in
for i = 0 to d - 1 do
invariant { length x = m }
if i < k then x[i] <- 9
else if i = k then x[i] <- mod delta 9
else if i = k then x[i] <- mod delta 9
else x[i] <- 0
done;
raise Success
......@@ -134,14 +134,14 @@ let search () =
if 0 <= delta && delta <= 9 * d then begin
x[d] <- c;
assert { sum x.elts d m = y - delta };
let k = div delta 9 in
let k = div delta 9 in
assert { k <= d };
for i = 0 to d - 1 do
invariant { length x = m /\ is_integer x.elts /\
sum x.elts d m = y - delta /\
sum x.elts 0 i = if i <= k then 9*i else delta }
if i < k then x[i] <- 9
else if i = k then x[i] <- (mod delta 9)
else if i = k then x[i] <- (mod delta 9)
else x[i] <- 0
done;
(* assume { sum !x 0 d = delta }; *)
......@@ -257,21 +257,21 @@ let search_smallest () =
for c = x[d] + 1 to 9 do
invariant {
x = at x Init /\
forall c' : int. x[d] < c' < c ->
forall c' : int. x[d] < c' < c ->
forall u : int.
interp (at x.elts Init) 0 m < u <= interp9 (M.set x.elts d c') d m ->
sum_digits u <> y }
sum_digits u <> y }
let delta = y - !s - c + x[d] in
if 0 <= delta && delta <= 9 * d then begin
assert { smallest_size delta <= d };
x[d] <- c;
assert { sum x.elts d m = y - delta };
assert { gt_digit x.elts (at x.elts Init) d };
let k = div delta 9 in
let k = div delta 9 in
assert { k <= d };
for i = 0 to d - 1 do
invariant {
length x = m /\ is_integer x.elts /\
length x = m /\ is_integer x.elts /\
sum x.elts d m = y - delta /\
sum x.elts 0 i = (if i <= k then 9*i else delta) /\
(forall j : int. 0 <= j < i ->
......@@ -279,7 +279,7 @@ let search_smallest () =
(j >= smallest_size delta -> x[j] = 0)) /\
gt_digit x.elts (at x.elts Init) d }
if i < k then x[i] <- 9
else if i = k then x[i] <- mod delta 9
else if i = k then x[i] <- mod delta 9
else x[i] <- 0;
assert { is_integer x.elts }
done;
......@@ -327,14 +327,14 @@ let () =
for c = x.(d) + 1 to 9 do
let delta = y - !s - c + x.(d) in
if 0 <= delta && delta <= 9 * d then begin
x.(d) <- c;
let k = delta / 9 in
for i = 0 to d-1 do
x.(i) <- if i < k then 9 else if i = k then delta mod 9 else 0
done;
for i = max d (n-1) downto 0 do Format.printf "%d" x.(i) done;
Format.printf "@.";
exit 0
x.(d) <- c;
let k = delta / 9 in
for i = 0 to d-1 do
x.(i) <- if i < k then 9 else if i = k then delta mod 9 else 0
done;
for i = max d (n-1) downto 0 do Format.printf "%d" x.(i) done;
Format.printf "@.";
exit 0
end
done;
s := !s - x.(d)
......
......@@ -28,7 +28,7 @@ module Quicksort
let m = ref l in
label L: begin
for i = l + 1 to r do
invariant { (forall j:int. l < j <= !m -> t[j] < v) /\
invariant { (forall j:int. l < j <= !m -> t[j] < v) /\
(forall j:int. !m < j < i -> t[j] >= v) /\
permut_sub t (at t L) l (r+1) /\
t[l] = v /\ l <= !m < i }
......
......@@ -18,7 +18,7 @@ module M
| App rope rope (len: int)
predicate inv (r: rope) = match r with
| Str s ofs len ->
| Str s ofs len ->
len = 0 \/ 0 <= ofs < S.length s /\ ofs + len <= S.length s
| App l r _ ->
0 < len l /\ inv l /\ 0 < len r /\ inv r
......@@ -33,33 +33,33 @@ module M
S.length s1 = S.length s2 /\
forall i:int. 0 <= i < S.length s1 -> S.get s1 i = S.get s2 i
let empty () =
{}
Str (S.create 0) 0 0
let empty () =
{}
Str (S.create 0) 0 0
{ len result = 0 /\ inv result /\ eq (model result) (S.create 0) }
let length r =
{}
len r
let length r =
{}
len r
{ result = len r }
(**
let rec get (r: rope) i =
let rec get (r: rope) i =
{ inv r /\ 0 <= i < len r }
match r with
| Str s ofs len ->
| Str s ofs len ->
S.get s (ofs + i)
| App l r _ ->
| App l r _ ->
let n = length l in
if i < n then get l i else get r (i - n)
end
{ result = S.get (model r) i }
**)
end
(*
Local Variables:
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/ropes"
End:
End:
*)
......@@ -74,7 +74,7 @@ Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
Parameter elt : Type.
Inductive tree :=
| Empty : tree
| Empty : tree
| Node : tree -> elt -> tree -> tree .
Parameter elements: tree -> (list elt).
......@@ -88,7 +88,7 @@ Axiom elements_def : forall (t:tree),
end.
Inductive enum :=
| Done : enum
| Done : enum
| Next : elt -> tree -> enum -> enum .
Parameter enum_elements: enum -> (list elt).
......@@ -112,7 +112,7 @@ Axiom leftlen_def : forall (t:tree),
Theorem leftlen_nonneg : forall (t:tree), (0%Z <= (leftlen t))%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
induction t;
induction t;
intuition.
rewrite (leftlen_def Empty).
omega.
......
......@@ -116,9 +116,9 @@ module M
match l with
| Node Red (Node Red a kx vx b) ky vy c
| Node Red a kx vx (Node Red b ky vy c) ->
Node Red (Node Black a kx vx b) ky vy (Node Black c k v r)
Node Red (Node Black a kx vx b) ky vy (Node Black c k v r)
| _ ->
Node Black l k v r
Node Black l k v r
end
{ bst result /\
(forall n : int. almost_rbtree n l -> rbtree n r -> rbtree (n+1) result)
......@@ -141,9 +141,9 @@ module M
match r with
| Node Red (Node Red b ky vy c) kz vz d
| Node Red b ky vy (Node Red c kz vz d) ->
Node Red (Node Black l k v b) ky vy (Node Black c kz vz d)
Node Red (Node Black l k v b) ky vy (Node Black c kz vz d)
| _ ->
Node Black l k v r
Node Black l k v r
end
{ bst result /\
(forall n : int. almost_rbtree n r -> rbtree n l -> rbtree (n+1) result)
......
......@@ -109,7 +109,7 @@ discriminate H8.
injection H8; intros; subst; clear H8.
clear H4 H5.
left.
split.
split.
rewrite (length_def _ (Cons 0%Z s)) in H2.
generalize (Length_nonnegative _ s).
omega.
......
......@@ -325,7 +325,7 @@ let () =
&& (not !opt_redo)
then
begin
eprintf "At least one bench is required or one prover and one file or
eprintf "At least one bench is required or one prover and one file or
the verification of a database .@.";
Arg.usage option_list usage_msg;
exit 1
......
......@@ -161,7 +161,7 @@ val add_proof_attempt : goal -> prover_id -> proof_attempt
val remove_proof_attempt : proof_attempt -> unit
(** removes a proof attempt from the database *)
val set_obsolete : proof_attempt -> unit
(** marks this proof as obsolete *)
......@@ -180,7 +180,7 @@ val add_transformation : goal -> transf_id -> transf
@raise AlreadyExist if a transformation with the same id
is already there *)
val remove_transformation : transf -> unit
val remove_transformation : transf -> unit
(** Removes a proof attempt from the database. Beware that the
subgoals are not removed by this function, you must remove them
first using [remove_subgoal]. In other words, this function
......
......@@ -334,7 +334,7 @@ let show_about_window () =
let ( _ : GWindow.Buttons.about) = about_dialog#run () in
about_dialog#destroy ()
let set_labels_flag =
let set_labels_flag =
let fl = Debug.lookup_flag "print_labels" in
fun b ->
(if b then Debug.set_flag else Debug.unset_flag) fl
......
......@@ -373,7 +373,7 @@ let set_proof_state ~obsolete a =
let model_index = Hashtbl.create 17
let get_any_from_iter row =
let get_any_from_iter row =
try
let idx = goals_model#get ~row ~column:index_column in
Hashtbl.find model_index idx
......@@ -391,14 +391,14 @@ let get_selected_row_references () =
(fun path -> goals_model#get_row_reference path)
goals_view#selection#get_selected_rows
let row_expanded b iter _path =
let row_expanded b iter _path =
match get_any_from_iter iter with
| M.File f ->
| M.File f ->
(*
eprintf "file_expanded <- %b@." b;
*)
M.set_file_expanded f b
| M.Theory t ->
| M.Theory t ->
(*
eprintf "theory_expanded <- %b@." b;
*)
......@@ -416,20 +416,20 @@ let row_expanded b iter _path =
| M.Proof_attempt _ -> ()
let (_:GtkSignal.id) =
let (_:GtkSignal.id) =
goals_view#connect#row_collapsed ~callback:(row_expanded false)
let (_:GtkSignal.id) =
let (_:GtkSignal.id) =
goals_view#connect#row_expanded ~callback:(row_expanded true)
let notify any =
let row,exp =
match any with
| M.Goal g ->
| M.Goal g ->
(*
if M.goal_expanded g then
begin
let n =
let n =
Hashtbl.fold (fun _ _ acc -> acc+1) (M.external_proofs g) 0
in
eprintf "expand_row on a goal with %d proofs@." n;
......@@ -441,7 +441,7 @@ let notify any =
| M.Proof_attempt a -> a.M.proof_key,false
| M.Transformation tr -> tr.M.transf_key,tr.M.transf_expanded
in
if exp then goals_view#expand_to_path row#path else
if exp then goals_view#expand_to_path row#path else
goals_view#collapse_row row#path;
match any with
| M.Goal g ->
......@@ -454,7 +454,7 @@ let notify any =
set_proof_state ~obsolete:a.M.proof_obsolete a
| M.Transformation tr ->
set_row_status row tr.M.transf_proved
let init =
let cpt = ref (-1) in
fun row any ->
......@@ -482,7 +482,7 @@ let init =
| M.Goal g -> M.goal_expl g
| M.Theory th -> M.theory_name th
| M.File f -> Filename.basename f.M.file_name
| M.Proof_attempt a ->
| M.Proof_attempt a ->
begin
match a.M.prover with
| M.Detected_prover p ->
......@@ -533,14 +533,14 @@ let () =
let () =
try
eprintf "[Info] Opening session...@\n@[<v 2> ";
M.open_session ~env:gconfig.env
M.open_session ~env:gconfig.env
(* ~provers:gconfig.provers *)
~config:gconfig.Gconfig.config
~init ~notify project_dir;
M.maximum_running_proofs := gconfig.max_running_processes;
eprintf "@]@\n[Info] Opening session: done@."
with e ->
eprintf "@[Error while opening session:@ %a@.@]"
eprintf "@[Error while opening session:@ %a@.@]"
Exn_printer.exn_printer e;
exit 1
......@@ -1175,7 +1175,7 @@ let reload () =
with
| e ->
let e = match e with
| Loc.Located(loc,e) ->
| Loc.Located(loc,e) ->
scroll_to_loc ~color:error_tag ~yalign:0.5 loc; e
| e -> e
in
......
......@@ -781,7 +781,7 @@ let file_exists fn =
(**********************************)
let reload_proof obsolete goal pid old_a =
let p =
let p =
try
Detected_prover (Util.Mstr.find pid !current_provers)
with Not_found ->
......@@ -810,7 +810,7 @@ let reload_proof ~provers obsolete goal pid old_a =
(* eprintf "proof_obsolete : %b@." obsolete; *)
let a =
raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit
~edit:old_a.edited_as goal p old_res
~edit:old_a.edited_as goal p old_res
in
!notify_fun (Goal a.proof_goal)
with Not_found ->
......@@ -876,7 +876,7 @@ and reload_trans _goal_obsolete goal _ tr =
g.goal_name subgoal_name;
*)
(Some g, Util.Mstr.remove sum old_subgoals)
with Not_found ->
with Not_found ->
(*
eprintf "Merge phase 1: no old goal -> new goal '%s'@."
subgoal_name;
......@@ -916,23 +916,23 @@ and reload_trans _goal_obsolete goal _ tr =
if merged list starts with g :
g1 < ... gk <= h1 < ... <
g1 < ... gk <= h1 < ... <
then g1 .. g{k-1} are new and gk associated to h1, and then
then g1 .. g{k-1} are new and gk associated to h1, and then
recursively merge g{k+1} ... and h2 ...
otherwise, list starts
h1 < ... hk <= g1 <= ... <
h1 < ... hk <= g1 <= ... <
....
Another formulation :
if merged list starts with
1) g1 g2 ...
1) g1 g2 ...
associate g1 to nothing and recursively process g2 ...
2) g1 h1 g2 ... with d(g1,h1) < d(h1,g2)
......@@ -940,20 +940,20 @@ and reload_trans _goal_obsolete goal _ tr =
associate g1 to h1 and recursively process g2 ...
3) g1 h1 g2 ... with d(g1,h1) > d(h1,g2)
?
4) g1 h1 h2 ...
PRELIMINARY: store the shape of the conclusion of the goal in the XML
file.
file.