		Search-engine friendly clone of the ACL2 documentation.

Semantics

Step

Semantics of Imp commands.

Signature
(step cfg) → new-cfg
Arguments: cfg — Guard (configp cfg).
Returns: new-cfg — Type (configp new-cfg).

According to the guard, this is defined only if there are commands in the configuration, i.e. there is something to do. Otherwise, execution is in a terminated state.

A step consists in taking the first command in the configuration and executing it. This may modify the environment, and the list of the commands in the configuration.

An assignment is executed by evaluating the expression and writing the obtained value into the variable. The assignment command is removed from the configuration, because it is completely executed.

A conditional is executed by evaluating the condition first. Based on the obtained value, the conditional is replaced by one of its branches. This means that conditionals are non-strict in Imp: the other branch is eliminated, not executed.

A loop is executed by evaluating the condition first. If it is false, the loop command is removed from the configuration: the loop is completely executed in this case. If the condition is true instead, the loop body is added in front of the command list in the configuration, without removing the loop command itself: since the loop condition is true, we need to execute the body at least one more time, and then we need to execute the loop as a whole again, i.e. re-evaluate the condition (generally in a different environment).

This step function is executable.

Definitions and Theorems

Function: step

(defun step (cfg)
  (declare (xargs :guard (configp cfg)))
  (declare (xargs :guard (consp (config->comms cfg))))
  (b* ((comms (config->comms cfg))
       (env (config->env cfg))
       ((unless (mbt (consp comms)))
        (config-fix cfg))
       (comm (car comms)))
    (comm-case comm :asg
               (b* ((var comm.var)
                    (val (aeval comm.exp env))
                    (new-env (write-var var val env))
                    (new-comms (cdr comms)))
                 (make-config :comms new-comms
                              :env new-env))
               :if
               (b* ((cond (beval comm.cond env))
                    (new-comms (append (if cond comm.then comm.else)
                                       (cdr comms))))
                 (make-config :comms new-comms :env env))
               :while
               (b* ((cond (beval comm.cond env))
                    (new-comms (if cond (append comm.body comms)
                                 (cdr comms))))
                 (make-config :comms new-comms
                              :env env)))))

Theorem: configp-of-step

(defthm configp-of-step
  (b* ((new-cfg (step cfg)))
    (configp new-cfg))
  :rule-classes :rewrite)

Theorem: step-of-config-fix-cfg

(defthm step-of-config-fix-cfg
  (equal (step (config-fix cfg))
         (step cfg)))

Theorem: step-config-equiv-congruence-on-cfg

(defthm step-config-equiv-congruence-on-cfg
  (implies (config-equiv cfg cfg-equiv)
           (equal (step cfg) (step cfg-equiv)))
  :rule-classes :congruence)