← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/concurrent-programs/bakery/certify.lsp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/concurrent-programs/bakery/certify.lsp
 
1
#|
 
2
 
 
3
  certify.lsp
 
4
  ~~~~~~~~~~~
 
5
 
 
6
This file is meant for running the proof of the simplified bakery
 
7
implementation. We decompose our proof into a number of books. Each of the
 
8
books should certify in ACL2 V2.6. The result is a proof of the bakery
 
9
implementation being refinement upto finite stuttering to a simplified model.
 
10
The model is simple enough for it to be obvious that it has all the properties
 
11
we need.  The proof is now a guarantee that the implementation guarantees the
 
12
desired properties.
 
13
 
 
14
Note: We designate all the final theorems and the functions they involve with a
 
15
capital DEFTHM and DEFUN respectively, so that they are easy to identify.
 
16
 
 
17
The theorems we prove are summarized in final-theorems.lisp. This book should
 
18
be a proof that the implementation is a stuttering bisimulation of the
 
19
original.
 
20
 
 
21
Where applicable, (in fact in all the theorems other than >>-stutter2,) we
 
22
prove the corresponding version of the theorem without fairness assumptions. It
 
23
turns out that the fairness is required only in the theorem >>-stutter2, and I
 
24
hope this fact becomes evident in the proof.
 
25
 
 
26
|#
 
27
 
 
28
(set-inhibit-output-lst '(proof-tree prove))
 
29
 
 
30
(ubt! 1)
 
31
 
 
32
(certify-book "total-order")
 
33
(u)
 
34
 
 
35
(certify-book "apply-total-order")
 
36
(u)
 
37
 
 
38
(certify-book "records")
 
39
(u)
 
40
 
 
41
(certify-book "variables")
 
42
(u)
 
43
 
 
44
(certify-book "measures")
 
45
(u)
 
46
 
 
47
(certify-book "fairenv")
 
48
(u)
 
49
 
 
50
(certify-book "lexicographic")
 
51
(u)
 
52
 
 
53
(certify-book "programs")
 
54
(u)
 
55
 
 
56
(certify-book "properties-of-sets")
 
57
(u)
 
58
 
 
59
(certify-book "properties")
 
60
(u)
 
61
 
 
62
(certify-book "initial-state")
 
63
(u)
 
64
 
 
65
(certify-book "labels")
 
66
(u)
 
67
 
 
68
(certify-book "stutter1-match")
 
69
(u)
 
70
 
 
71
(certify-book "pos=1+temp")
 
72
(u)
 
73
 
 
74
(certify-book "lexicographic-pos")
 
75
(u)
 
76
 
 
77
(certify-book "stutter2")
 
78
(u)
 
79
 
 
80
(certify-book "inv-sufficient")
 
81
(u)
 
82
 
 
83
(certify-book "inv-persists")
 
84
 (u)
 
85
 
 
86
(certify-book "final-theorems")
 
87
(u)
 
88
 
 
89
(set-inhibit-output-lst '(proof-tree))
 
90
 
 
91
 
 
92