package ortac-qcheck-stm

  1. Overview
  2. Docs
package ortac-qcheck-stm
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:('b -> Ppxlib.Location.t) -> 'c -> 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_var : Ident.t;
  5. args : (Ppxlib.core_type * Ident.t option) list;
  6. ret : Ident.t list;
  7. ret_values : term list list;
  8. next_state : next_state;
  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 -> (Ppxlib.core_type * Ident.t option) list -> Ident.t list -> term list list -> next_state -> 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. 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