sig
type 'a predicate = 'a Specification.predicate
type ('a, 'b) t =
('a, 'b) Specification.t = {
precond : 'a Abbreviations.Spec.predicate;
postcond : ('a * 'b) Abbreviations.Spec.predicate;
}
type 'a outcome = Result of 'a | Exception of exn
val implies :
'a Specification.predicate ->
('a * 'b) Specification.predicate -> ('a, 'b) Specification.t
val ( => ) :
'a Specification.predicate ->
('a * 'b) Specification.predicate -> ('a, 'b) Specification.t
val implies' :
'a Specification.predicate ->
'b Specification.predicate -> ('a, 'b) Specification.t
val ( ==> ) :
'a Specification.predicate ->
'b Specification.predicate -> ('a, 'b) Specification.t
val is_exception :
exn Specification.predicate ->
'a Specification.outcome Specification.predicate
val is_result :
'a Specification.predicate ->
'a Specification.outcome Specification.predicate
val always : 'a Specification.predicate
val never : 'a Specification.predicate
val is_pos_int : int Specification.predicate
val is_neg_int : int Specification.predicate
val is_zero_int : int Specification.predicate
val is_nonzero_int : int Specification.predicate
val is_even_int : int Specification.predicate
val is_odd_int : int Specification.predicate
val is_pos_int32 : int32 Specification.predicate
val is_neg_int32 : int32 Specification.predicate
val is_zero_int32 : int32 Specification.predicate
val is_nonzero_int32 : int32 Specification.predicate
val is_even_int32 : int32 Specification.predicate
val is_odd_int32 : int32 Specification.predicate
val is_pos_int64 : int64 Specification.predicate
val is_neg_int64 : int64 Specification.predicate
val is_zero_int64 : int64 Specification.predicate
val is_nonzero_int64 : int64 Specification.predicate
val is_even_int64 : int64 Specification.predicate
val is_odd_int64 : int64 Specification.predicate
val is_pos_nativeint : nativeint Specification.predicate
val is_neg_nativeint : nativeint Specification.predicate
val is_zero_nativeint : nativeint Specification.predicate
val is_nonzero_nativeint : nativeint Specification.predicate
val is_even_nativeint : nativeint Specification.predicate
val is_odd_nativeint : nativeint Specification.predicate
val is_pos_float : float Specification.predicate
val is_neg_float : float Specification.predicate
val is_zero_float_eps : float -> float Specification.predicate
val is_nonzero_float_eps : float -> float Specification.predicate
val is_zero_float : float Specification.predicate
val is_nonzero_float : float Specification.predicate
val is_nan_float : float Specification.predicate
val is_nonnan_float : float Specification.predicate
val is_letter_char : char Specification.predicate
val is_digit_char : char Specification.predicate
val is_digit_bin_char : char Specification.predicate
val is_digit_oct_char : char Specification.predicate
val is_digit_hex_char : char Specification.predicate
val is_space_char : char Specification.predicate
val is_alphanum_char : char Specification.predicate
val is_empty_string : string Specification.predicate
val is_nonempty_string : string Specification.predicate
val is_empty_list : 'a list Specification.predicate
val is_nonempty_list : 'a list Specification.predicate
val is_empty_array : 'a array Specification.predicate
val is_nonempty_array : 'a array Specification.predicate
val is_none_option : 'a option Specification.predicate
val is_some_option : 'a option Specification.predicate
val exists_string :
char Specification.predicate -> string Specification.predicate
val for_all_string :
char Specification.predicate -> string Specification.predicate
val exists_list :
'a Specification.predicate -> 'a list Specification.predicate
val for_all_list :
'a Specification.predicate -> 'a list Specification.predicate
val exists_array :
'a Specification.predicate -> 'a array Specification.predicate
val for_all_array :
'a Specification.predicate -> 'a array Specification.predicate
module type Pred = sig type p val p : p Specification.predicate end
module Map :
functor (M : Map.S) ->
functor
(P : sig type p = M.key val p : p Specification.predicate end) ->
sig
val exists :
'a Specification.predicate -> 'a M.t Specification.predicate
val for_all :
'a Specification.predicate -> 'a M.t Specification.predicate
end
module Set :
functor (S : Set.S) ->
functor
(P : sig type p = S.elt val p : p Specification.predicate end) ->
sig
val exists : S.t Specification.predicate
val for_all : S.t Specification.predicate
end
val exists_hashtbl :
('a * 'b) Specification.predicate ->
('a, 'b) Hashtbl.t Specification.predicate
val for_all_hashtbl :
('a * 'b) Specification.predicate ->
('a, 'b) Hashtbl.t Specification.predicate
val exists_queue :
'a Specification.predicate -> 'a Queue.t Specification.predicate
val for_all_queue :
'a Specification.predicate -> 'a Queue.t Specification.predicate
val exists_stack :
'a Specification.predicate -> 'a Stack.t Specification.predicate
val for_all_stack :
'a Specification.predicate -> 'a Stack.t Specification.predicate
val exists_weak :
'a option Specification.predicate -> 'a Weak.t Specification.predicate
val for_all_weak :
'a option Specification.predicate -> 'a Weak.t Specification.predicate
module Weak :
functor (W : Weak.S) ->
functor
(P : sig type p = W.data val p : p Specification.predicate end) ->
sig
val exists : W.t Specification.predicate
val for_all : W.t Specification.predicate
end
val logand :
'a Specification.predicate ->
'a Specification.predicate -> 'a Specification.predicate
val ( &&& ) :
'a Specification.predicate ->
'a Specification.predicate -> 'a Specification.predicate
val logand_list :
'a Specification.predicate list -> 'a Specification.predicate
val ( &&&& ) :
'a Specification.predicate list -> 'a Specification.predicate
val logor :
'a Specification.predicate ->
'a Specification.predicate -> 'a Specification.predicate
val ( ||| ) :
'a Specification.predicate ->
'a Specification.predicate -> 'a Specification.predicate
val logor_list :
'a Specification.predicate list -> 'a Specification.predicate
val ( |||| ) :
'a Specification.predicate list -> 'a Specification.predicate
val logxor :
'a Specification.predicate ->
'a Specification.predicate -> 'a Specification.predicate
val ( ^^^ ) :
'a Specification.predicate ->
'a Specification.predicate -> 'a Specification.predicate
val logxor_list :
'a Specification.predicate list -> 'a Specification.predicate
val ( ^^^^ ) :
'a Specification.predicate list -> 'a Specification.predicate
val not : 'a Specification.predicate -> 'a Specification.predicate
val zip1 : 'a Specification.predicate -> 'a Specification.predicate
val zip2 :
'a Specification.predicate ->
'b Specification.predicate -> ('a * 'b) Specification.predicate
val zip3 :
'a Specification.predicate ->
'b Specification.predicate ->
'c Specification.predicate -> ('a * 'b * 'c) Specification.predicate
val zip4 :
'a Specification.predicate ->
'b Specification.predicate ->
'c Specification.predicate ->
'd Specification.predicate -> ('a * 'b * 'c * 'd) Specification.predicate
val zip5 :
'a Specification.predicate ->
'b Specification.predicate ->
'c Specification.predicate ->
'd Specification.predicate ->
'e Specification.predicate ->
('a * 'b * 'c * 'd * 'e) Specification.predicate
val create_int_functions :
('a -> 'a -> int) ->
'a ->
('a -> 'a -> 'a) ->
'a ->
'a Specification.predicate * 'a Specification.predicate *
'a Specification.predicate * 'a Specification.predicate *
'a Specification.predicate * 'a Specification.predicate
end