		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-run-tests

Generate Java code to run the specified tests.

Signature
(atj-gen-run-tests tests$) → block
Arguments: tests$ — Guard (atj-test-listp tests$).
Returns: block — Type (jblockp block).

This is generated only if the :tests input is not nil.

This is a sequence of calls to the methods generated by atj-gen-test-methods. These calls are part of the main method of the test Java class.

Definitions and Theorems

Function: atj-gen-run-tests

(defun atj-gen-run-tests (tests$)
 (declare (xargs :guard (atj-test-listp tests$)))
 (let ((__function__ 'atj-gen-run-tests))
  (declare (ignorable __function__))
  (if (endp tests$)
      nil
    (b*
     ((method-name
           (atj-gen-test-method-name (atj-test->name (car tests$))))
      (first-block
           (jblock-method method-name (list (jexpr-name "n"))))
      (rest-block (atj-gen-run-tests (cdr tests$))))
     (append first-block rest-block)))))

Theorem: jblockp-of-atj-gen-run-tests

(defthm jblockp-of-atj-gen-run-tests
  (b* ((block (atj-gen-run-tests tests$)))
    (jblockp block))
  :rule-classes :rewrite)