File: certify.lsp

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (45 lines) | stat: -rw-r--r-- 1,219 bytes parent folder | download
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
#|

 certify.lsp
 ~~~~~~~~~~~

This script file certifies all the books for proving the equivalence between
clock functions and inductive invariants in ACL2. 

The set of books here is (hopefully) well documented. For further details about
the books the reader is encouraged to look at the following paper on the
subject.

1. S. Ray and J S. Moore. Proof Styles in Operational Semantics. In A. J. Hu
   and A. K. Martin, editors, Proceedings of the 5th International Conference
   on Formal Methods in Computer-Aided Design (FMCAD 2004), volume 3312 of LNCS,
   Nov 2004, pages 67-81. Springer-Verlag.

|#


(set-inhibit-output-lst '(proof-tree prove))

(ubt! 1)

;; The directory i2c contains the set of books that show how to transform
;; inductive invariant proofs to clock function proofs. 
(set-cbd "i2c")
(ld "certify-i2c.lsp")

(set-cbd "..")

;; The directory c2i contains the set of books that show how to transform clock
;; function proofs to inductive invariants.
(set-cbd "c2i")
(ld "certify-c2i.lsp")

(set-cbd "..")

;; Finally the directory compose contains the books for composition of proofs.
(set-cbd "compose")
(ld "certify-compose.lsp")

(set-cbd "..")

(set-inhibit-output-lst '(proof-tree prove))