← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2004/legato/support/generic-theories.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2004/legato/support/generic-theories.lisp
 
1
;;; This file contains a collection of theories useful for reasoning about
 
2
;;; instantiated weakest preconditions.
 
3
 
 
4
;;; A generic theory for using loop invariants to prove weakest preconditions.
 
5
 
 
6
;;; (wp s) = (if (b s) (qp s) (wp (sigma s)))
 
7
 
 
8
;;; (not (b s)) ^ (r s) => (r (sigma s))
 
9
;;; (b s) ^ (r s) => (qp s)
 
10
 
 
11
(in-package "ACL2")
 
12
 
 
13
(encapsulate
 
14
 (((measure *) => *)
 
15
  ((sigma *) => *)
 
16
  ((b *) => *)
 
17
  ((qp *) => *)
 
18
  ((wp *) => *)
 
19
  ((r *) => *))
 
20
 (local (defun measure (s) (1+ (nfix (car s)))))
 
21
 (local (defun sigma (s) (cons (1- (car s)) (cdr s))))
 
22
 (local (defun b (s) (zp (car s))))
 
23
 (local (defun qp (s) (declare (ignore s)) t))
 
24
 (local (defun wp (s) (declare (ignore s)) t))
 
25
 (local (defun r (s) (declare (ignore s)) t))
 
26
 (defthm loop-invariant-wp-def-1
 
27
   (implies (b s) (equal (wp s) (qp s))))
 
28
 (defthm loop-invariant-wp-def-2
 
29
   (implies (and (not (b s)) (r s)) (equal (wp (sigma s)) (wp s))))
 
30
 (defthm loop-invariant-ordinalp (o-p (measure s)))
 
31
 (defthm loop-invariant-ord-<
 
32
   (implies (not (b s)) (o< (measure (sigma s)) (measure s))))
 
33
 (defthm loop-invariant-r-1
 
34
   (implies (and (not (b s)) (r s)) (r (sigma s))))
 
35
 (defthm loop-invariant-r-2
 
36
   (implies (and (b s) (r s)) (qp s))))
 
37
 
 
38
;;; An induct hint
 
39
 
 
40
(defun wp-ind (s)
 
41
  (declare (xargs :measure (measure s)))
 
42
  (if (b s) (qp s) (wp-ind (sigma s))))
 
43
 
 
44
;;; The main result derived from the loop-invariant theory.
 
45
 
 
46
(defthm wp-is-weakest-invariant
 
47
  (implies (r s) (wp s))
 
48
  :hints (("Goal"
 
49
           :induct (wp-ind s))))
 
50
 
 
51
;;; A generic theory for conversion of tail to primitive recursive functions.
 
52
 
 
53
;;; (g a s) = (if (bb s) (qt a s) (g (rho a s) (tau s)))
 
54
;;; (h s) = (if (bb s) (id) (rhoh (h (tau s)) s))
 
55
;;; (rt a s) is an invariant which assures desired properties of rho, op and (id)
 
56
;;; (hs s) = (if (bb s) s (hs (tau s))), computes a bottom object under tau
 
57
 
 
58
;(set-bind-free-error nil)
 
