Revision 92cb30fe9926e97bad69dd1a8d4beef98b5659a8 authored by Adrien Koutsos on 24 November 2021, 19:22:03 UTC, committed by Adrien Koutsos on 24 November 2021, 19:22:03 UTC
1 parent 402c734
ecCHoare.mli
open EcFol
open EcPath
open EcSymbols
(* -------------------------------------------------------------------- *)
val check_loaded : EcEnv.env -> unit
(* -------------------------------------------------------------------- *)
val oget_c_bnd : form option -> bool -> form
val cost_orcl : symbol -> xpath -> form -> form
(* -------------------------------------------------------------------- *)
type csub_res = { cond : form; res : form; }
(* Backward reasoning on cost.
Looks for a solution [x] of [c = x + sub]. *)
val cost_sub : c:form -> sub:form -> csub_res
(* Same as [cost_sub], but only for the concrete cost.
[c] of type [tcost], [sub] of type [xint]. *)
val cost_sub_self : c:form -> sub:form -> csub_res
(* -------------------------------------------------------------------- *)
(* [c] of type [tcost], [a] of type [xint] *)
val cost_add_self : c:form -> a:form -> form
(* -------------------------------------------------------------------- *)
(* [choare_xsum cost (m,n)]:
[cost] of type [tcost], [m] of type [tint], [n] of type [txint].
[n] must be finite, i.e. [n = f_N n_fin]. *)
val choare_xsum : form -> (form * form) -> form
(* -------------------------------------------------------------------- *)
val free_expr : EcTypes.expr -> bool
(* The cost of an expression evaluation in any memory of type [menv]
satisfying [pre].
Type [xint]. *)
val cost_of_expr : EcFol.form -> EcMemory.memenv -> EcTypes.expr -> EcFol.form
(* The cost of an expression evaluation in any memory of type [menv].
Type [xint]. *)
val cost_of_expr_any : EcMemory.memenv -> EcTypes.expr -> EcFol.form
Computing file changes ...