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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct