Standard libraries for ACL2.
The std library is meant to become ACL2, Batteries Included. Its features a wide variety of books that work well together to provide a well-thought-out, documented, coherent reasoning strategy.
Std is currently under active development. You are welcome to use it, but please be aware that things may change out from under you.
So far, std itself includes libraries about basic concepts, lists, sets, alists, typed-lists, stobjs, input/output. Each of these libraries provides many lemmas for reasoning about built-in ACL2 functions, and also many additional functions. There is also a very convenient std/util macro library, with macros that automate many otherwise-tedious tasks. There is also a std/testing library with utilities to create tests.
Subtopics 
- Obags
- A library of obags (ordered bags), i.e. finite bags (a.k.a. multisets) represented as non-strictly ordered lists.
- Std/alists
- A library for reasoning about association list (alist) operations like alist-keys, alist-vals, hons-get, etc.
- Std/basic
- A collection of very basic functions that are occasionally convenient.
- Std/bitsets
- Optimized libraries for representing finite sets of natural numbers using bit masks, featuring a strong connection to the std/osets library.
- Std/io
- A library for reasoning about file input/output operations.
- Std/lists
- A library for reasoning about basic list operations like append, len, member, take, etc.
- Std/osets
- A finite set theory implementation for ACL2 based on fully ordered lists. Some major features of this approach are that set equality is just equal, and set operations like union, intersect, and so forth have O(n) implementations.
- Std/stobjs
- A library for working with stobjs.
- Std/strings
- A library with many useful functions for working with strings, and for reasoning about ACL2’s built-in string operations and these new operations.
- Std/system
- A library that complements the built-in system utilities with theorems and with non-built-in system utilities.
- Std/testing
- A library of testing utilities.
- Std/typed-alists
- Typed alists.
- Std/typed-lists
- A library about the built-in typed lists, like character-listp, nat-listp, string-listp, etc.
- Std/util
- A macro library that automates defining types, introducing typed functions, mapping over lists, and many other boilerplate tasks.
0 comments:
Post a Comment