A Phonebook Specification
The other tutorial examples are rather small and entirely self contained. The present example is rather more elaborate, and makes use of a feature that really adds great power and versatility to ACL2, namely: the use of previously defined collections of lemmas, in the form of ``books.''
This example was written almost entirely by Bill Young of Computational Logic, Inc.
This example is based on one developed by Ricky Butler and Sally Johnson of NASA Langley for the PVS system, and subsequently revised by Judy Crow, et al, at SRI. It is a simple phone book specification. We will not bother to follow their versions closely, but will instead present a style of specification natural for ACL2.
The idea is to model an electronic phone book with the following properties.
Our phone book will store the phone numbers of a city.
It must be possible to retrieve a phone number, given a name.
It must be possible to add and delete entries.
Of course, there are numerous ways to construct such a model. A natural
approach within the Lisp/ACL2 context is to use ``association lists'' or
``alists.'' Briefly, an alist is a list of pairs
We could build a theory of alists from scratch, or we can use a previously constructed theory (book) of alist definitions and facts. By using an existing book, we build upon the work of others, start our specification and proof effort from a much richer foundation, and hopefully devote more of our time to the problem at hand. Unfortunately, it is not completely simple for the new user to know what books are available and what they contain. We hope later to improve the documentation of the growing collection of community-books that are typically downloaded with ACL2; for now, the reader is encouraged to look in the README.html file in the books' top-level directory. For present purposes, the beginning user can simply take our word that a book exists containing useful alist definitions and facts. These definitions and lemmas can be introduced into the current theory using the command:
(include-book "data-structures/alist-defthms" :dir :system)
Including this book makes available a collection of functions including the following:
(ALISTP A) ; is A an alist (actually a primitive ACL2 function) (BIND X V A) ; associate the key X with value V in alist A (BINDING X A) ; return the value associated with key X in alist A (BOUND? X A) ; is key X associated with any value in alist A (DOMAIN A) ; return the list of keys bound in alist A (RANGE A) ; return the list of values bound to keys in alist A (REMBIND X A) ; remove the binding of key X in alist A
Along with these function definitions, the book also provides a number of proved lemmas that aid in simplifying expressions involving these functions. (See rule-classes for the way in which lemmas are used in simplification and rewriting.) For example,
asserts that the resulting binding will be
Thus, the inclusion of this book essentially extends our specification and reasoning capabilities by the addition of new operations and facts about these operations that allow us to build further specifications on a richer and possibly more intuitive foundation.
However, it must be admitted that the use of a book such as this has two potential limitations:
the definitions available in a book may not be ideal for your particular problem;
it is (extremely) likely that some useful facts (especially, rewrite rules) are not available in the book and will have to be proved.
For example, what is the value of
ACL2 !>:pe binding d 33 (INCLUDE-BOOK "/slocal/src/acl2/v1-9/books/public/alist-defthms") >V d (DEFUN BINDING (X A) "The value bound to X in alist A." (DECLARE (XARGS :GUARD (ALISTP A))) (CDR (ASSOC-EQUAL X A)))
This tells us that
ACL2 !>:pe assoc-equal V -489 (DEFUN ASSOC-EQUAL (X ALIST) (DECLARE (XARGS :GUARD (ALISTP ALIST))) (COND ((ENDP ALIST) NIL) ((EQUAL X (CAR (CAR ALIST))) (CAR ALIST)) (T (ASSOC-EQUAL X (CDR ALIST)))))
we can see that assoc-equal returns
These definitions aren't ideal for all purposes. For one thing, there's
nothing that keeps us from having
Why not take a look at the definitions of other alist functions and see how they work together to provide the ability to construct and search alists? We'll be using them rather heavily in what follows so it will be good if you understand basically how they work. Simply start up ACL2 and execute the form shown earlier, but substituting our directory name for the top-level ACL2 directory with yours. Alternatively, just
(include-book "data-structures/alist-defthms" :dir :system)
Then, you can use
The other problem with using a predefined book is that it will seldom be
``sufficiently complete,'' in the sense that the collection of rewrite
rules supplied won't be adequate to prove everything we'd like to know about
the interactions of the various functions. If it were, there'd be no real
reason to know that
Notice that alists are mappings of keys to values; but, there is no notion of a ``type'' associated with the keys or with the values. Our phone book example, however, does have such a notion of types; we map names to phone numbers. We can introduce these ``types'' by explicitly defining them, e.g., names are strings and phone numbers are integers. Alternatively, we can partially define or axiomatize a recognizer for names without giving a full definition. A way to safely introduce such ``constrained'' function symbols in ACL2 is with the encapsulate form. For example, consider the following form.
(encapsulate ;; Introduce a recognizer for names and give a ``type'' lemma. (((namep *) => *)) ;; (local (defun namep (x) ;; This declare is needed to tell ;; ACL2 that we're aware that the ;; argument x is not used in the body ;; of the function. (declare (ignore x)) t)) ;; (defthm namep-booleanp (booleanp (namep x))))
This encapsulate form introduces the new function
The first ``argument'' to
We can subsequently use
We wish to do something similar to define what it means to be a legal phone number. We submit the following form to ACL2:
(encapsulate ;; Introduce a recognizer for phone numbers. (((pnump *) => *)) ;; (local (defun pnump (x) (not (equal x nil)))) ;; (defthm pnump-booleanp (booleanp (pnump x))) ;; (defthm nil-not-pnump (not (pnump nil)))).
This introduces a Boolean-valued recognizer
Now a legal phone book is an alist mapping from
(defun name-phonenum-pairp (x) ;; Recognizes a pair of (name . pnum). (and (consp x) (namep (car x)) (pnump (cdr x)))) (defun phonebookp (l) ;; Recognizes a list of such pairs. (if (not (consp l)) (null l) (and (name-phonenum-pairp (car l)) (phonebookp (cdr l)))))
Thus, a phone book is really a list of pairs
Now we are ready to define some of the functions necessary for our phonebook example. The functions we need are:
(IN-BOOK? NM BK) ; does NM have a phone number in BK (FIND-PHONE NM BK) ; find NM's phone number in phonebook BK (ADD-PHONE NM PNUM BK) ; give NM the phone number PNUM in BK (CHANGE-PHONE NM PNUM BK) ; change NM's phone number to PNUM in BK (DEL-PHONE NM PNUM) ; remove NM's phone number from BK
Given our underlying theory of alists, it is easy to write these functions. But we must take care to specify appropriate ``boundary'' behavior. Thus, what behavior do we want when, say, we try to change the phone number of a client who is not currently in the book? As usual, there are numerous possibilities; here we'll assume that we return the phone book unchanged if we try anything ``illegal.''
Possible definitions of our phone book functions are as follows.
(defun in-book? (nm bk) (bound? nm bk)) (defun find-phone (nm bk) (binding nm bk)) (defun add-phone (nm pnum bk) ;; If nm already in-book?, make no change. (if (in-book? nm bk) bk (bind nm pnum bk))) (defun change-phone (nm pnum bk) ;; Make a change only if nm already has a phone number. (if (in-book? nm bk) (bind nm pnum bk) bk)) (defun del-phone (nm bk) ;; Remove the binding from bk, if there is one. (rembind nm bk))
Notice that we don't have to check whether a name is in the book before
In some sense, this completes our specification. But we can't have any real confidence in its correctness without validating our specification in some way. One way to do so is by proving some properties of our specification. Some candidate properties are:
1. A name will be in the book after we add it.
2. We will find the most recently added phone number for a client.
3. If we change a number, we'll find the change.
4. Changing and then deleting a number is the same as just deleting.
5. A name will not be in the book after we delete it.
Let's formulate some of these properties. The first one, for example, is:
(defthm add-in-book (in-book? nm (add-phone nm pnum bk))).
You may wonder why we didn't need any hypotheses about the ``types'' of the
arguments. In fact,
(defthm add-in-book (implies (and (namep nm) (pnump pnum) (phonebookp bk)) (in-book? nm (add-phone nm pnum bk)))),
but that would have yielded a weaker and less useful lemma because it would apply to fewer situations. In general, it is best to state lemmas in the most general form possible and to eliminate unnecessary hypotheses whenever possible. The reason for that is simple: lemmas are usually stored as rules and used in later proofs. For a lemma to be used, its hypotheses must be relieved (proved to hold in that instance); extra hypotheses require extra work. So we avoid them whenever possible.
There is another, more important observation to make about our lemma. Even
in its simpler form (without the extraneous hypotheses), the lemma
(in-book? nm (add-phone nm pnum bk)).
Since we've already proved
Warnings: Non-rec Time: 0.18 seconds (prove: 0.05, print: 0.00, other: 0.13) ADD-IN-BOOK
The ``Warnings'' line notifies you that there are non-recursive function
calls in the left hand side of the conclusion and that this problem might
arise. Of course, it may be that you don't ever plan to use the lemma for
rewriting or that your intention is to disable these functions. Disabled functions are not expanded and the lemma should apply. However, you
should always take note of such warnings and consider an appropriate response.
By the way, we noted above that
For our current example, let's assume that we're just investigating the
properties of our specifications and not concerned about using our lemmas for
rewriting. So let's go on. If we really want to avoid the warnings, we can
Property 2 is: we always find the most recently added phone number for a client. Try the following formalization:
and you'll find that the proof attempt fails. Examining the proof attempt
and our function definitions, we see that the lemma is false if
(defthm find-add1 (implies (not (in-book? nm bk)) (equal (find-phone nm (add-phone nm pnum bk)) pnum))) (defthm find-add2 (equal (find-phone nm (add-phone nm pnum bk)) (if (in-book? nm bk) (find-phone nm bk) pnum)))
For technical reasons, lemmas such as
Property 3 says: If we change a number, we'll find the change. This is very similar to the previous example. The formalization is as follows.
(defthm find-change (equal (find-phone nm (change-phone nm pnum bk)) (if (in-book? nm bk) pnum (find-phone nm bk))))
Property 4 says: changing and then deleting a number is the same as just deleting. We can model this as follows.
Unfortunately, when we try to prove this, we encounter subgoals that seem
to be true, but for which the prover is stumped. For example, consider the
following goal. (Note:
Subgoal *1/4 (IMPLIES (AND (NOT (ENDP BK)) (NOT (EQUAL NM (CAAR BK))) (NOT (BOUND? NM (CDR BK))) (BOUND? NM BK)) (EQUAL (REMBIND NM (BIND NM PNUM BK)) (REMBIND NM BK))).
Our intuition about
The prover proves this by induction, and stores it as a rewrite rule.
After that, the prover has no difficulty in proving
The need to prove lemma
Finally, let's consider our property 5 above: a name will not be in the book after we delete it. We formalize this as follows:
This proves easily. But notice that it's only true because
To complete this example, let's consider adding an invariant to our specification. In particular, suppose we want to assure that no client has more than one associated phone number. One way to ensure this is to require that the domain of the alist is a ``set'' (has no duplicates).
(defun setp (l) (if (atom l) (null l) (and (not (member-equal (car l) (cdr l))) (setp (cdr l))))) (defun valid-phonebookp (bk) (and (phonebookp bk) (setp (domain bk))))
Now, we want to show under what conditions our operations preserve the
property of being a
(defthm in-book-booleanp (booleanp (in-book? nm bk))) (defthm in-book-namep (implies (and (phonebookp bk) (in-book? nm bk)) (namep nm)) :hints (("Goal" :in-theory (enable bound?)))) (defthm find-phone-pnump (implies (and (phonebookp bk) (in-book? nm bk)) (pnump (find-phone nm bk))) :hints (("Goal" :in-theory (enable bound? binding))))
Note the ``
Below we develop the theorems showing that
(defthm bind-preserves-phonebookp (implies (and (phonebookp bk) (namep nm) (pnump num)) (phonebookp (bind nm num bk)))) (defthm member-equal-strip-cars-bind (implies (and (not (equal x y)) (not (member-equal x (strip-cars a)))) (not (member-equal x (strip-cars (bind y z a)))))) (defthm bind-preserves-domain-setp (implies (and (alistp bk) (setp (domain bk))) (setp (domain (bind nm num bk)))) :hints (("Goal" :in-theory (enable domain)))) (defthm phonebookp-alistp (implies (phonebookp bk) (alistp bk))) (defthm ADD-PHONE-PRESERVES-INVARIANT (implies (and (valid-phonebookp bk) (namep nm) (pnump num)) (valid-phonebookp (add-phone nm num bk))) :hints (("Goal" :in-theory (disable domain-bind)))) (defthm CHANGE-PHONE-PRESERVES-INVARIANT (implies (and (valid-phonebookp bk) (namep nm) (pnump num)) (valid-phonebookp (change-phone nm num bk))) :hints (("Goal" :in-theory (disable domain-bind)))) (defthm remove-equal-preserves-setp (implies (setp l) (setp (remove-equal x l)))) (defthm rembind-preserves-phonebookp (implies (phonebookp bk) (phonebookp (rembind nm bk)))) (defthm DEL-PHONE-PRESERVES-INVARIANT (implies (valid-phonebookp bk) (valid-phonebookp (del-phone nm bk))))
As a final test of your understanding, try to formulate and prove an invariant that says that no phone number is assigned to more than one name. The following hints may help.
1. Define the appropriate invariant. (Hint: remember the function
2. Do our current definitions of
add-phoneand change-phonenecessarily preserve this property? If not, consider what hypotheses are necessary in order to guarantee that they do preserve this property.
3. Study the definition of the function
rangeand notice that it is defined in terms of the function strip-cdrs. Understand how this defines the range of an alist.
4. Formulate the correctness theorems and attempt to prove them. You'll probably benefit from studying the invariant proof above. In particular, you may need some fact about the function strip-cdrs analogous to the lemma
Below is one solution to this exercise. Don't look at the solution,
however, until you've struggled a bit with it. Notice that we didn't actually
change the definitions of
(defun pnums-in-use (bk) (range bk)) (defun phonenums-unique (bk) (setp (pnums-in-use bk))) (defun new-pnump (pnum bk) (not (member-equal pnum (pnums-in-use bk)))) (defthm member-equal-strip-cdrs-rembind (implies (not (member-equal x (strip-cdrs y))) (not (member-equal x (strip-cdrs (rembind z y)))))) (defthm DEL-PHONE-PRESERVES-PHONENUMS-UNIQUE (implies (phonenums-unique bk) (phonenums-unique (del-phone nm bk))) :hints (("Goal" :in-theory (enable range)))) (defthm strip-cdrs-bind-non-member (implies (and (not (bound? x a)) (alistp a)) (equal (strip-cdrs (bind x y a)) (append (strip-cdrs a) (list y)))) :hints (("Goal" :in-theory (enable bound?)))) (defthm setp-append-list (implies (setp l) (equal (setp (append l (list x))) (not (member-equal x l))))) (defthm ADD-PHONE-PRESERVES-PHONENUMS-UNIQUE (implies (and (phonenums-unique bk) (new-pnump pnum bk) (alistp bk)) (phonenums-unique (add-phone nm pnum bk))) :hints (("Goal" :in-theory (enable range)))) (defthm member-equal-strip-cdrs-bind (implies (and (not (member-equal z (strip-cdrs a))) (not (equal z y))) (not (member-equal z (strip-cdrs (bind x y a)))))) (defthm CHANGE-PHONE-PRESERVES-PHONENUMS-UNIQUE (implies (and (phonenums-unique bk) (new-pnump pnum bk) (alistp bk)) (phonenums-unique (change-phone nm pnum bk))) :hints (("Goal" :in-theory (enable range))))