		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-expr-when-asg-ident-rules

Rules for executing assignment expressions to identifier expressions.

The first one is used in the large symbolic execution.

The second one is for the new modular proof approach.

Definitions and Theorems

Theorem: exec-expr-when-asg-ident

(defthm exec-expr-when-asg-ident
  (implies (and (syntaxp (quotep expr))
                (not (zp limit))
                (equal (expr-kind expr) :binary)
                (equal (binop-kind (expr-binary->op expr))
                       :asg)
                (equal left (expr-binary->arg1 expr))
                (equal right (expr-binary->arg2 expr))
                (equal (expr-kind left) :ident)
                (equal var (expr-ident->get left))
                (equal oldval (read-var var compst))
                (valuep oldval)
                (not (equal (value-kind oldval) :array))
                (equal eval+compst1
                       (exec-expr right compst fenv (1- limit)))
                (equal eval (mv-nth 0 eval+compst1))
                (equal compst1 (mv-nth 1 eval+compst1))
                (expr-valuep eval)
                (equal eval1 (apconvert-expr-value eval))
                (expr-valuep eval1)
                (equal newval (expr-value->value eval1))
                (equal compst2 (write-var var newval compst1))
                (compustatep compst2))
           (equal (exec-expr expr compst fenv limit)
                  (mv (expr-value newval nil) compst2))))

Theorem: exec-expr-when-asg-ident-via-object

(defthm exec-expr-when-asg-ident-via-object
  (implies (and (syntaxp (quotep expr))
                (not (zp limit))
                (equal (expr-kind expr) :binary)
                (equal (binop-kind (expr-binary->op expr))
                       :asg)
                (equal left (expr-binary->arg1 expr))
                (equal right (expr-binary->arg2 expr))
                (equal (expr-kind left) :ident)
                (equal objdes
                       (objdesign-of-var (expr-ident->get left)
                                         compst))
                objdes
                (not (equal (value-kind (read-object objdes compst))
                            :array))
                (equal eval+compst1
                       (exec-expr right compst fenv (1- limit)))
                (equal eval (mv-nth 0 eval+compst1))
                (equal compst1 (mv-nth 1 eval+compst1))
                (expr-valuep eval)
                (equal eval1 (apconvert-expr-value eval))
                (expr-valuep eval1)
                (equal val (expr-value->value eval1))
                (equal compst2
                       (write-object objdes val compst1))
                (compustatep compst2))
           (equal (exec-expr expr compst fenv limit)
                  (mv (expr-value val nil) compst2))))