| A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. # (2007) | |||||||||||||||
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 di#erent 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 equations. In that work, multisets were represented using lists, and some of the theorems proved there depend on this particular representation. Now suppose that we have another ACL2 book developing a theory about finite multisets, based on a di#erent implementation (for example, using association lists to represent characteristic functions). If we had wanted to use our well-foundedness theorem with this alternative representation of multisets, we would have had two possibilities: | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||