Ponencia
A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.
Autor/es | Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2002 |
Fecha de depósito | 2021-03-16 |
Publicado en |
|
Resumen | 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 ... 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. |
Agencias financiadoras | Ministerio de Ciencia Y Tecnología (MCYT). España |
Identificador del proyecto | TIC2000-1368-CO3-02 |
Cita | Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2002). A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.. En ACL2 2002: Third International Workshop on the ACL2 Theorem Prover and Its Applications Grenoble, France: University of Texas. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
A generic instantiation tool and ... | 122.7Kb | [PDF] | Ver/ | |