1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
; Event-Level Assertions -- Tests
;
; Copyright (C) 2017 Kestrel Institute (http://www.kestrel.edu)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Authors:
; Matt Kaufmann (kaufmann@cs.utexas.edu)
; Alessandro Coglio (coglio@kestrel.edu)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "std/testing/assert" :dir :system)
(include-book "std/testing/eval" :dir :system)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(local
(progn
(assert! (equal 3 3)
(defun assert-test1 (x) x))
; Check that above defun was evaluated.
(value-triple (or (equal (assert-test1 3) 3)
(er hard 'top-level
"Failed to evaluate (assert-test1 3) to 3.")))))
(local
(progn
(must-fail
(assert! (equal 3 4)
(defun assert-test2 (x) x)))
; Check that above defun was not evaluated.
(defun assert-test2 (x)
(cons x x))))
; Simple test with no second argument:
(assert! (equal (append '(a b c) '(d e f))
'(a b c d e f)))
; Check failure of assertion when condition is false:
(local
(must-fail
(assert! (equal (append '(a b c) '(d e f))
'(a b)))))
; The following requires that this book be certified in the initial
; certification world, unless an acl2-customization file has been supplied. It
; also succeeds at include-book time even if we include the book after
; executing another command, because assert! uses make-event with
; :check-expansion nil. See assert-include.lisp.
; HOWEVER....
; This book is no longer certified in the initial certification world during
; regressions, because cert.pl causes LD of books/xdoc/top.port and also, in
; the current directory, eval.port. So we comment out the following form.
; (local (make-event
; (er-let* ((c (getenv$ "ACL2_CUSTOMIZATION" state)))
; (value
; (if (and c (not (equal c "NONE")))
; `(value-triple
; (cw "SKIPPING due to ACL2_CUSTOMIZATION=~x0~%" ,c))
; '(assert! (equal (access-command-tuple-form
; (cddr (car (scan-to-command (w state)))))
; '(exit-boot-strap-mode))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Test-stobj example from David Rager.
(local
(encapsulate
()
(defstobj foo field1 field2)
(defun test-stobj (x foo)
(declare (xargs :stobjs foo))
(let ((foo (update-field1 17 foo)))
(update-field2 x foo)))
; Passes.
(assert!-stobj (let* ((foo (test-stobj 14 foo)))
(mv (equal (field1 foo)
17)
foo))
foo)
(must-fail
(assert!-stobj (let* ((foo (test-stobj 14 foo)))
(mv (equal (field1 foo)
14)
foo))
foo))
))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(must-succeed*
(defun f (x) (cons x x))
(assert-equal (f 3) '(3 . 3)))
(must-fail
(assert-equal 1 2))
|
