Commit 5130cf43 authored by Andrei Paskevich's avatar Andrei Paskevich

update CHANGES + some cosmetics

parent c69c2624
......@@ -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
......
......@@ -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 \\
......
......@@ -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
......
......@@ -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
......
......@@ -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)
......
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