Newer
Older
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Tactical
open Strategy
(* -------------------------------------------------------------------------- *)
(** {2 Basic Strategies}
It is always safe to apply strategies to any goal. *)
(* -------------------------------------------------------------------------- *)
val array : ?priority:float -> selection -> strategy
val choice : ?priority:float -> selection -> strategy
val absurd : ?priority:float -> selection -> strategy
val contrapose : ?priority:float -> selection -> strategy
val compound : ?priority:float -> selection -> strategy
val cut : ?priority:float -> ?modus:bool -> selection -> strategy
val filter : ?priority:float -> ?anti:bool -> unit -> strategy
val havoc : ?priority:float -> selection -> strategy
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
val separated : ?priority:float -> selection -> strategy
val instance : ?priority:float -> selection -> selection list -> strategy
val lemma : ?priority:float -> ?at:selection -> string -> selection list -> strategy
val intuition : ?priority:float -> selection -> strategy
val range : ?priority:float -> selection -> vmin:int -> vmax:int -> strategy
val split : ?priority:float -> selection -> strategy
val definition : ?priority:float -> selection -> strategy
(* -------------------------------------------------------------------------- *)
(** {2 Registered Heuristics} *)
(* -------------------------------------------------------------------------- *)
val auto_split : Strategy.heuristic
val auto_range : Strategy.heuristic
module Range :
sig
type rg
val compute : Conditions.sequence -> rg
val ranges : rg -> (int * int) Lang.F.Tmap.t
val bounds : rg -> (int option * int option) Lang.F.Tmap.t
end
(* -------------------------------------------------------------------------- *)
(** {2 Trusted Tactical Process}
Tacticals with hand-written process are not safe.
However, the combinators below are guarantied to be sound. *)
(* -------------------------------------------------------------------------- *)
(** Find a contradiction. *)
val t_absurd : process
(** Keep goal unchanged. *)
val t_id : process
(** Apply a description to a leaf goal. Same as [t_descr "..." t_id]. *)
val t_finally : string -> process
(** Apply a description to each sub-goal *)
val t_descr : string -> process -> process
(** Split with [p] and [not p]. *)
val t_split : ?pos:string -> ?neg:string -> Lang.F.pred -> process
(** Prove condition [p] and use-it as a forward hypothesis. *)
val t_cut : ?by:string -> Lang.F.pred -> process -> process
(** Case analysis: [t_case p a b] applies process [a] under hypothesis [p]
and process [b] under hypothesis [not p]. *)
val t_case : Lang.F.pred -> process -> process -> process
(** Complete analysis: applies each process under its guard, and proves that
all guards are complete. *)
val t_cases : ?complete:string -> (Lang.F.pred * process) list -> process
(** Apply second process to every goal generated by the first one. *)
val t_chain : process -> process -> process
(** @raise Invalid_argument when range is empty *)
val t_range : Lang.F.term -> int -> int ->
upper:process -> lower:process -> range:process -> process
(** Prove [src=tgt] then replace [src] by [tgt]. *)
val t_replace :
?equal:string -> src:Lang.F.term -> tgt:Lang.F.term -> process -> process
(**************************************************************************)