▼ACL2s Beginner Mode
On this page:
definec
defunc
check=
defconst
test?
  top  contents    up   

1 Definitions and Checks🔗ℹ

syntax

(definec fn-name (param ...) :out-type
  body-expr)
 
param = param-name :in-type
Defines the function fn-name.

; sum-n : Nat -> Nat
; Given n, return 0 + 1 + 2 + ... + n
> (definec sum-n (n :nat) :nat
    (cond ((equal n 0) 0)
          (t ; else
           (+ n (sum-n (- n 1))))))

syntax

(defunc fn-name (param-name ...)
  :input-contract in-ctc-expr
  :output-contract out-ctc-expr
  body-expr)
Defines the function fn-name.

; sum-n : Nat -> Nat
; Given n, return 0 + 1 + 2 + ... + n
> (defunc sum-n (n)
    :input-contract (natp n)
    :output-contract (natp (sum-n n))
    (cond ((equal n 0) 0)
          (t ; else
           (+ n (sum-n (- n 1))))))

syntax

(check= actual-expr expected-expr)

Checks that actual-expr and expected-expr are equal.

> (check= (sum-n 5) (+ 1 2 3 4 5))
> (check= (sum-n 0) 0)
> (check= (sum-n 3) 6)
> (check= (sum-n 4) -32)

--------------------

FAILURE

name:       check=

location:   eval:7:0

actual:     10

expected:   -32

--------------------

> (check= (sum-n 4) 10)
> (check= (sum-n 100) 5050)

syntax

(defconst *name* expr)

Defines *name* as a constant with the value of expr. The *name* must start and end with a * character.

> (defconst *num-letters* 26)
> *num-letters*

26

syntax

(test? expr-with-free-vars)

Tests whether the expr-with-free-vars is always true when a bunch of different values are filled in for the free variables.

The simplest test?s, without free variables, just check that the expression produces true:

> (test? t)
> (test? nil)

--------------------

FAILURE

name:       check-t

location:   eval:13:0

params:     '(nil)

--------------------

> (test? (equal (sum-n 5) 15))
> (test? (< (sum-n 10) 100))
> (test? (integerp 36))
> (test? (integerp "not an integer"))

--------------------

FAILURE

name:       check-t

location:   eval:17:0

params:     '(nil)

--------------------

> (test? (equal (rev (list 7 8 9)) (list 9 8 7)))

Other test?s might use free variables to test that it works the same way for any values.

> (test? (equal (rev (list a b c)) (list c b a)))
> (test? (equal (app (list a b) (list c d)) (list a b c d)))

To test functions that work on only a certain types of data, you can guard tests with an implies form. The sum-n function works on natural numbers, so you can wrap (implies (natp x) ....) around the test expression to test it with only natural numbers.

> (test? (implies (natp x) (> (sum-n x) x)))
> (test? (implies (natp y) (< (sum-n y) (* y y))))
> (test? (implies (natp n)
           (equal (sum-n n)
                  (/ (* n (+ n 1)) 2))))
  top  contents    up