		Search-engine friendly clone of the ACL2 documentation.

Variable-visibility-preservation

Var-visible-preservep-of-exec

Preservation of variable visibility under execution, for any number of peeled frames and scopes.

We prove by induction that var-visible-preservep holds between each computation state before execution and the computation state after execution.

Definitions and Theorems

Theorem: var-visible-preservep-of-exec-fun

(defthm var-visible-preservep-of-exec-fun
  (b* (((mv result compst1)
        (exec-fun fun args compst fenv limit)))
    (implies (not (errorp result))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-expr

(defthm var-visible-preservep-of-exec-expr
  (b* (((mv result compst1)
        (exec-expr e compst fenv limit)))
    (implies (not (errorp result))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-stmt

(defthm var-visible-preservep-of-exec-stmt
  (b* (((mv result compst1)
        (exec-stmt s compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-stmt-while

(defthm var-visible-preservep-of-exec-stmt-while
  (b* (((mv result compst1)
        (exec-stmt-while test body compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-stmt-dowhile

(defthm var-visible-preservep-of-exec-stmt-dowhile
  (b* (((mv result compst1)
        (exec-stmt-dowhile body test compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-initer

(defthm var-visible-preservep-of-exec-initer
  (b* (((mv result compst1)
        (exec-initer initer compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-obj-declon

(defthm var-visible-preservep-of-exec-obj-declon
  (b* ((compst1 (exec-obj-declon declon compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp compst1)))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-block-item

(defthm var-visible-preservep-of-exec-block-item
  (b* (((mv result compst1)
        (exec-block-item item compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-visible-preservep compst compst1))))

Theorem: var-visible-preservep-of-exec-block-item-list

(defthm var-visible-preservep-of-exec-block-item-list
  (b* (((mv result compst1)
        (exec-block-item-list items compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-visible-preservep compst compst1))))