STOBJ-EXAMPLE-3

another example of a single-threaded object 
Major Section:  STOBJ

The event 

(defstobj $s
  (x :type integer :initially 0)
  (a :type (array (integer 0 9) (3)) :initially 9 :resizable t))
introduces a stobj named $S. The stobj has two fields, X and A. The A field is an array. The X field contains an integer and is initially 0. The A field contains a list of integers, each between 0 and 9, inclusively. (Under the hood, this ``list'' is actually implemented as an array.) Initially, the A field has three elements, each of which is 9.

This event introduces the following sequence of function definitions: 

(DEFUN XP (X) ...)               ; recognizer for X field
(DEFUN AP (X) ...)               ; recognizer of A field
(DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
(DEFUN CREATE-$S NIL ...)        ; creator for stobj $S
(DEFUN X ($S) ...)               ; accessor for X field
(DEFUN UPDATE-X (V $S) ...)      ; updater for X field
(DEFUN A-LENGTH ($S) ...)        ; length of A field
(DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
(DEFUN AI (I $S) ...)            ; accessor for A field at index I
(DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

Here is the definition of $SP: 

(DEFUN $SP ($S)
  (DECLARE (XARGS :GUARD T :VERIFY-GUARDS T))
  (AND (TRUE-LISTP $S)
       (= (LENGTH $S) 2)
       (XP (NTH 0 $S))
       (AP (NTH 1 $S))
       T))
This reveals that in order to satisfy $SP an object must be a true list of length 2 whose first element satisfies XP and whose second satisfies AP. By printing the definition of AP one learns that it requires its argument to be a true list, each element of which is an integer between 0 and 9.

The initial value of stobj $S is given by zero-ary ``creator'' function CREATE-$S. Creator functions may only be used in limited contexts. See with-local-stobj.

Here is the definition of UPDATE-AI, the updater for the A field at index I: 

(DEFUN UPDATE-AI (I V $S)
  (DECLARE (XARGS :GUARD
                  (AND ($SP $S)
                       (INTEGERP I)
                       (<= 0 I)
                       (< I (A-LENGTH $S))
                       (AND (INTEGERP V) (<= 0 V) (<= V 9)))
                  :VERIFY-GUARDS T))
  (UPDATE-NTH-ARRAY 1 I V $S))
By definition (UPDATE-NTH-ARRAY 1 I V $S) is (UPDATE-NTH 1 (UPDATE-NTH I V (NTH 1 $S)) $S). This may be a little surprising but should be perfectly clear.

First, ignore the guard, since it is irrelevant in the logic. Reading from the inside out, (UPDATE-AI I V $S) extracts (NTH 1 $S), which is array a of $S. (Recall that NTH is 0-based.) The next higher expression in the definition above, (UPDATE-NTH I V a), ``modifies'' a by setting its Ith element to V. Call this a'. The next higher expression, (UPDATE-NTH 1 a' $S), ``modifies'' $S by setting its 1st component to a'. Call this result $s'. Then $s' is the result returned by UPDATE-AI.

So the first useful observation is that from the perspective of the logic, the type ``restrictions'' on stobjs are irrelevant. They are ``enforced'' by ACL2's guard mechanism, not by the definitions of the updater functions.

As one might also imagine, the accessor functions do not really ``care,'' logically, whether they are applied to well-formed stobjs or not. For example, (AI I $S) is defined to be (NTH I (NTH 1 $S)).

Thus, you will not be able to prove that (AI 2 $S) is an integer. That is, 

(integerp (AI 2 $S))
is not a theorem, because $S may not be well-formed.

Now (integerp (AI 2 $S)) will always evaluate to T in the top-level ACL2 command loop, because we insist that the current value of the stobj $S always satisfies $SP by enforcing the guards on the updaters, independent of whether guard checking is on or off; see set-guard-checking. But in a theorem $S is just another variable, implicitly universally quantified.

So (integerp (AI 2 $S)) is not a theorem because it is not true when the variable $S is instantiated with, say, 

'(1 (0 1 TWO))
because, logically speaking, (AI 2 '(1 (0 1 TWO))) evaluates to the symbol TWO. That is, 
(equal (AI 2 '(1 (0 1 TWO))) 'TWO)
is true.

However, 

(implies (and ($SP $S) (< 2 (A-LENGTH $S))) (integerp (AI 2 $S)))
is a theorem. To prove it, you will have to prove a lemma about AP. The following will do: 
(defthm ap-nth
  (implies (and (AP x)
                (integerp i)
                (<= 0 i)
                (< i (len x)))
           (integerp (nth i x)))).

Similarly, 

(implies (and (integerp i)
              (<= 0 i)
              (< i (A-LENGTH $S))
              (integerp v)
              (<= 0 v)
              (<= v 9))
         ($SP (UPDATE-AI i v $S)))
is not a theorem until you add the additional hypothesis ($SP $S). To prove the resulting theorem, you will need a lemma such as the following. 
(defthm ap-update-nth
  (implies (and (AP a)
                (integerp v)
                (<= 0 v)
                (<= v 9)
                (integerp i)
                (<= 0 i)
                (< i (len a)))
           (AP (update-nth i v a))))

The moral here is that from the logical perspective, you must provide the hypotheses that, as a programmer, you think are implicit on the structure of your stobjs, and you must prove their invariance. This is a good area for further support, perhaps in the form of a library of macros.

Resizing Array Fields

Recall the specification of the array field, A for the stobj $S introduced above: 

(a :type (array (integer 0 9) (3)) :initially 9 :resizable t)
Logically, this field is a list, initially of length 3. Under the hood, this field is implemented using a Common Lisp array with 3 elements. In some applications, one may wish to lengthen an array field, or even (to reclaim space) to shrink an array field. The defstobj event provides functions to access the current length of an array field and to change the array field, with default names obtained by suffixing the field name with ``LENGTH-'' or prefixing it with ``RESIZE-,'' respectively. The following log shows the uses of these fields in the above example. 
ACL2 !>(A-LENGTH $S)
3
ACL2 !>(RESIZE-A 10 $S) ; change length of A to 10
<$s>
ACL2 !>(A-LENGTH $S)
10
ACL2 !>(AI 7 $S)        ; new elements get value from :initially
9
ACL2 !>(RESIZE-A 2 $S)  ; truncate A down to first 2 elements
<$s>
ACL2 !>(A-LENGTH $S)
2
ACL2 !>(AI 7 $S)        ; error:  access past array bound



ACL2 Error in TOP-LEVEL:  The guard for the function symbol AI, which
is (AND ($SP $S) (INTEGERP I) (<= 0 I) (< I (A-LENGTH $S))), is violated
by the arguments in the call (AI 7 $S).


ACL2 !>
Here are the definitions of the relevant functions for the above example; also see resize-list. 
(DEFUN A-LENGTH ($S)
  (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
  (LEN (NTH 1 $S)))


(DEFUN RESIZE-A (K $S)
  (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
  (UPDATE-NTH 1
              (RESIZE-LIST (NTH 1 $S) K 9)
              $S))

It is important to note that the implementation of array resizing in ACL2 involves copying the entire array into a newly allocated space and thus can be quite costly if performed often. This approach was chosen in order to make array access and update as efficient as possible, with the suspicion that for most applications, array access and update are considerably more frequent than resizing (especially if the programmer is aware of the relative costs beforehand).

It should also be noted that computations of lengths of stobj array fields should be fast (constant-time) in all or most Common Lisp implementations.

Finally, if :resizable t is not supplied as shown above, then an attempt to resize the array will result in an error. If you do not intend to resize the array, it is better to omit the :resizable option (or to supply :resizable nil), since then the length function will be defined to return a constant, namely the initial length, which can simplify guard proofs (compare with the definition of A-LENGTH above).

This completes the tour through the documentation of stobjs. However, you may now wish to read the documentation for the event that introduces a new single-threaded object; see defstobj.