		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-test-method-name

Name of the Java method to run one of the specified tests.

Signature
(atj-gen-test-method-name test-name) → method-name
Arguments: test-name — Guard (stringp test-name).
Returns: method-name — Type (stringp method-name).

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

We generate a private static method for each test specified by the :tests input. This function generates the name of this method, which has the form test_..., where ... is the name of the test. Since ATJ checks that the tests have unique names, this scheme ensures that the method names are all distinct.

The argument of this function is the name of the test.

Definitions and Theorems

Function: atj-gen-test-method-name

(defun atj-gen-test-method-name (test-name)
  (declare (xargs :guard (stringp test-name)))
  (let ((__function__ 'atj-gen-test-method-name))
    (declare (ignorable __function__))
    (str::cat "test_" test-name)))

Theorem: stringp-of-atj-gen-test-method-name

(defthm stringp-of-atj-gen-test-method-name
  (b* ((method-name (atj-gen-test-method-name test-name)))
    (stringp method-name))
  :rule-classes :rewrite)