Module LustreContract

type svar = {
  1. pos : Lib.position;
    (*

    Position of the original expression.

    *)
  2. num : int;
    (*

    Number given to it at parse time.

    If this svar is an assumption / a guarantee, it means it's the num assumption / guarantee in the contract it's from.

    If this svar is a require / an ensure, it means it's the num require / ensure of the mode it's from.

    *)
  3. name : string option;
    (*

    Optional name for an assume or a guarantee

    *)
  4. src_expr : string;
    (*

    Source expression of this contract variable

    *)
  5. svar : StateVar.t;
    (*

    Actual state variable.

    *)
  6. scope : (Lib.position * string) list;
    (*

    Succession of imports leading to this precise state variable.

    *)
}

Wraps a state variable for use in a contract.

val mk_svar : Lib.position -> int -> string option -> StateVar.t -> (Lib.position * string) list -> string -> svar

Creates a svar.

val pos_of_svar : svar -> Lib.position

Returns the position of the svar

val prop_name_of_svar : svar -> string -> string -> string

Generates a property name.

prop_name_of_svar svar kind name generates a property name with the trace of contract call / position pairs. kind and name are concatenated and placed between the trace and the svar position and number.

type mode = {
  1. name : LustreIdent.t;
    (*

    Name of the mode.

    *)
  2. pos : Lib.position;
    (*

    Position of the mode.

    *)
  3. path : string list;
    (*

    Path of contract imports to this node.

    *)
  4. requires : svar list;
    (*

    Requires of the mode.

    *)
  5. ensures : svar list;
    (*

    Ensures of the mode.

    *)
  6. candidate : bool;
    (*

    Is this mode a candidate?.

    *)
}

Type of modes.

val mk_mode : LustreIdent.t -> Lib.position -> string list -> svar list -> svar list -> bool -> mode

Creates a mode.

type t = {
  1. assumes : svar list;
    (*

    Assumptions of the contract.

    *)
  2. sofar_assump : StateVar.t option;
    (*

    State variable to model Sofar(/\ assumes), if any

    *)
  3. guarantees : (svar * bool) list;
    (*

    Guarantees of the contract (boolean is the candidate flag).

    *)
  4. modes : mode list;
    (*

    Modes of the contract.

    *)
}

Type of contracts.

val mk : svar list -> StateVar.t option -> (svar * bool) list -> mode list -> t

Creates a new contract from a set of assumes, a set of guarantess, and a list of modes.

val add_ass : t -> svar list -> t

Adds assumes to a contract.

val add_gua : t -> (svar * bool) list -> t

Adds guarantees to a contract.

val add_modes : t -> mode list -> t

Adds modes to a contract.

val svars_of : ?with_sofar_var:bool -> t -> StateVar.StateVarSet.t
val pp_print_svar : Stdlib.Format.formatter -> svar -> unit

Pretty prints a svar wrapper.

val pp_print_svar_debug : Stdlib.Format.formatter -> svar -> unit

Pretty prints a svar wrapper for debugging.

val pp_print_mode : bool -> Stdlib.Format.formatter -> mode -> unit

Pretty prints a mode.

val pp_print_mode_debug : bool -> Stdlib.Format.formatter -> mode -> unit

Pretty prints a mode for debugging.

val pp_print_contract : bool -> Stdlib.Format.formatter -> t -> unit

Pretty prints a contract.

val pp_print_contract_debug : bool -> Stdlib.Format.formatter -> t -> unit

Pretty prints a contract for debugging.

module ModeTrace : sig ... end

Mode traces as cex.