• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/io
      • Std/osets
      • Std/basic
      • Std/system
      • Std/typed-lists
      • Std/bitsets
      • Std/testing
        • Must-fail
        • Assert!-stobj
        • Must-eval-to
        • Assert!
        • Must-succeed
        • Must-succeed*
        • Assert?
        • Must-fail-with-soft-error
        • Must-fail-with-hard-error
        • Must-fail-with-error
        • Must-eval-to-t
        • Must-prove
        • Must-not-prove
        • Must-not-be-table-key
        • Must-be-redundant
        • Must-fail-local
        • Must-be-table-key
        • Assert-equal
      • Std/typed-alists
      • Std/stobjs
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Std
  • Testing-utilities

Std/testing

A library of testing utilities.

These are utilities for creating tests. This library does not contain actual tests (other than perhaps tests for the testing utilities themselves), which are normally next to the code that they test. Note that community-book system/tests/ contains actual tests, for the ACL2 system code.

Subtopics

Must-fail
A top-level assert$-like command. Ensures that a command which returns an error-triple—e.g., defun or defthm—will not be successful.
Assert!-stobj
Variant of assert! and assert-event allowing stobjs
Must-eval-to
A top-level assert$-like command to ensure that a form evaluates to a non-erroneous error triple with the value of a specified expression.
Assert!
Event variant of assert$ that abbreviates assert-event
Must-succeed
A top-level assert$-like command. Ensures that a command which returns an error-triple—e.g., a defun or defthm—will return successfully.
Must-succeed*
A variant of must-succeed that accepts multiple forms.
Assert?
A variation of assert$ with customizable context and message.
Must-fail-with-soft-error
A specialization of must-fail to ensure that a soft error occurs.
Must-fail-with-hard-error
A specialization of must-fail to ensure that a hard error occurs.
Must-fail-with-error
A specialization of must-fail to ensure that an error occurs.
Must-eval-to-t
A specialization of must-eval-to to ensure that a form evaluates to a non-erroneous error triple with value t.
Must-prove
A top-level assert$-like command to ensure that a formula gets proved.
Must-not-prove
A top-level assert$-like command to ensure that a formula does not get proved.
Must-not-be-table-key
A top-level assert$-like command to ensure that a table does not include a certain key.
Must-be-redundant
A top-level assert$-like command to ensure that given forms are redundant.
Must-fail-local
A local variant of must-fail.
Must-be-table-key
A top-level assert$-like command to ensure that a table includes a certain key.
Assert-equal
Abbreviation for calling assert! on an equality.