sig
  type 'a predicate = 'a -> bool
  type ('a, 'b) t = {
    precond : 'a Specification.predicate;
    postcond : ('a * 'b) Specification.predicate;
  }
  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
  type 'a outcome = Result of 'a | Exception of exn
  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 : Specification.Pred.p Specification.predicate end
  module Map :
    functor (M : Map.S) ->
      functor (P : sig type p = M.key val p : p 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 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 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