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  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
Andrei Paskevich's avatar
Andrei Paskevich committed
11

12
13
(** {1 Weakest preconditions} *)

14
open Theory
15
open Mlw_ty.T
16
open Mlw_decl
17
open Mlw_expr
Andrei Paskevich's avatar
Andrei Paskevich committed
18

19
(** {2 WP-only builtins} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
20

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

Andrei Paskevich's avatar
Andrei Paskevich committed
23
val fs_at  : Term.lsymbol
24
val fs_old : Term.lsymbol
25

26
val t_at_old : Term.term -> Term.term
27

28
val mark_theory : Theory.theory
29
30
val th_mark_at  : Theory.theory
val th_mark_old : Theory.theory
Andrei Paskevich's avatar
Andrei Paskevich committed
31

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

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
(** {2 Weakest precondition computations} *)
41

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
42
43
44
45
46
47
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