mlw_wp.mli 1.5 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   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

(** WP-only builtins *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
20
21
val lemma_label : Ident.label

Andrei Paskevich's avatar
Andrei Paskevich committed
22
23
24
25
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty

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

28
val t_at_old : Term.term -> Term.term
29
30
31

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

MARCHE Claude's avatar
MARCHE Claude committed
33
val fs_now : Term.lsymbol
34
val e_now : expr
Andrei Paskevich's avatar
Andrei Paskevich committed
35

36
val pv_old : pvsymbol
37
val remove_old : Term.term -> Term.term
38

39
40
41
val full_invariant :
  Decl.known_map -> Mlw_decl.known_map -> Term.vsymbol -> ity -> Term.term

42
43
(** Weakest preconditions *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
44
45
46
47
48
49
val wp_val:
  wp:bool -> Env.env -> known_map -> theory_uc -> let_sym  -> theory_uc
val wp_let:
  wp:bool -> Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val wp_rec:
  wp:bool -> Env.env -> known_map -> theory_uc -> fun_defn list -> theory_uc
50
51