		Search-engine friendly clone of the ACL2 documentation.

Semantics

Step*

Exhaustively step from a configuration.

Signature
(step* cfg) → outcome
Arguments: cfg — Guard (configp cfg).
Returns: outcome — Type (outcomep outcome).

If the configuration is terminating, we take the witness number of terminatingp, execute that number of steps, and return the resulting environment. Otherwise, we return the outcome that indicates nontermination.

This, essentially, formalizes a big-step operational semantics.

This function is not executable, because it calls the non-executable function terminatingp.

Definitions and Theorems

Function: step*

(defun step* (cfg)
  (declare (xargs :guard (configp cfg)))
  (if (terminatingp cfg)
      (b* ((n (terminatingp-witness (config-fix cfg)))
           (final-cfg (stepn cfg n))
           (final-env (config->env final-cfg)))
        (outcome-terminated final-env))
    (outcome-nonterminating)))

Theorem: outcomep-of-step*

(defthm outcomep-of-step*
  (b* ((outcome (step* cfg)))
    (outcomep outcome))
  :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)