		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Jstatems+jblocks-count-ifs

Number of ifs in a statement or block.

This is useful as a measure for certain recursive functions.

We prove some theorems about the results of these counting functions. Additional similar theorems could be added as needed.

Definitions and Theorems

Function: jstatem-count-ifs

(defun jstatem-count-ifs (statem)
  (declare (xargs :guard (jstatemp statem)))
  (let ((__function__ 'jstatem-count-ifs))
    (declare (ignorable __function__))
    (jstatem-case statem
                  :locvar 0
                  :expr 0
                  :return 0
                  :throw 0
                  :break 0
                  :continue 0
                  :if (1+ (jblock-count-ifs statem.then))
                  :ifelse (1+ (+ (jblock-count-ifs statem.then)
                                 (jblock-count-ifs statem.else)))
                  :while (jblock-count-ifs statem.body)
                  :do (jblock-count-ifs statem.body)
                  :for (jblock-count-ifs statem.body))))

Function: jblock-count-ifs

(defun jblock-count-ifs (block)
  (declare (xargs :guard (jblockp block)))
  (let ((__function__ 'jblock-count-ifs))
    (declare (ignorable __function__))
    (cond ((endp block) 0)
          (t (+ (jstatem-count-ifs (car block))
                (jblock-count-ifs (cdr block)))))))

Theorem: return-type-of-jstatem-count-ifs.count

(defthm return-type-of-jstatem-count-ifs.count
  (b* ((common-lisp::?count (jstatem-count-ifs statem)))
    (natp count))
  :rule-classes :rewrite)

Theorem: return-type-of-jblock-count-ifs.count

(defthm return-type-of-jblock-count-ifs.count
  (b* ((common-lisp::?count (jblock-count-ifs block)))
    (natp count))
  :rule-classes :rewrite)

Theorem: jblock-count-ifs-of-cons

(defthm jblock-count-ifs-of-cons
  (equal (jblock-count-ifs (cons statem block))
         (+ (jstatem-count-ifs statem)
            (jblock-count-ifs block))))

Theorem: jblock-count-ifs-of-append

(defthm jblock-count-ifs-of-append
  (equal (jblock-count-ifs (append block1 block2))
         (+ (jblock-count-ifs block1)
            (jblock-count-ifs block2))))

Theorem: jstatem-count-ifs-of-return

(defthm jstatem-count-ifs-of-return
  (equal (jstatem-count-ifs (jstatem-return expr?))
         0))

Theorem: jblock-count-ifs-of-jstatem-if->then-decreases

(defthm jblock-count-ifs-of-jstatem-if->then-decreases
  (implies (jstatem-case statem :if)
           (< (jblock-count-ifs (jstatem-if->then statem))
              (jstatem-count-ifs statem)))
  :rule-classes :linear)

Theorem: jblock-count-ifs-of-jstatem-ifelse->then-decreases

(defthm jblock-count-ifs-of-jstatem-ifelse->then-decreases
  (implies (jstatem-case statem :ifelse)
           (< (jblock-count-ifs (jstatem-ifelse->then statem))
              (jstatem-count-ifs statem)))
  :rule-classes :linear)

Theorem: jblock-count-ifs-of-jstatem-ifelse->else-decreases

(defthm jblock-count-ifs-of-jstatem-ifelse->else-decreases
  (implies (jstatem-case statem :ifelse)
           (< (jblock-count-ifs (jstatem-ifelse->else statem))
              (jstatem-count-ifs statem)))
  :rule-classes :linear)

Theorem: jblock-count-ifs-of-take-not-increases

(defthm jblock-count-ifs-of-take-not-increases
  (<= (jblock-count-ifs (take n block))
      (jblock-count-ifs block))
  :rule-classes :linear)

Theorem: jblock-count-ifs-of-nthcdr-not-increases

(defthm jblock-count-ifs-of-nthcdr-not-increases
  (<= (jblock-count-ifs (nthcdr n block))
      (jblock-count-ifs block))
  :rule-classes :linear)

Theorem: jstatem-count-ifs-of-car-not-increases

(defthm jstatem-count-ifs-of-car-not-increases
  (<= (jstatem-count-ifs (car block))
      (jblock-count-ifs block))
  :rule-classes :linear)

Theorem: jblock-count-ifs-of-cdr-not-increases

(defthm jblock-count-ifs-of-cdr-not-increases
  (<= (jblock-count-ifs (cdr block))
      (jblock-count-ifs block))
  :rule-classes :linear)

Theorem: jblock-count-ifs-positive-when-nth-ifelse

(defthm jblock-count-ifs-positive-when-nth-ifelse
  (implies (jstatem-case (nth i block) :ifelse)
           (> (jblock-count-ifs block) 0))
  :rule-classes :linear)

Subtopics

Jstatem-count-ifs
Jblock-count-ifs