mlw_wp.mli 1.71 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
(*                                                                  *)
(*  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
(* unused
25
val fs_old : Term.lsymbol
26
27
*)
val t_at_old : Term.term -> Term.term
28
29
30

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

32
val e_now : expr
Andrei Paskevich's avatar
Andrei Paskevich committed
33

34
val pv_old : pvsymbol
35
val remove_old : Term.term -> Term.term
36

37
38
39
val full_invariant :
  Decl.known_map -> Mlw_decl.known_map -> Term.vsymbol -> ity -> Term.term

40
41
(** Weakest preconditions *)

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


(** 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
53
val fast_wp_rec: Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
54