		Search-engine friendly clone of the ACL2 documentation.

Semantics

Aeval

Semantics of Imp arithmetic expressions.

Signature
(aeval exp env) → int
Arguments: exp — Guard (aexpp exp).; env — Guard (envp env).
Returns: int — Type (integerp int).

This is formalized via an evaluation function that maps an arithmetic expression and an envionment to an integer. The integer is the value of the expression given the environment.

The (recursive) evaluation of Imp's arithmetic expressions always terminates.

This evaluation function is executable.

Definitions and Theorems

Function: aeval

(defun aeval (exp env)
  (declare (xargs :guard (and (aexpp exp) (envp env))))
  (aexp-case exp
             :const exp.value
             :var (read-var exp.name env)
             :add (+ (aeval exp.left env)
                     (aeval exp.right env))
             :mul (* (aeval exp.left env)
                     (aeval exp.right env))))

Theorem: integerp-of-aeval

(defthm integerp-of-aeval
  (b* ((int (aeval exp env)))
    (integerp int))
  :rule-classes :rewrite)

Theorem: aeval-of-aexp-fix-exp

(defthm aeval-of-aexp-fix-exp
  (equal (aeval (aexp-fix exp) env)
         (aeval exp env)))

Theorem: aeval-aexp-equiv-congruence-on-exp

(defthm aeval-aexp-equiv-congruence-on-exp
  (implies (aexp-equiv exp exp-equiv)
           (equal (aeval exp env)
                  (aeval exp-equiv env)))
  :rule-classes :congruence)

Theorem: aeval-of-env-fix-env

(defthm aeval-of-env-fix-env
  (equal (aeval exp (env-fix env))
         (aeval exp env)))

Theorem: aeval-env-equiv-congruence-on-env

(defthm aeval-env-equiv-congruence-on-env
  (implies (env-equiv env env-equiv)
           (equal (aeval exp env)
                  (aeval exp env-equiv)))
  :rule-classes :congruence)