| A generic instantiation tool and a case study: A generic multiset theory (2002) | |||||||||||||||
Abstract | |||||||||||||||
| In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the theory be as independent of a concrete implementation as possible. This is particularly interesting when we design theories about basic data types, making those developments more general, reusable and extensible. At the same time, it would also be desirable to be able to instantiate (in a convenient way) the definitions and theorems of the theory, for a concrete implementation. In this paper we present the development of a particular generic theory, and a tool to instantiate its events. As a case study we have chosen to describe a generic theory about finite multisets. It is also shown how this generic theory can be instantiated (using several macros we have defined) to build a theory about two different implementations of multisets. Finally we propose some directions for further research in this topic. 1 Motivation of this work In [7] we proved the well-foundedness of an extension to finite multisets of a well-founded ACL2 relation, and showed how this result can be used to prove the termination of non-trivial recursive | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||