mlw_wp.mli 1.66 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
4
5
6
7
8
9
10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
Andrei Paskevich's avatar
Andrei Paskevich committed
11

12
open Theory
13
14
open Mlw_ty
open Mlw_ty.T
15
open Mlw_decl
16
open Mlw_expr
Andrei Paskevich's avatar
Andrei Paskevich committed
17
18
19
20
21
22
23

(** WP-only builtins *)

val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty

val fs_at  : Term.lsymbol
24
25
26
27
val fs_old : Term.lsymbol

val th_mark_at  : Theory.theory
val th_mark_old : Theory.theory
Andrei Paskevich's avatar
Andrei Paskevich committed
28

29
val e_now : expr
Andrei Paskevich's avatar
Andrei Paskevich committed
30

31
val pv_old : pvsymbol
32
val remove_old : Term.term -> Term.term
33

34
35
36
val full_invariant :
  Decl.known_map -> Mlw_decl.known_map -> Term.vsymbol -> ity -> Term.term

37
38
(** Weakest preconditions *)

39
val wp_val: Env.env -> known_map -> theory_uc -> let_sym  -> theory_uc
40
val wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
41
val wp_rec: Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
42
43
44
45
46
47
48
49


(** Efficient weakest preconditions *)

val fast_wp: Debug.flag

val fast_wp_val: Env.env -> known_map -> theory_uc -> let_sym  -> theory_uc
val fast_wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
50
val fast_wp_rec: Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
51