59
 
 
60
(encapsulate
 
61
 (((measure-g *) => *)
 
62
  ((tau *) => *)
 
63
  ((rt * *) => *)
 
64
  ((rho * *) => *)
 
65
  ((rhoh * *) => *)
 
66
  ((bb *) => *)
 
67
  ((qt * *) => *)
 
68
  ((g * *) => *)
 
69
  ((h *) => *)
 
70
  ((id) => *)
 
71
  ((op * * *) => *)
 
72
  ((hs *) => *))
 
73
 (local (defun measure-g (s) (1+ (nfix s))))
 
74
 (local (defun tau (s) (1- (nfix s))))
 
75
 (local (defun qt (a s) (declare (ignore a s)) t))
 
76
 (local (defun rho (a s) (declare (ignore a s)) 0))
 
77
 (local (defun rhoh (a s) (declare (ignore a s)) 0))
 
78
 (local (defun bb (s) (zp s)))
 
79
 (local (defun g (a s) (declare (ignore a s)) t))
 
80
 (local (defun id () 0))
 
81
 (local (defun op (a x s) (if (and (zp s) (equal x 0)) a 0)))
 
82
 (local (defun h (s) (declare (ignore s)) 0))
 
83
 (local (defun rt (a s) (and (integerp a) (integerp s) (<= 0 a) (<= 0 s))))
 
84
 (local (defun hs (s) (if (zp s) s 0)))
 
85
 (defthm tail-recursion-g-def-1
 
86
   (implies (and (bb s) (rt a s)) (equal (g a s) (qt a s))))
 
87
 (defthm tail-recursion-g-def-2
 
88
   (implies (and (not (bb s)) (rt a s)) (equal (g (rho a s) (tau s)) (g a s))))
 
89
 (defthm tail-recursion-ordinalp
 
90
   (o-p (measure-g s)))
 
91
 (defthm tail-recursion-ord-<
 
92
   (implies (not (bb s))
 
93
            (o< (measure-g (tau s)) (measure-g s))))
 
94
 (defthm tail-recursion-h-def-1
 
95
   (implies (and (bb s) (rt a s)) (equal (h s) (id))))
 
96
 (defthm tail-recursion-h-def-2
 
97
   (implies (and (not (bb s)) (rt a s)) (equal (rhoh (h (tau s)) s) (h s))))
 
98
 (defthm tail-recursion-rt
 
99
   (implies (and (not (bb s)) (rt a s))
 
100
            (rt (rho a s) (tau s))))
 
101
 (defthm tail-recursion-hs-1
 
102
   (implies (bb s) (equal (hs s) s)))
 
103
 (defthm tail-recursion-hs-2
 
104
   (implies (not (bb s)) (equal (hs (tau s)) (hs s))))
 
105
 (defthm tail-recursion-op-rho-rhoh  ; generated by proof of a-g-as-op-h
 
106
   (implies (and (not (bb s)) (rt a s))
 
107
            (equal (op (rho a s) (h (tau s)) (tau s))
 
108
                   (op a (rhoh (h (tau s)) s) s))))
 
109
 (defthm tail-recursion-op-id  ; generated by proof of a-g-as-op-h
 
110
   (implies (and (bb s) (rt a s))
 
111
            (equal (op a (id) s) a))))
 
112
 
 
113
(defun a-g (a s)
 
114
  (declare (xargs :measure (measure-g s)))
 
115
  (if (bb s)
 
116
      a
 
117
    (a-g (rho a s) (tau s))))
 
118
 
 
119
(defthm a-g-as-op-h
 
120
  (implies (rt a s)
 
121
           (equal (a-g a s)
 
122
                  (op a (h s) s)))
 
123
  :hints (("Goal"
 
124
           :induct (a-g a s))))
 
125
 
 
126
(defthm g-as-a-g
 
127
  (implies (rt a s)
 
128
           (equal (g a s) (qt (a-g a s) (hs s))))
 
129
  :hints (("Goal"
 
130
           :induct (a-g a s))))
 
131
 
 
132
;;; Main result of tail recursion theory
 
133
 
 
134
(defthm g=h
 
135
  (implies (rt a s)
 
136
           (equal (g a s)
 
137
                  (if (bb s)
 
138
                      (qt a s)
 
139
                    (qt (op a (h s) s) (hs s)))))
 
140
  :hints (("Goal"
 
141
           :induct (a-g a s))))
 
142
 
 
143
;;; The following theory can be used to prove equivalence, under the hypothesis
 
144
;;; p, between alternative representations fn1 and fn2 of the same function
 
145
;;; or in developing induction patterns different from that suggested by the
 
146
;;; standard definition.  The function id-alt below has dual roles.  When proving
 
147
;;; equivalence between fn1 and fn1, id-alt is the identity function.  Otherwise it
 
148
;;; represents the alternative induction.  In this latter case sigma1 = sigma2.
 
149
;;;
 
150
;;;      (fn1 s) = (if (b1 s) (q1 s) (fn1 (sigma1 s)))
 
151
;;;      (fn2 s) = (if (b2 s) (q2 s) (fn2 (sigma2 s)))
 
