← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/concurrent-programs/bakery/initial-state.lisp

  • 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/initial-state.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
#|
 
4
 
 
5
  initial-state.lisp
 
6
  ~~~~~~~~~~~~~~~~~~
 
7
 
 
8
In this book, we define an encapsulated function, initial-state, and show that
 
9
the invariant inv holds for that state. Thus our stuttering bisimulation will
 
10
claim that there exists an initial state such that if you run the program from
 
11
that state then the execution of the program matches the spec upto finite
 
12
stuttering.
 
13
 
 
14
|#
 
15
 
 
16
(include-book "programs")
 
17
(include-book "properties")
 
18
 
 
19
 
 
20
;; BEGIN Proofs of theorems.
 
21
 
 
22
(encapsulate 
 
23
 (((initial-state-b) => *))
 
24
 
 
25
  (local
 
26
   (defun initial-state-b ()
 
27
     (>_ :procs nil
 
28
         :queue nil
 
29
         :bucket nil
 
30
         :maxval 0))
 
31
   )
 
32
 
 
33
  (local
 
34
   (defun initial-state-c ()
 
35
     nil)
 
36
   )
 
37
 
 
38
  (DEFTHM inv-b-c-initial-state->>
 
39
    (inv-b-c (initial-state-b))
 
40
    :rule-classes nil)
 
41
 
 
42
  (DEFTHM fair-inv-b-c-initial-state->>
 
43
    (fair-inv-b-c (initial-state-b))
 
44
    :rule-classes nil)
 
45
  
 
46
  (DEFTHM inv-c-s-rep-initial-state->>
 
47
    (inv-c-s (rep-c-s (initial-state-b)))
 
48
    :rule-classes nil)
 
49
 
 
50
)
 
51