File: initial-state.lisp

package info (click to toggle)
acl2 7.2dfsg-3
  • links: PTS
  • area: main
  • in suites: stretch
  • size: 198,968 kB
  • ctags: 182,300
  • sloc: lisp: 2,415,261; ansic: 5,675; perl: 5,577; xml: 3,576; sh: 3,255; cpp: 2,835; makefile: 2,440; ruby: 2,402; python: 778; ml: 763; yacc: 709; csh: 355; php: 171; lex: 162; tcl: 44; java: 24; asm: 23; haskell: 17
file content (51 lines) | stat: -rw-r--r-- 1,003 bytes parent folder | download | duplicates (6) 
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
 
(in-package "ACL2")

#|

  initial-state.lisp
  ~~~~~~~~~~~~~~~~~~

In this book, we define an encapsulated function, initial-state, and show that
the invariant inv holds for that state. Thus our stuttering bisimulation will
claim that there exists an initial state such that if you run the program from
that state then the execution of the program matches the spec upto finite
stuttering.

|#

(include-book "programs")
(include-book "properties")


;; BEGIN Proofs of theorems.

(encapsulate
 (((initial-state-b) => *))

  (local
   (defun initial-state-b ()
     (>_ :procs nil
         :queue nil
         :bucket nil
         :maxval 0))
   )

  (local
   (defun initial-state-c ()
     nil)
   )

  (DEFTHM inv-b-c-initial-state->>
    (inv-b-c (initial-state-b))
    :rule-classes nil)

  (DEFTHM fair-inv-b-c-initial-state->>
    (fair-inv-b-c (initial-state-b))
    :rule-classes nil)

  (DEFTHM inv-c-s-rep-initial-state->>
    (inv-c-s (rep-c-s (initial-state-b)))
    :rule-classes nil)

)