Check if an ACL2 string is a valid ASCII Java package name.
The string must consist of one or more ASCII Java identifiers separated by dots.
Function:
(defun atj-string-ascii-java-package-name-p (string) (declare (xargs :guard (stringp string))) (let ((__function__ 'atj-string-ascii-java-package-name-p)) (declare (ignorable __function__)) (b* ((identifiers (str::strtok! string (list #\.)))) (and (consp identifiers) (atj-string-ascii-java-identifier-listp identifiers)))))
Theorem:
(defthm booleanp-of-atj-string-ascii-java-package-name-p (b* ((yes/no (atj-string-ascii-java-package-name-p string))) (booleanp yes/no)) :rule-classes :rewrite)