152
 
 
153
(encapsulate
 
154
 (((fn1 *) => *)
 
155
  ((fn2 *) => *)
 
156
  ((b1 *) => *)
 
157
  ((b2 *) => *)
 
158
  ((q1 *) => *)
 
159
  ((q2 *) => *)
 
160
  ((p *) => *)
 
161
  ((measure1 *) => *)
 
162
  ((sigma1 *) => *)
 
163
  ((sigma2 *) => *)
 
164
  ((id-alt *) => *))
 
165
 (local (defun fn1 (s) (declare (ignore s)) t))
 
166
 (local (defun fn2 (s) (declare (ignore s)) t))
 
167
 (local (defun b1 (s) (zp (car s))))
 
168
 (local (defun b2 (s) (zp (cdr s))))
 
169
 (local (defun q1 (s) (declare (ignore s)) t))
 
170
 (local (defun q2 (s) (declare (ignore s)) t))
 
171
 (local (defun p (s) (declare (ignore s)) t))
 
172
 (local (defun measure1 (s) (1+ (nfix (car s)))))
 
173
 (local (defun sigma1 (s) (cons (1- (nfix (car s))) (cdr s))))
 
174
 (local (defun sigma2 (s) (cons (car s) (1- (nfix (cdr s))))))
 
175
 (local (defun id-alt (s) (cons (cdr s) (car s))))
 
176
 (defthm alternative-induction-fn1-def-1
 
177
   (implies (b1 s) (equal (fn1 s) (q1 s))))
 
178
 (defthm alternative-induction-fn1-def-2
 
179
   (implies (and (not (b1 s)) (p s)) (equal (fn1 (sigma1 s)) (fn1 s))))
 
180
 (defthm alternative-induction-fn2-def-1
 
181
   (implies (b2 s) (equal (fn2 s) (q2 s))))
 
182
 (defthm alternative-induction-fn2-def-2
 
183
   (implies (not (b2 s)) (equal (fn2 (sigma2 s)) (fn2 s))))
 
184
 (defthm alternative-induction-ordinalp
 
185
   (o-p (measure1 s)))
 
186
 (defthm alternative-induction-ord-<
 
187
   (implies (not (b1 s)) (o< (measure1 (sigma1 s)) (measure1 s))))
 
188
 (defthm alternative-induction-id-alt
 
189
   (implies (and (p s) (not (b1 s)))
 
190
            (equal (id-alt (sigma1 s)) (sigma2 (id-alt s)))))
 
191
 (defthm alternative-induction-b2-id-alt
 
192
   (implies (p s) (equal (b2 (id-alt s)) (b1 s))))
 
193
 (defthm alternative-induction-p
 
194
   (implies (and (not (b1 s)) (p s)) (p (sigma1 s))))
 
195
 (defthm alternative-induction-q2-id-alt
 
196
   (implies (and (b1 s) (p s)) (equal (q2 (id-alt s)) (q1 s)))))
 
197
  
 
198
(defun fn1-ind (s)
 
199
  (declare (xargs :measure (measure1 s)))
 
200
  (if (b1 s) (q1 s) (fn1-ind (sigma1 s))))
 
201
 
 
202
;;; This is the main goal of the alternative induction theory.
 
203
 
 
204
(defthm fn1-as-fn2 
 
205
  (implies (p s)
 
206
           (equal (fn1 s) (fn2 (id-alt s))))
 
207
  :hints (("Goal" :induct (fn1-ind s))))
 
208
 
 
209
;;; Define computed hint function for loop invariant theory
 
210
 
 
211
;;; Create a substitution that maps ith formal argument to (nth i s).
 
