package logtk

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

Module Logtk.Test_propSource

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.

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

Use rewriting to normalize the formula

Sourceval 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.

Sourceval 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