From 5130cf436132b504918dcaf2f4f36ace99119b62 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Sun, 24 Jun 2018 14:38:41 +0200
Subject: [PATCH] update CHANGES + some cosmetics
---
CHANGES.md | 20 +++++++++++++-------
doc/manual.tex | 2 --
examples/binary_sort.mlw | 3 +--
examples/bitwalker.mlw | 8 +++-----
src/mlw/vc.ml | 18 +++++++++---------
5 files changed, 26 insertions(+), 25 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index 00749518a..d3cde36af 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -12,8 +12,8 @@ Language
so equality functions must be declared/defined on a per-type basis
(already done for type `int` in the standard library) :x:
* added overloading of program symbols
- * new clause `alias` in function contracts :x:
- * support for multiple assignments
+ * new contract clause `alias { <term> with <term>, ... }` :x:
+ * support for parallel assignment `<term>,... <- <term>,...`
* type invariants now produce logical axioms;
a type with an invariant must be proved to be inhabited :x:
* support for local exceptions using `exception ... in ...`
@@ -21,12 +21,18 @@ Language
* support for `exception` branches in `match` constructs
* support for `for` loops on range types
(including machine integers from the standard library)
- * attribute `[@vc:sp]` on an expression switches from traditional WP to
- Flanagan-Saxe-like VC generation
+ * attribute `[@vc:sp]` on an expression switches from traditional WP
+ to Flanagan-Saxe-like VC generation
* support for type coercions in logic using `meta coercion`
- * deprecated `theory`; use `module` instead
+ * keyword `theory` is deprecated; use `module` instead
* term on the left of sequence `;` must be of type `unit` :x:
- * cloned axioms are now turned into lemmas; use `with axiom foo` to prevent :x:
+ * cloned axioms turn into lemmas; use `with axiom my_axiom`
+ or `with axiom .` to keep them as axioms :x:
+ * `any <type> <spec>` produces an existential precondition;
+ use `val f : <type> <spec> in ...` (unsafe!) instead :x:
+ * `use T` and `clone T` now import the generated namespace T;
+ use `use T as T` and `clone T as T` to prevent this :x:
+ * `pure { <term> }` produces a ghost value in program code
Standard library
* machine integers in `mach.int.*` are now range types :x:
@@ -39,7 +45,7 @@ Extraction
Transformations
* transformations can now have arguments
- * added transformations `assert`, `apply`, `cut`, `rewrite`, etc, à la Coq
+ * added transformations `assert`, `apply`, `cut`, `rewrite`, etc., à la Coq
* added transformations for reflection-based proofs
Drivers
diff --git a/doc/manual.tex b/doc/manual.tex
index bed077b9b..8f0264fec 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -334,8 +334,6 @@ file contains other potential incompatibility.
\hline
\texttt{at x 'L} & \texttt{x at L} \\
\hline
-\texttt{assert \{ ... (old x) ... \}} & \texttt{assert \{ ... (x at Init) ... \}} \\
-\hline
\texttt{\char`\\ x. e} & \texttt{fun x -> e} \\
\hline
\texttt{use HighOrd} & nothing, not needed anymore \\
diff --git a/examples/binary_sort.mlw b/examples/binary_sort.mlw
index 8d364ac2a..4b8f7db5e 100644
--- a/examples/binary_sort.mlw
+++ b/examples/binary_sort.mlw
@@ -39,11 +39,10 @@ module BinarySort
ensures { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
ensures { permut_sub (old a) a 0 (length a) }
=
- label Init in
for k = 1 to length a - 1 do
(* a[0..k-1) is sorted; insert a[k] *)
invariant { forall i j. 0 <= i <= j < k -> a[i] <= a[j] }
- invariant { permut_sub (a at Init) a 0 (length a) }
+ invariant { permut_sub (old a) a 0 (length a) }
let v = a[k] in
let left = ref 0 in
let right = ref k in
diff --git a/examples/bitwalker.mlw b/examples/bitwalker.mlw
index b5504d5d5..d2e4999c7 100644
--- a/examples/bitwalker.mlw
+++ b/examples/bitwalker.mlw
@@ -254,18 +254,17 @@ module Bitwalker
let lstart = BV32.sub_check (BV32.of_int 64) len in
let i = ref BV32.zeros in
- label Init in
while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
invariant {0 <= BV32.t'int !i <= BV32.t'int len}
invariant {forall j:int. 0 <= j < BV32.t'int start ->
- nth8_stream (addr at Init) j
+ nth8_stream (old addr) j
= nth8_stream addr j}
invariant {forall j:int. BV32.t'int start <= j < BV32.t'int start + BV32.t'int !i ->
nth8_stream addr j
= BV64.nth value (BV32.t'int len - j - 1 + BV32.t'int start) }
invariant {forall j:int. BV32.t'int start + BV32.t'int !i <= j < 8 * length addr ->
nth8_stream addr j
- = nth8_stream (addr at Init) j }
+ = nth8_stream (old addr) j }
let flag = peek_64bit value (BV32.add_check lstart !i) in
@@ -292,7 +291,6 @@ module Bitwalker
ensures {forall i. 0 <= i < 8 * length addr ->
nth8_stream addr i = nth8_stream (old addr) i}
=
- label Init in
let value = peek start len addr in
let res = poke start len addr value in
@@ -300,7 +298,7 @@ module Bitwalker
assert {forall i. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
nth8_stream addr i
- = nth8_stream (addr at Init) i};
+ = nth8_stream (old addr) i};
res
diff --git a/src/mlw/vc.ml b/src/mlw/vc.ml
index 045acf8bf..631988d84 100644
--- a/src/mlw/vc.ml
+++ b/src/mlw/vc.ml
@@ -20,7 +20,7 @@ open Pdecl
(* basic tools *)
-let debug = Debug.register_info_flag "vc_debug"
+let debug_vc = Debug.register_info_flag "vc_debug"
~desc:"Print@ details@ of@ verification@ conditions@ generation."
let debug_reflow = Debug.register_info_flag "vc_reflow"
@@ -29,11 +29,11 @@ let debug_reflow = Debug.register_info_flag "vc_reflow"
let debug_sp = Debug.register_flag "vc_sp"
~desc:"Use@ 'Efficient@ Weakest@ Preconditions'@ for@ verification."
-let no_eval = Debug.register_flag "vc_no_eval"
+let debug_no_eval = Debug.register_flag "vc_no_eval"
~desc:"Do@ not@ simplify@ pattern@ matching@ on@ record@ datatypes@ in@ VCs."
-let debug_ignore_missing_diverges = Debug.register_info_flag "ignore_missing_diverges"
- ~desc:"Suppress@ warnings@ on@ missing@ diverges"
+let debug_ignore_diverges = Debug.register_info_flag "ignore_missing_diverges"
+ ~desc:"Suppress@ warnings@ on@ missing@ diverges."
let case_split = Ident.create_attribute "case_split"
let add_case t = t_attr_add case_split t
@@ -523,7 +523,7 @@ let rec k_expr env lps e res xmap =
let var_or_proxy = var_or_proxy_case xmap in
let check_divergence k =
if eff.eff_oneway && not env.divergent then begin
- if Debug.test_noflag debug_ignore_missing_diverges then
+ if Debug.test_noflag debug_ignore_diverges then
Warning.emit ?loc "termination@ of@ this@ expression@ \
cannot@ be@ proved,@ but@ there@ is@ no@ `diverges'@ \
clause@ in@ the@ outer@ specification";
@@ -1184,12 +1184,12 @@ let rec havoc kn wr regs t ity fl =
t, begin match f.t_node with Ttrue -> fl | _ -> f::fl end
end
-let print_dst dst = if Debug.test_flag debug then
+let print_dst dst = if Debug.test_flag debug_vc then
Format.printf "@[vars = %a@]@." (Pp.print_list Pp.space
(fun fmt (o,n) -> Format.fprintf fmt "(%a -> %a)"
Ity.print_pv o Pretty.print_vs n)) (Mpv.bindings dst)
-let print_regs regs = if Debug.test_flag debug then
+let print_regs regs = if Debug.test_flag debug_vc then
Format.printf "@[regs = %a@]@." (Pp.print_list Pp.space
(fun fmt (r,t) -> Format.fprintf fmt "(%a -> %a)"
Ity.print_reg r Pretty.print_term t)) (Mreg.bindings regs)
@@ -1466,7 +1466,7 @@ and wp_expr kn k q = match k with
(** VCgen *)
let vc_kode {known_map = kn} vc_wp k =
- if Debug.test_flag debug then
+ if Debug.test_flag debug_vc then
Format.eprintf "K @[%a@]@\n" k_print k;
let k = reflow vc_wp k in
if Debug.test_flag debug_reflow then
@@ -1486,7 +1486,7 @@ let mk_vc_decl kn id f =
let pr = create_prsymbol (id_fresh ~attrs ?loc ("VC " ^ nm)) in
let f = wp_forall (Mvs.keys (t_freevars Mvs.empty f)) f in
let f = Typeinv.inject kn f in
- let f = if Debug.test_flag no_eval then f else
+ let f = if Debug.test_flag debug_no_eval then f else
Eval_match.eval_match kn f in
create_pure_decl (create_prop_decl Pgoal pr f)
--
GitLab