package ortac-qcheck-stm

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type new_state_formulae = {
  1. model : Ident.t;
  2. description : Gospel.Tterm.term;
}
type term = int * Gospel.Tterm.term
type next_state = {
  1. formulae : (int * new_state_formulae) list;
  2. modifies : (Ident.t * Ppxlib.Location.t) list;
}
type postcond = {
  1. normal : term list;
  2. exceptional : xpost list;
  3. checks : Gospel.Tterm.term list;
}
type value = {
  1. id : Ident.t;
  2. ty : Ppxlib.core_type;
  3. inst : (string * Ppxlib.core_type) list;
  4. sut_var : Ident.t;
  5. args : (Ppxlib.core_type * Ident.t option) list;
  6. ret : Ident.t list;
  7. next_state : next_state;
  8. precond : Gospel.Tterm.term list;
  9. 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 -> (Ppxlib.core_type * Ident.t option) list -> Ident.t list -> next_state -> Gospel.Tterm.term list -> postcond -> value
type t = {
  1. state : (Ident.t * Ppxlib.core_type) list;
  2. init_state : init_state;
  3. ghost_functions : Gospel.Tast.function_ list;
  4. values : value list;
}
val pp_state : Stdlib.Format.formatter -> (Ident.t * Astlib.Ast_414.Parsetree.core_type) list -> unit
val pp_inst : Stdlib.Format.formatter -> (string * Astlib.Ast_414.Parsetree.core_type) list -> unit
val pp_value : Stdlib.Format.formatter -> value -> unit
val pp : Stdlib.Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.