		Search-engine friendly clone of the ACL2 documentation.

Projects

Legacy-defrstobj

A predecessor of the defrstobj library that wasn't based on abstract stobjs.

The directory projects/legacy-defrstobj contains the ACL2 source files for the original version of the defrstobj library. These ACL2 books may be built by running, e.g., make legacy-defrstobj from the books/ directory.

This legacy version of record-like stobjs was written by Jared Davis before ACL2 supported abstract stobjs. As a result, many tricks and twists are needed to effectively hide the true nature of the stobj and to be able to treat it like a record.

The legacy version isn't bad—we used this version of rstobjs for our microcode model at Centaur Technology for a couple of years. But we eventually became irritated with how long it took to define rstobjs with many fields (it's quadratic in the number of fields). It's likely that a sufficiently motivated person could speed this up, and we considered a way of doing so.

But ultimately, we decided that with abstract stobjs, we could reimplement defrstobj in a much simpler way. The new approach, implemented by Sol Swords, avoids this quadratic cost, and also has a couple of other nice features. For instance:

You don't need to "good stobj" predicate in your guards, because abstract stobjs basically give you that for free;
You can use the record library's s and g functions directly, instead of needing "equivalent", stobj-specific functions.

So today there is little reason to use the legacy version. Use the new, more modern defrstobj instead!

Rather than delete the original version, we decided to put it into the projects directory. This is partly for posterity, but mostly:

For pedagogical value. The project's groundwork directory notably works through several demos, uncovering along the way the tricks that we need to support progressively more complicated stobjs as records. This may be of interest to anyone who is interested in doing crazy things to avoid hypotheses.
For regression-testing value. This is a very elaborate use of stobjs, non-executablility, and MBE tricks, and may be a good exercise to put ACL2 through as it evolves.

Copyright Information

Contact:

Centaur Technology Formal Verification Group
7600-C N. Capital of Texas Highway, Suite 300
Austin, TX 78731, USA.

License: (An MIT/X11-style license)

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.