		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-init-method

Generate the Java public method to initialize the ACL2 environment.

Signature
(atj-gen-init-method) → method
Returns: method — Type (jmethodp method).

This method is actually empty, but its invocation ensures that the class initializer, which builds the ACL2 environment, has been executed.

The reason for having an empty initialization method and the environment-building code in the static initializer, as opposed to having no static initializer and the environment-building code in the initialization method, is that, in the shallow embedding approach, we need the ACL2 environment to be initialized before we create certain final static fields that involve ACL2 symbols, and that therefore need the ACL2 environment to be built. This is unnecessary in the deep embedding approach, but we use the same code structure for uniformity and simplicity.

Definitions and Theorems

Function: atj-gen-init-method

(defun atj-gen-init-method nil
  (declare (xargs :guard t))
  (let ((__function__ 'atj-gen-init-method))
    (declare (ignorable __function__))
    (make-jmethod :access (jaccess-public)
                  :abstract? nil
                  :static? t
                  :final? nil
                  :synchronized? nil
                  :native? nil
                  :strictfp? nil
                  :result (jresult-void)
                  :name "initialize"
                  :params nil
                  :throws nil
                  :body nil)))

Theorem: jmethodp-of-atj-gen-init-method

(defthm jmethodp-of-atj-gen-init-method
  (b* ((method (atj-gen-init-method)))
    (jmethodp method))
  :rule-classes :rewrite)