		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-test-main-method

Generate the Java main method for the test Java class.

Signature
(atj-gen-test-main-method tests$ java-class$ no-aij-types$) → method
Arguments: tests$ — Guard (atj-test-listp tests$).; java-class$ — Guard (stringp java-class$).; no-aij-types$ — Guard (booleanp no-aij-types$).
Returns: method — Type (jmethodp method).

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

This method initializes the ACL2 environment and then calls each test method. It also prints a message saying whether all tests passed or not.

If :no-aij-types is t, we do not generate the call to initialize the environment, because there is no environment needed to run this kind of Java code.

If no argument is passed to this method (the argument normally comes from the command line, when the generated code is called as a Java application), then the test methods are called with 0 as the repetition parameter: that is, no time information is printed. Otherwise, there must exactly one argument that must parse to a positive integer, which is passed as the repetition parameter to the test methods.

Note that we generate an expression name for args.length, because grammatically this is not a field access expression in Java: it cannot be generated from the nonterminal field-acces; it can be generated from the nonterminal expression-name.

Definitions and Theorems

Function: atj-gen-test-main-method

(defun atj-gen-test-main-method (tests$ java-class$ no-aij-types$)
 (declare (xargs :guard (and (atj-test-listp tests$)
                             (stringp java-class$)
                             (booleanp no-aij-types$))))
 (let ((__function__ 'atj-gen-test-main-method))
  (declare (ignorable __function__))
  (b*
   ((method-param
         (make-jparam :final? nil
                      :type (jtype-array (jtype-class "String"))
                      :name "args"))
    (method-body
     (append
      (jblock-locvar (jtype-int)
                     "n" (jexpr-literal-0))
      (jblock-if
       (jexpr-binary (jbinop-eq)
                     (jexpr-name "args.length")
                     (jexpr-literal-1))
       (jblock-asg
            (jexpr-name "n")
            (jexpr-smethod (jtype-class "Integer")
                           "parseInt"
                           (list (jexpr-array (jexpr-name "args")
                                              (jexpr-literal-0))))))
      (jblock-if
       (jexpr-binary (jbinop-gt)
                     (jexpr-name "args.length")
                     (jexpr-literal-1))
       (jblock-throw
        (jexpr-newclass
         (jtype-class "IllegalArgumentException")
         (list
          (jexpr-literal-string
           "There must be 0 or 1
                                  arguments.")))))
      (and (not no-aij-types$)
           (jblock-smethod (jtype-class java-class$)
                           "initialize" nil))
      (atj-gen-run-tests tests$)
      (jblock-ifelse
       (jexpr-name "failures")
       (append (jblock-imethod
                    (jexpr-name "System.out")
                    "println"
                    (list (atj-gen-jstring "Some tests failed.")))
               (jblock-imethod (jexpr-name "System.out")
                               "println" nil)
               (jblock-smethod (jtype-class "System")
                               "exit" (list (jexpr-literal-1))))
       (append (jblock-imethod
                    (jexpr-name "System.out")
                    "println"
                    (list (atj-gen-jstring "All tests passed.")))
               (jblock-imethod (jexpr-name "System.out")
                               "println" nil)
               (jblock-smethod (jtype-class "System")
                               "exit" (list (jexpr-literal-0))))))))
   (make-jmethod :access (jaccess-public)
                 :abstract? nil
                 :static? t
                 :final? nil
                 :synchronized? nil
                 :native? nil
                 :strictfp? nil
                 :result (jresult-void)
                 :name "main"
                 :params (list method-param)
                 :throws (and (not no-aij-types$)
                              (list *aij-class-undef-pkg-exc*))
                 :body method-body))))

Theorem: jmethodp-of-atj-gen-test-main-method

(defthm jmethodp-of-atj-gen-test-main-method
 (b*
  ((method
       (atj-gen-test-main-method tests$ java-class$ no-aij-types$)))
  (jmethodp method))
 :rule-classes :rewrite)