mlw_wp.mli 1.53 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
val mark_theory : Theory.theory
31
32
val th_mark_at  : Theory.theory
val th_mark_old : Theory.theory
Andrei Paskevich's avatar
Andrei Paskevich committed
33

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

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

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

43
44
(** Weakest preconditions *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
46
47
48
49
50
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
51
52