		Search-engine friendly clone of the ACL2 documentation.

Declare-stobjs

Declaring a formal parameter name to be a single-threaded object

When a defun uses one of its formals as a single-threaded object (stobj), the defun must include a declaration that the formal is to be so used. An exception is the formal ``state,'' which if not declared as explained below, may still be used provided an appropriate global ``declaration'' is issued: see set-state-ok.

If the formal in question is counters then an appropriate declaration is

(declare (xargs :stobjs counters))

or, more generally,

(declare (xargs :stobjs (... counters ...)))

where all the single-threaded formals are listed.

For such a declaration to be legal it must be the case that all the names have previously been defined as single-threaded objects with defstobj.

When an argument is declared to be single-threaded the guard of the function is augmented by conjoining to it the condition that the argument satisfy the recognizer for the single-threaded object. Furthermore, the syntactic checks done to enforce the legal use of single-threaded objects are also sufficient to allow these guard conjuncts to be automatically proved.

The obvious question arises: Why does ACL2 insist that you declare stobj names before using them in defuns if you can only declare names that have already been defined with defstobj? What would go wrong if a formal were treated as a single-threaded object if and only if it had already been so defined?

Suppose that one user, say Jones, creates a book in which counters is defined as a single-threaded object. Suppose another user, Smith, creates a book in which counters is used as an ordinary formal parameter. Finally, suppose a third user, Brown, wishes to use both books. If Brown includes Jones' book first and then Smith's, then Smith's function treats counters as single-threaded. But if Brown includes Smith's book first, the argument is treated as ordinary.

ACL2 insists on the declaration to ensure that the definition is processed the same way no matter what the context.