package ortac-qcheck-stm

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term = {
  1. term : Gospel.Tterm.term;
  2. text : string;
}
val term : prj_txt:('a -> string) -> prj_loc:('a -> Ppxlib.Location.t) -> 'a -> Gospel.Tterm.term -> term
type new_state_formulae = {
  1. model : Ident.t;
  2. description : Gospel.Tterm.term;
}
type indexed_term = int * term
type next_state = {
  1. formulae : (int * new_state_formulae) list;
  2. modifies : (Ident.t * Ppxlib.Location.t) list;
}
type postcond = {
  1. normal : indexed_term list;
  2. exceptional : xpost list;
  3. checks : term list;
}
type value = {
  1. id : Ident.t;
  2. ty : Ppxlib.core_type;
  3. inst : (string * Ppxlib.core_type) list;
  4. sut_vars : Ident.t list;
  5. args : (Ppxlib.core_type * Ident.t option) list;
  6. ret : Ident.t list;
  7. ret_values : term list list;
  8. next_states : (Ident.t * next_state) list;
  9. precond : Gospel.Tterm.term list;
  10. postcond : postcond;
}
type init_state = {
  1. arguments : (Gospel.Tast.lb_arg * Ppxlib.expression) list;
  2. returned_sut : Ident.t;
  3. descriptions : new_state_formulae list;
}
val get_return_type : value -> Ppxlib.core_type
val value : Ident.t -> Ppxlib.core_type -> (string * Ppxlib.core_type) list -> Ident.t list -> (Ppxlib.core_type * Ident.t option) list -> Ident.t list -> term list list -> (Ident.t * next_state) list -> Gospel.Tterm.term list -> postcond -> value
type t = {
  1. state : (Ident.t * Ppxlib.core_type) list;
  2. invariants : (Ident.t * term list) option;
  3. init_state : init_state;
  4. ghost_functions : Gospel.Tast.function_ list;
  5. ghost_types : (Gospel.Tast.rec_flag * Gospel.Tast.type_declaration list) list;
  6. values : value list;
}
OCaml

Innovation. Community. Security.