		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Stmts-formalp

Check if statements and related entities have formal dynamic semantics.

Definitions and Theorems

Function: stmt-formalp

(defun stmt-formalp (stmt)
  (declare (xargs :guard (stmtp stmt)))
  (declare (xargs :guard (stmt-unambp stmt)))
  (let ((__function__ 'stmt-formalp))
    (declare (ignorable __function__))
    (stmt-case stmt
               :labeled nil
               :compound (comp-stmt-formalp stmt.stmt)
               :expr (or (not stmt.expr?)
                         (expr-formalp stmt.expr?))
               :if (and (expr-formalp stmt.test)
                        (stmt-formalp stmt.then))
               :ifelse (and (expr-formalp stmt.test)
                            (stmt-formalp stmt.then)
                            (stmt-formalp stmt.else))
               :switch nil
               :while (and (expr-formalp stmt.test)
                           (stmt-formalp stmt.body))
               :dowhile (and (stmt-formalp stmt.body)
                             (expr-formalp stmt.test))
               :for-expr nil
               :for-decl nil
               :for-ambig (impossible)
               :goto nil
               :gotoe nil
               :continue nil
               :break nil
               :return (or (not stmt.expr?)
                           (expr-formalp stmt.expr?))
               :asm nil)))

Function: comp-stmt-formalp

(defun comp-stmt-formalp (cstmt)
  (declare (xargs :guard (comp-stmtp cstmt)))
  (declare (xargs :guard (comp-stmt-unambp cstmt)))
  (let ((__function__ 'comp-stmt-formalp))
    (declare (ignorable __function__))
    (b* (((comp-stmt cstmt) cstmt))
      (and (not cstmt.labels)
           (block-item-list-formalp cstmt.items)))))

Function: block-item-formalp

(defun block-item-formalp (item)
  (declare (xargs :guard (block-itemp item)))
  (declare (xargs :guard (block-item-unambp item)))
  (let ((__function__ 'block-item-formalp))
    (declare (ignorable __function__))
    (block-item-case item
                     :decl (decl-block-formalp item.decl)
                     :stmt (stmt-formalp item.stmt)
                     :ambig (impossible))))

Function: block-item-list-formalp

(defun block-item-list-formalp (items)
  (declare (xargs :guard (block-item-listp items)))
  (declare (xargs :guard (block-item-list-unambp items)))
  (let ((__function__ 'block-item-list-formalp))
    (declare (ignorable __function__))
    (or (endp items)
        (and (block-item-formalp (car items))
             (block-item-list-formalp (cdr items))))))

Theorem: return-type-of-stmt-formalp.yes/no

(defthm return-type-of-stmt-formalp.yes/no
  (b* ((?yes/no (stmt-formalp stmt)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-comp-stmt-formalp.yes/no

(defthm return-type-of-comp-stmt-formalp.yes/no
  (b* ((?yes/no (comp-stmt-formalp cstmt)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-formalp.yes/no

(defthm return-type-of-block-item-formalp.yes/no
  (b* ((?yes/no (block-item-formalp item)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-list-formalp.yes/no

(defthm return-type-of-block-item-list-formalp.yes/no
  (b* ((?yes/no (block-item-list-formalp items)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: stmt-formalp-of-stmt-fix-stmt

(defthm stmt-formalp-of-stmt-fix-stmt
  (equal (stmt-formalp (stmt-fix stmt))
         (stmt-formalp stmt)))

Theorem: comp-stmt-formalp-of-comp-stmt-fix-cstmt

(defthm comp-stmt-formalp-of-comp-stmt-fix-cstmt
  (equal (comp-stmt-formalp (comp-stmt-fix cstmt))
         (comp-stmt-formalp cstmt)))

Theorem: block-item-formalp-of-block-item-fix-item

(defthm block-item-formalp-of-block-item-fix-item
  (equal (block-item-formalp (block-item-fix item))
         (block-item-formalp item)))

Theorem: block-item-list-formalp-of-block-item-list-fix-items

(defthm block-item-list-formalp-of-block-item-list-fix-items
  (equal (block-item-list-formalp (block-item-list-fix items))
         (block-item-list-formalp items)))

Theorem: stmt-formalp-stmt-equiv-congruence-on-stmt

(defthm stmt-formalp-stmt-equiv-congruence-on-stmt
  (implies (stmt-equiv stmt stmt-equiv)
           (equal (stmt-formalp stmt)
                  (stmt-formalp stmt-equiv)))
  :rule-classes :congruence)

Theorem: comp-stmt-formalp-comp-stmt-equiv-congruence-on-cstmt

(defthm comp-stmt-formalp-comp-stmt-equiv-congruence-on-cstmt
  (implies (comp-stmt-equiv cstmt cstmt-equiv)
           (equal (comp-stmt-formalp cstmt)
                  (comp-stmt-formalp cstmt-equiv)))
  :rule-classes :congruence)

Theorem: block-item-formalp-block-item-equiv-congruence-on-item

(defthm block-item-formalp-block-item-equiv-congruence-on-item
  (implies (block-item-equiv item item-equiv)
           (equal (block-item-formalp item)
                  (block-item-formalp item-equiv)))
  :rule-classes :congruence)

Theorem: block-item-list-formalp-block-item-list-equiv-congruence-on-items

(defthm
  block-item-list-formalp-block-item-list-equiv-congruence-on-items
  (implies (block-item-list-equiv items items-equiv)
           (equal (block-item-list-formalp items)
                  (block-item-list-formalp items-equiv)))
  :rule-classes :congruence)

Subtopics

Stmt-formalp: Check if a statement has formal dynamic semantics.
Block-item-list-formalp: Check if a list of block items have formal dynamic semantics.
Block-item-formalp: Check if a block item has formal dynamic semantics.
Comp-stmt-formalp: Check if a compound statement has formal dynamic semantics.