Chek if statements and blocks have formal dynamic semantics.
Function:
(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 (block-item-list-formalp stmt.items) :expr (and stmt.expr? (or (expr-call-formalp stmt.expr?) (expr-asg-formalp stmt.expr?))) :if (and (expr-pure-formalp stmt.test) (stmt-formalp stmt.then)) :ifelse (and (expr-pure-formalp stmt.test) (stmt-formalp stmt.then) (stmt-formalp stmt.else)) :switch nil :while (and (expr-pure-formalp stmt.test) (stmt-formalp stmt.body)) :dowhile nil :for-expr nil :for-decl nil :for-ambig (impossible) :goto nil :continue nil :break nil :return (or (not stmt.expr?) (expr-call-formalp stmt.expr?) (expr-pure-formalp stmt.expr?)))))
Function:
(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.unwrap) :stmt (stmt-formalp item.unwrap) :ambig (impossible))))
Function:
(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:
(defthm return-type-of-stmt-formalp.yes/no (b* ((?yes/no (stmt-formalp stmt))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-item-formalp.yes/no (b* ((?yes/no (block-item-formalp item))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(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:
(defthm stmt-formalp-of-stmt-fix-stmt (equal (stmt-formalp (stmt-fix stmt)) (stmt-formalp stmt)))
Theorem:
(defthm block-item-formalp-of-block-item-fix-item (equal (block-item-formalp (block-item-fix item)) (block-item-formalp item)))
Theorem:
(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:
(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:
(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:
(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)