package logtk

  1. Overview
  2. Docs
On This Page
  1. Test Properties
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Test Properties

Test universal properties that use defined functions, within some "reasonable" bound (e.g. smallcheck/quickcheck).

This is used to test a property semantically (by evaluation) before trying the costly proof by induction; if the property is false there is no need to try to prove it.

type term = Term.t
type lit = Literal.t
type form = Literals.t list
type res =
  1. | R_ok
  2. | R_fail of Subst.t
val normalize_form : form -> form

Use rewriting to normalize the formula

val check_form : ?limit:int -> form -> res

check_form rules form returns R_ok if the property seems to hold up to depth, or R_fail subst if subst makes form evaluate to false

  • parameter limit

    a limit on how many "steps" are done (for some notion of steps). The higher, the more expensive, but also the more accurate this is.

val default_limit : int