1 Definitions and Checks

On this page:

definec

defunc

check=

defconst

test?

top ← prev up next →

1Definitions and Checks🔗 i

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 n0)0)
(t ;else
(+ n(sum-n(- n1))))))

syntax
( defunc fn-name(param-name...)
:input-contractin-ctc-expr
:output-contractout-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-nn))
(cond ((equal n0)0)
(t ;else
(+ n(sum-n(- n1))))))

syntax
( check= actual-exprexpected-expr)

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

> (check= (sum-n5)(+ 12345))
> (check= (sum-n0)0)
> (check= (sum-n3)6)
> (check= (sum-n4)-32)

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

FAILURE

name: check=

location: eval:7:0

actual: 10

expected: -32

--------------------
> (check= (sum-n4)10)
> (check= (sum-n100)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-n5)15))
> (test? (< (sum-n10)100))
> (test? (integerp 36))
> (test? (integerp "not an integer"))

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

FAILURE

name: check-t

location: eval:17:0

params: '(nil)

--------------------
> (test? (equal (rev (list 789))(list 987)))

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

> (test? (equal (rev (list abc))(list cba)))
> (test? (equal (app (list ab)(list cd))(list abcd)))

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-nx)x)))
> (test? (implies (natp y)(< (sum-ny)(* yy))))

> (test? (implies (natp n)
(equal (sum-nn)
(/ (* n(+ n1))2))))

top ← prev up next →