		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Jstatems+jblocks-methods

Method names in a statement or block.

We return all the methods names in expressions.

Definitions and Theorems

Function: jstatem-methods

(defun jstatem-methods (statem)
 (declare (xargs :guard (jstatemp statem)))
 (let ((__function__ 'jstatem-methods))
  (declare (ignorable __function__))
  (jstatem-case
    statem
    :locvar nil
    :expr (jexpr-methods statem.get)
    :return (and statem.expr?
                 (jexpr-methods statem.expr?))
    :throw (jexpr-methods statem.expr)
    :break nil
    :continue nil
    :if (union-equal (jexpr-methods statem.test)
                     (jblock-methods statem.then))
    :ifelse (union-equal (jexpr-methods statem.test)
                         (union-equal (jblock-methods statem.then)
                                      (jblock-methods statem.else)))
    :while (union-equal (jexpr-methods statem.test)
                        (jblock-methods statem.body))
    :do (union-equal (jblock-methods statem.body)
                     (jexpr-methods statem.test))
    :for (union-equal
              (union-equal (union-equal (jexpr-methods statem.init)
                                        (jexpr-methods statem.test))
                           (jexpr-methods statem.update))
              (jblock-methods statem.body)))))

Function: jblock-methods

(defun jblock-methods (block)
  (declare (xargs :guard (jblockp block)))
  (let ((__function__ 'jblock-methods))
    (declare (ignorable __function__))
    (cond ((endp block) nil)
          (t (union-equal (jstatem-methods (car block))
                          (jblock-methods (cdr block)))))))

Theorem: return-type-of-jstatem-methods.methods

(defthm return-type-of-jstatem-methods.methods
  (b* ((?methods (jstatem-methods statem)))
    (string-listp methods))
  :rule-classes :rewrite)

Theorem: return-type-of-jblock-methods.methods

(defthm return-type-of-jblock-methods.methods
  (b* ((?methods (jblock-methods block)))
    (string-listp methods))
  :rule-classes :rewrite)

Subtopics

Jstatem-methods
Jblock-methods