212
 
 
213
(defun make-subs (formals i)
 
214
  (declare (xargs :mode :program))
 
215
  (if (endp formals)
 
216
      nil
 
217
    (cons (cons (car formals) `(nth ,i s))
 
218
          (make-subs (cdr formals) (+ 1 i)))))
 
219
 
 
220
;;; Converts a set of arguments to a proper logical expression using the operator op.
 
221
 
 
222
(defun set-to-predicate (a op)
 
223
  (if (< (length a) 2)
 
224
      (car a)
 
225
    (cons op a)))
 
226
 
 
227
;;; Extract the predicate b from the induction-machine property of wp.
 
228
 
 
229
(defun make-b (induction-machine)
 
230
    (declare (xargs :mode :program))
 
231
    (if (endp induction-machine)
 
232
        nil
 
233
      (if (and (equal (caar induction-machine) 'tests-and-calls)
 
234
               (endp (cddar induction-machine))) ; detects base case predicates
 
235
          (cons (set-to-predicate (cadar induction-machine) 'and)
 
236
                (make-b (cdr induction-machine)))
 
237
        (make-b (cdr induction-machine)))))
 
238
 
 
239
;;; Construct the argument for a cond expression that delivers an instance of the
 
240
;;; generic substitution sigma.  flat-to-s is the substitution generated by make-subs.
 
241
 
 
242
(defun make-sigma (induction-machine flat-to-s)
 
243
    (declare (xargs :mode :program))
 
244
    (if (endp induction-machine)
 
245
        (list (list t 's)) ; default value of cond
 
246
      (if (and (equal (caar induction-machine) 'tests-and-calls)
 
247
               (consp (cddar induction-machine)))
 
248
          (cons (sublis flat-to-s
 
249
                        (list (set-to-predicate (cadar induction-machine) 'and)
 
250
                              (cons 'list (cdaddr (car induction-machine)))))
 
251
                (make-sigma (cdr induction-machine) flat-to-s))
 
252
        (make-sigma (cdr induction-machine) flat-to-s))))
 
253
 
 
254
(defun build-instance (wp r world)
 
255
  (declare (xargs :mode :program))
 
256
  (let* ((formals
 
257
          (getprop wp 'formals nil '*current-acl2-world* world))
 
258
         (flat-to-s ; mapping from flat to structured state space
 
259
          (cons (cons wp 'list) (make-subs formals 0))))
 
260
    `(:use
 
261
      (:instance
 
262
       (:functional-instance
 
263
        wp-is-weakest-invariant
 
264
        (b (lambda (s) ,(set-to-predicate
 
265
                         (sublis
 
266
                          flat-to-s
 
267
                          (make-b (getprop wp
 
268
                                           'induction-machine
 
269
                                           nil
 
270
                                           '*current-acl2-world*
 
271
                                           world)))
 
272
                          'or)))
 
273
        (qp (lambda (s) (,wp ,@(sublis flat-to-s
 
274
                                       (getprop wp
 
275
                                                'formals
 
276
                                                nil
 
277
                                                '*current-acl2-world*
 
278
                                                world)))))
 
279
        (wp (lambda (s) (,wp  ,@(sublis flat-to-s
 
280
                                       (getprop wp
 
281
                                                'formals
 
282
                                                nil
 
283
                                                '*current-acl2-world*
 
284
                                                world)))))
 
285
; This is probably incomplete.  What is the purpose of the repetition of
 
286
; "justification" within the 'justification property?
 
287
        (measure (lambda (s) ,(sublis flat-to-s
 
288
; Matt K. mod after Version 3.0.1: Replace (car (cddddr (getprop ...))) so that
 
289
; we access justification property without relying on its layout.
 
290
                                      (let ((j (getprop wp
 
291
                                                        'justification
 
292
                                                        nil
 
293
                                                        '*current-acl2-world*
 
294
                                                        world)))
 
295
                                        (and j (access justification
 
296
                                                       j
 
297
                                                       :measure))))))
 
298
          (sigma (lambda (s) (cond ,@(make-sigma (getprop wp
 
299
                                                          'induction-machine
 
300
                                                          nil
 
301
                                                          '*current-acl2-world*
 
302
                                                          world)
 
303
                                                 flat-to-s))))
 
304
          (r (lambda (s) ,(sublis flat-to-s r))))
 
305
       (s (list ,@(getprop wp
 
306
                           'formals
 
307
                           nil
 
308
                           '*current-acl2-world*
 
309
                           world)))))))
 
310
 
 
311
(defmacro loop-invariant-hint (wp r)
 
312
  `(build-instance ,wp ,r world))
 
313
 
 
314
;;; A user will include (loop-invariant wp r) within the :hints field of a defthm,
 
315
;;; where wp and r are concrete instances of the weakest precondition and loop
 
316
;;; invariant respectively.  For example
 
317
 
 
318
;;; (defthm foo
 
319
;;;  (implies <insert concrete loop invariant here>
 
320
;;;           <insert concrete weakest precondition here>)
 
321
;;;  :hints
 
322
;;;   ((loop-invariant-hint
 
323
;;;     '<name of concrete weakest precondition>
 
324
;;;     '<concrete loop invariant>)))
 
325