		Search-engine friendly clone of the ACL2 documentation.

Atj-code-generation

Atj-gen-test-methods

Generate all the Java methods to run the specified tests.

Signature
(atj-gen-test-methods tests$ deep$ guards$ no-aij-types$ java-class$ verbose$ pkg-class-names fn-method-names wrld) → methods
Arguments: tests$ — Guard (atj-test-listp tests$).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; no-aij-types$ — Guard (booleanp no-aij-types$).; java-class$ — Guard (stringp java-class$).; verbose$ — Guard (booleanp verbose$).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; fn-method-names — Guard (symbol-string-alistp fn-method-names).; wrld — Guard (plist-worldp wrld).
Returns: methods — Type (jmethod-listp methods).

These are generated only if the :tests input is not nil.

Definitions and Theorems

Function: atj-gen-test-methods

(defun atj-gen-test-methods
       (tests$ deep$ guards$
               no-aij-types$ java-class$ verbose$
               pkg-class-names fn-method-names wrld)
 (declare (xargs :guard (and (atj-test-listp tests$)
                             (booleanp deep$)
                             (booleanp guards$)
                             (booleanp no-aij-types$)
                             (stringp java-class$)
                             (booleanp verbose$)
                             (string-string-alistp pkg-class-names)
                             (symbol-string-alistp fn-method-names)
                             (plist-worldp wrld))))
 (let ((__function__ 'atj-gen-test-methods))
  (declare (ignorable __function__))
  (if (endp tests$)
      nil
   (b*
    ((first-method
         (atj-gen-test-method (car tests$)
                              deep$ guards$
                              no-aij-types$ java-class$ verbose$
                              pkg-class-names fn-method-names wrld))
     (rest-methods
       (atj-gen-test-methods (cdr tests$)
                             deep$ guards$
                             no-aij-types$ java-class$ verbose$
                             pkg-class-names fn-method-names wrld)))
    (cons first-method rest-methods)))))

Theorem: jmethod-listp-of-atj-gen-test-methods

(defthm jmethod-listp-of-atj-gen-test-methods
 (b*
  ((methods
       (atj-gen-test-methods tests$ deep$ guards$
                             no-aij-types$ java-class$ verbose$
                             pkg-class-names fn-method-names wrld)))
  (jmethod-listp methods))
 :rule-classes :rewrite)