La abstracción como tipo de dato
DSN_XP entre en contacto con John Guttag cuando comenzamos a analizar tanto a la ingeniería que da soporte al proceso de abstracción en el desarrollo de software y a la ingeniería de software / ciencias de la computación en el desarrollo e implementación de dicho software.
Para la arquitectura, la ingeniería es la base fundamental para el desarrollo de las perspectivas de diseño que necesariamente requieren de una estructura modular.
El concepto de tipo de dato abstracto (TDA, Abstract Data Type), fue propuesto por primera vez hacia 1974 por John Guttag y otros, pero no fue hasta 1975 que por primera vez Barbara Liskov lo propuso para el lenguaje CLU.
El diseño de especificaciones de tipos de datos
Documento de conferencia
Enero de 1976
John V. Guttag *, Ellis Horowitz * y David R. Musser **
Resumen
Este artículo trata sobre el diseño de tipos de datos en la creación de un sistema de software. El punto principal es explorar un significado para especificar un tipo de dato que es independiente de su eventual implementación. El estilo particular de especificación denominado axiomas algebraicos, se exhibe axiomatizando muchos tipos de datos de uso común. Como tal, estos ejemplos revelan mucho sobre las complejidades de la especificación del tipo de datos a través de axiomas algebraicos y, además, un estándar con el que se pueden comparar formas alternativas. Más allá del uso de esta técnica de especificación para probar la exactitud de las implementaciones y en la ejecución interpretativa de un diseño de sistema grande antes de que comience la implementación real.
Términos de indexación:
Tipo de datos, especificación, axiomas algebraicos, software diseño, programación recursiva, corrección del programa.
Introducción
El proceso de creación de un sistema de software es generalmente considerado como un proceso de cuatro etapas: requisitos, diseño, codificación y pruebas. Para algunas de estas etapas, las herramientas, las técnicas o ambas han sido desarrolladas para mejorar significativamente el proceso.
Recientemente ha habido una creciente preocupación por el desarrollo de ayudas para la etapa de diseño. El diseño es esencialmente un proceso creativo, sintético y una herramienta completamente automatizada es muy poco probable que lo sea.
Lo que se sugiere es seguir una "metodología" o un estilo de trabajo, que se supone produce diseños mejorados.
El diseño de arriba hacia abajo es un proceso mediante el cual se transforma una tarea en un programa ejecutable. Este proceso en su forma más pura, requiere refinar cuidadosamente, paso a paso, los requisitos funcionales de un sistema en programas operativos, más las directrices sobre la elección de declaraciones apropiadas y el aplazamiento de decisiones de diseño, se puede encontrar en [Dahl 72].
El propósito de este artículo es explorar una estrategia complementaria de diseño, el diseño de tipos de datos.
Un sistema completo de software puede contener una variedad de tipos de datos (listas, pilas, árboles, matrices, etc.) y una variedad de operaciones.
Un procedimiento de diseño útil es tratar aquellas operaciones que actúan principalmente sobre un solo tipo de datos como parte de una unidad y considerar la semántica de estas operaciones como la definición del tipo.
Esta idea estaba implícita en el lenguaje de programación SIMULA 67 [Dahl 70], en el que la designación sintáctica class denota una colección de tales operaciones. Sin embargo, el concepto de clase aplica este principio a nivel de lenguaje de programación en lugar de en tiempo de diseño.
Cada operación de una clase es directamente un programa ejecutable. También es útil considerar una colección de operaciones en tiempo de diseño y luego el proceso de diseño (de tipos de datos) consiste en especificar esas operaciones a cada vez mayor nivel de detalle hasta que se logre una implementación ejecutable, la idea que deseamos explorar aquí es cómo crear una especificación inicial de un tipo de dato.
Una especificación de un tipo de dato (o tipo de dato abstracto) es una definición formal independiente de la representación de cada operación de un tipo de datos. Por lo tanto, el diseño completo de un solo tipo de datos procede dando primero su especificación, seguido de una (eficiente) implementación que esté de acuerdo con la especificación. Esta separación del diseño de tipos de datos en dos fases distintas es muy útil desde un punto de vista organizacional. Cualquier proceso que necesite hacer uso del tipo de datos puede hacerlo examinando solo la especificación.
No es necesario esperar hasta que el tipo esté completamente implementado ni necesario para comprender completamente la implementación.
Hay dos preocupaciones principales al diseñar una técnica para especificación de tipo datos:
- La primera es idear una notación que permita una definición rigurosa de operaciones pero sigue siendo una representación independiente y
- la segunda es aprender a usar esa notación. Ahí hay muchos criterios que se pueden usar para medir el valor de una notación de especificación, pero las dos principales son las siguientes:
- ¿pueden las especificaciones ser construidas sin dificultad indebida? y,
- ¿es la especificación resultante fácil de comprender?.
Al igual que con la programación, hay potencialmente un gran número de formas de especificar una operación. Una buena especificación de tipo de dato debe proporcionar la información suficiente para definir el tipo, pero no tanto que la elección de sus implementaciones que son basadas en la especificación es limitada. Por tanto, decimos que una especificación de tipo de dato es una abstracción de un concepto cuya implementación final es solo una instancia.
En este artículo, nuestra intención es explorar una técnica de especificación particular [Guttag 75], [Zilles 75], [Goguen 75], al exhibir especificaciones para una serie de tipos de datos de uso común.
Los que hemos elegido son típicos de los que son discutidos en un curso sobre estructuras de datos, ver [Horowitz 76]. Por proporcionar estos ejemplos esperamos convencer al lector de que el estilo de especificación que discutimos aquí es especialmente apropiado para diseñar tipos de datos y que cumpla con los dos criterios previamente fijados. En segundo lugar, esperamos que estas especificaciones de ejemplo proporcionen un estándar por el cual se pueden comparar con otros métodos.
Nosotros no pretendemos haber proporcionado especificaciones definitivas de los tipos de datos de ejemplo. Tanto nuestra elección de operaciones como la semántica que asociamos con algunas de las operaciones son algo arbitrarias. En el último apartado indicamos cómo se pueden realizar estas especificaciones más utilizadas para probar la exactitud de las implementaciones y para probar, en tiempo de diseño, grandes sistemas de software.
Sin embargo, desde que estos temas son bastante largos para discutir, limitamos nuestra presentación aquí para una discusión informal de lectura y escritura del tipo de especificaciones de datos. Los temas restantes solo se insinuarán aquí y que son tratados en [Guttag 76b].
Muchas otras personas han estado trabajando en estas áreas relacionadas y nos hemos beneficiado de sus ideas. Una bibliografía útil de este trabajo se da en [Liskov 75]. Algunas de las particulares axiomatizaciones ya han aparecido en la literatura, en particular pilas, colas y conjuntos, consulte [Liskov 75], [Guttag 76a], [Goguen 751 [Standish 73] y [Spitzen 75].
Las especificaciones
¿Cómo se puede describir un tipo de datos sin restringir indebidamente su eventual forma implementada?
Un método es definir el objeto utilizando lenguaje natural y la notación matemática.
Por ejemplo, una pila puede ser definida como una secuencia de objetos (al, ..., an) n>=0, donde solo se permiten inserciones o eliminaciones a su extremo derecho.
Este tipo de definición no es satisfactorio desde el punto de vista informático en donde es preferible definir constructivamente un tipo de dato por definir las operaciones que crean, acumulan y destruyen instancias del tipo.
Dado que los diseñadores de software generalmente saben cómo programar, el uso de un lenguaje de programación para la especificación es especialmente deseable.
Las características que elegimos permiten solo lo siguiente:
- variables libres
- if-then-else expresiones
- Expresiones booleanas
- recursividad
Además restringimos el uso de procedimientos para aquellos que son de valor único y no tienen efectos secundarios. Tenga en cuenta que muchas características normalmente que se presumen que están presentes en los lenguajes de programación convencionales (como la asignación a variables, una declaración de iteración) no están permitidas en este formalismo.
Este enfoque puede parecer tan arbitrario como para eliminar la posibilidad de lograr las metas previamente establecidas, pero en realidad tiene varios puntos fuertes por los que se lo recomienda.
- Primero, el conjunto restringido produce una representación independiente para suministrar una especificación.
- Segundo, las especificaciones resultantes pueden expresar muy claramente los conceptos si el lector se siente cómodo con la lectura de programas recursivos. (Aunque muchos programadores no están tan acostumbrados, una lectura fiel de este documento servirá como tutorial sobre este tema).
- En tercer lugar, la separación de valores y efectos secundarios aporta claridad y simplifica una especificación. Aunque requerir esta separación puede ser demasiado restrictivo para una implementación, los criterios de eficiencia pueden relajarse en la etapa de especificación.
- Cuarto, las características anteriores pueden ser fácilmente axiomatizadas, que es un primer paso necesario para realizar con éxito pruebas de implementación, ver [Guttag 76b].
Comencemos con un ejemplo muy simple de una pila que está dada en la Figura 2.1.
Las operaciones que están disponibles para manipular una pila son:
- NEWSTACK, que produce una instancia de una pila vacía;
- PUSH, que inserta un nuevo elemento en la pila y devuelve la pila resultante;
- POP, que elimina el elemento superior y devuelve la pila resultante;
- TOP, que devuelve el elemento superior de la pila;
- ISNEWSTACK, que prueba si una pila está vacía.
Para cada operación, los tipos de entradas y salidas son enumerados en la sentencia de la declaración. Observe que todas las operaciones son verdaderas funciones que devuelven un valor único y no permiten efectos secundarios. Si las operaciones de pila se implementan mediante procedimientos con efectos secundarios, su efecto se puede especificar fácilmente en términos de las operaciones que se han dado. La extensión del formalismo de esta manera se analiza en la sección 3.
En este punto, introduzcamos las convenciones de notación que se utilizan a lo largo de este documento.
- Todos los nombres de las operaciones están escritos en mayúsculas.
- Los nombres de los tipos comienzan con una letra mayúscula, por ejemplo, Pila. Minúscula
- Los símbolos se consideran variables libres, como s e i en la figura 2.1. que se toman como de tipo Pila y artículo respectivamente.
- Los nombres de tipo se pueden modificar enumerando "parámetros" dentro de corchetes. Estos parámetros pueden ser nombres de tipos o variables libres cuyo rango es un tipo, por ejemplo , el elemento es una variable e indica que el tipo Pila puede aplicarse a cualquier otro tipo de datos . Las ecuaciones dentro de for all y final son los axiomas que describen la semántica de las operaciones.
Al principio, estos axiomas pueden resultar difíciles de comprender. Una ayuda consiste en interpretar los axiomas como la definición de un conjunto de funciones recursivas.
La pila vacía está representada por la función con entrada sin argumentos NEWSTACK. Luego preguntando por el elemento superior de NEWSTACK se considera una condición excepcional que no dan como resultado un elemento, por lo tanto, lo llamamos INDEFINIDO. La única otra pila que podemos tener debe ser de la forma PUSH (s, i) donde s es cualquier pila e i es el elemento insertado más recientemente.
Luego por la línea 12 el último elemento insertado es el primero devuelto. Note que no debemos preocuparnos por expresiones de la forma TOP (POP (s)), ya que los axiomas 9 y 10 nos dan reglas para expresar cualquier valor de tipo Pila en términos de NEWSTACK y PUSH.
Desafortunadamente, el ejemplo de la pila es demasiado simple al respecto para ilustrar adecuadamente las complejidades de la especificación de tipo de datos. Un ejemplo algo más rico es el tipo de datos Oueue o lista de primero en entrar, primero en salir. Su especificación se da en la Figura 2.2. Ahí son seis operaciones, cuatro de las cuales producen colas, una devuelve un elemento y otra tiene valor booleano. Los axiomas de la cola son más complejos que los axiomas de una pila en el sentido de que hacen uso de la construcción if-then-else y recursión.
Una forma fácil de entender estos axiomas es concebir el conjunto de todas las colas como representado por el conjunto de cadenas que consta de
NEWQ o ADDQ (... ADDQ (ADDQ (NEWQ, it), i2), ..., in), n> l.
El artículo i1 está en la parte delantera y en la parte trasera. Entonces los axiomas pueden ser concebidos concretamente como reglas que muestran cómo cada operación actúa sobre cualquier cadena de este tipo. Por ejemplo, tomando el FRONTQ de la cola vacía es INDEFINIDA. De lo contrario, FRONTQ se aplica a una cola cuyo elemento insertado más recientemente es i, y q representa el resto de la cola. Si q está vacío, entonces i es el resultado correcto, de lo contrario, FRONTQ se aplica recursivamente a q. Una situación similar se mantiene para la operación DELETEQ. Tenga en cuenta que ninguna de las formas de representación de la cola, por ejemplo, como listas enlazadas o en una matriz, es implícito ni excluido por esta definición.
Consideremos una tercera estructura familiar, el árbol binario (Btree) y examinar con más detalle la virtud de considerar todos los valores de la estructura de datos representada por cadenas. Su especificación se da en la Figura 2.3.
Las operaciones incluidas son EMPTYTREE que crea el árbol vacío, MAKE, que une dos árboles con una nueva raíz y operaciones que acceden a los datos en un nodo, el subárbol izquierdo y el subárbol derecho de un nodo y busque un elemento de datos determinado. Tres operaciones que, naturalmente, podríamos preguntarnos si incluir los métodos de recorrido son habituales, preorder, inorder y postorder, que coloque los elementos contenidos en el árbol en una cola [Horowitz 76].
Quizás la razón más poderosa para incluirlos es el hecho de que están expresados de manera tan sucinta por nuestra notación recursiva, por ejemplo,
INORD(Btree) -* Queue y
INORD(EMPTYTREE) = NEWQ
INORD(MAKE(I,d,r)) = APPENDQ(ADDQ(INORD(I),d),INORD(r))
Para cada I,r perteneciente a Btree y d perteneciente a item. La elección de qué operaciones incluir en una especificación es arbitraria. Hemos omitido esto operación porque hace un uso significativo de las operaciones de otro tipo de datos: Cola. De todos modos, esto nos da la oportunidad de experimentar con la representación de cadenas.
Hagamos un ejemplo que comienza con el árbol binario.
T = MAKE(MAKE(EMPTYTREE,B,EMPTYTREE),A,
MAKE(EMPTYTREE,C,EMPTYTREE))
y aplica los axiomas a INORD (T) para obtener
INORD (T) = APPENDQ (ADDQ (INORD (MAKE (EMPTYTREE, B, EMPTYTREE)), A) INORD (MAKE (EMPTYTREE, C, EMPTYTREE)))
que por la definición de INORD se convierte en
APENI ~ Q (ADDQ (APENDQ (ADDQ (NEWQ, B), NEWQ), A), APENDQ (ADDQ (NEWQ, C), NEWQ))
y ahora usando los axiomas para APPENDQ obtenemos
APENDQ (ADDQ (ADDQ (NEWQ, B), A), ADDQ (NEWQ, C)) y nuevamente aplicando APPENDQ
obtenemos
ADDQ(APPENDQ(ADDQ(ADDQ(NEWQ,B),A),NEWQ),C) lo cual nos lleva al resultado final
ADDQ(ADDQ(ADDQ(NEWQ,B),A),C)
EMPTYFILE o WRITE (WRITE (, .. (EMPTYFILE, r 1), ..., rn) o
Una especificación de Polinomios como un tipo de datos con once operaciones en la Figura 2.8.
P (var x, uar y) - x * - F (x, y), y <- G (x); H (x, y).
En algunos casos, estas últimas operaciones ya no serán accesibles por el usuario del tipo de datos. Las llamamos funciones ocultas e indíquelos colocando una estrella junto a su nombre.
En este punto, el lector ha visto tres ejemplos y estamos en una mejor posición para argumentar las virtudes de la notación de especificación.
El número de axiomas está directamente relacionado con el número de operaciones del tipo que se describe. La restricción de expresar axiomas usando solo el if-then-else y la recursividad no ha causado ninguna contorsión.
Esto no debería sorprender a los programadores LISP que han encontrado estas suficientes características muchos años de programación. Una crítica que uno generalmente se encuentra es que la recursividad obliga a uno a un código ineficaz, como el evidenciado por la operación FRONTQ que encuentra el elemento frontal de la cola comenzando en el último elemento. A esto respondemos que una especificación no debe verse como una descripción del eventual programa implementado, sino simplemente como un medio para comprender la operación que está por hacer.
Un segundo comentario supone que los nombres de la operación no están bien elegidos y luego se pregunta ¿Qué tan fácil es es revelar su significado a través de los axiomas?. Esto es difícil de responder, especialmente cuando se trata de imaginar cómo otras técnicas serían justamente bajo esta restricción. Sin embargo, podríamos preguntarle al lector si él puede determinar qué hace la operación MISTERIO donde:
MYSTERY(Queue) --> Queue and
MYSTERY(NEWQ) --> NEWQ
MYSTERY(ADDQ(q,i)) --> APPENDQ(ADDQ(NEWQ,i),MYSTERY(q))
Consideremos otro tipo familiar: String. En la especificación de la Figura 2.4, hemos elegido cinco operaciones primitivas:
NULL, que crea la cadena nula; ADDCHAR, que agrega un carácter a una cadena; CONCAT, que une dos hilos; SUBSTR (s, i, j), que de una cadena s devuelve la subcadena de caracteres j comenzando en el i-ésimo carácter de s; INDICE (s, t), que devuelve el posición de una cadena t como subcadena de una cadena s (0 si t no es una subcadena de s).
Tenga en cuenta que existen varios tipos que componen esta definición además del tipo String; a saber, Carácter, Entero y Booleano. En general, una especificación de tipo de datos siempre define solo un tipo, pero se puede requerir en las operaciones de otros tipos de datos para lograr esto.
Otra pregunta que surge de nuevo es ¿Cuándo debería una operación ser parte de la especificación y cuándo no debería serlo?, problema que ya hemos encontrado con árboles binarios. Las operaciones que hemos elegido aquí son básicamente las que se proporcionan en PL / I.
Hasta ahora nos hemos concentrado principalmente en cómo leer los axiomas. Ahora consideremos cómo crearlos. Como esquema general de ataque, comenzamos con un conjunto básico de operaciones fl, ..., fm. Un subconjunto de estos, digamos 'fl, ..., fk k_ <m, tienen como salida el tipo de datos que es definido. De las k operaciones se elige un subconjunto que llamamos el conjunto de constructores que satisface la propiedad de que todas las instancias de los tipos de datos se pueden representar utilizando solo operaciones de conjuntos de constructores. Entonces, los axiomas que deben escribirse son los que muestran cómo cada operación de conjunto no constructor se comporta en todas las instancias posibles de tipo de datos.
Como un nuevo ejemplo, considere el tipo Set. Las operaciones cuyo rango es de tipo Set son:
EMPTYSET que tiene el habitual sentido; INSERT y DELSET que ponen un elemento en uno o lo eliminan del conjunto respectivamente. De estas tres operaciones seleccionamos EMPTYSET e INSERT como constructores. Entonces un conjunto arbitrario que contiene n_> 1 elementos viene dado por la expresión
INSERT(...INSERT(EMPTYSET,i 1 ,),...,in).
Una característica muy importante de esta definición es el hecho de que no existe pedido asumido en los artículos. Alternativamente, la especificación podría insistir en que il <i2 <... <in también sea cierto. Una especificación anterior de un conjunto que asumió que se dio un pedido en [Zilles 75].
El tipo de gráfico de la figura 2.6 es interesante en varios aspectos. La definición matemática de un gráfico es generalmente en términos de dos conjuntos: nodos y aristas. Esto se refleja en los constructores de esta definición que son EMPTYGRAPH, ADDNODE y ADDEDGE. Esta definición permite un gráfico no conectado y para nodos sin incidentes en sus bordes. Una arista está dada por la función REL (i, j) (un constructor del borde del tipo de datos) y no se especifica si los bordes están dirigidos o no.
Observe que tres de las operaciones resultado en conjuntos y la notación de parámetros ha sido naturalmente extendida para distinguir entre conjuntos con diferentes tipos de elementos. ADJAC encuentra todos los nodos adyacentes a algún vértice. NODOUT (g, v) elimina el nodo v y todos los bordes incidentes a v. EDGEOUT elimina un solo borde del gráfico.
El siguiente ejemplo es un tipo de datos de archivo secuencial (Figura 2.7). Las operaciones incluyen READ, WRITE, RESET, ISEOF (fin de archivo check) y SKIP (más allá de un número específico de registros).
Las operaciones secuenciales de archivos no serían, en la práctica, implementados como funciones, sino más bien como procedimientos con efectos secundarios, diga READP (f, r) y WRITEP (f, r).
Las operaciones que hemos dado pueden utilizarse para especificar los efectos de estos procedimientos:
READP (f, r) significa r <- LEER (f), f ~ SALTAR (f, 1); y WRITEP (f, r) significa f <- WRITE (f, r).
Nota: Los axiomas implican que si una operación SKIP sigue inmediatamente a una de ESCRIBIR, significa restablecer el archivo a su comienzo, luego saltar más allá de i registros. Además, si se sobrescribe un registro, la parte del archivo más allá se pierde el registro. Para un estudio más detallado de los axiomas, tenga en cuenta que todos los valores de archivos se pueden ver como una de las siguientes formas de cadena:
EMPTYFILE o WRITE (WRITE (, .. (EMPTYFILE, r 1), ..., rn) o
SKIP (WRITE (WRITE (..., (EMPTYFILE, r 1,), ..., rn), i).
donde x es un indeterminado y el ai proviene de algún anillo conmutativo. Si am fO entonces m se llama grado, am el coeficiente principal, y am_lxm-l + ... + alx + a 0 el reductum.
Concluimos este apartado con una presentación de tipo Polinomio. La definición matemática habitual de un polinomio es una expresión de la forma:
Una especificación de Polinomios como un tipo de datos con once operaciones en la Figura 2.8.
En esta especificación cada polinomio es CERO o construido aplicando ADDTERM a un polinomio.
Nota: La ausencia de supuestos sobre el orden de los exponentes, distintos coeficientes de cero, etc., que son importantes como decisiones de representación pero no es esencial para la especificación.
La verdadera virtud de esta especificación es que un sistema bastante complejo el objeto se ha definido completamente utilizando solo unas pocas líneas. los programas correspondientes en un lenguaje de programación convencional pueden ser varias veces este tamaño. (Esto será especialmente cierto si algunos de se utilizan los algoritmos "rápidos".)
Procedimientos y tipos finitos
Hasta ahora todos los tipos de datos abstractos que tenemos axiomatizados han sido infinitos. Es relevante observar un paralelo aquí entre la informática y las matemáticas, que los tipos finitos a menudo son más difíciles de definir que los infinitos. Esta sección tiene la intención de hacer frente a las complicaciones añadidas de especificar más tipos de datos realistas. En particular, investigamos cómo especificar un tipo de tamaño finito. Al mismo tiempo relajaremos la restricción que todas las operaciones sean de un solo valor y permitan una notación que se asemeja al uso convencional de procedimientos. Esta notación fue introducida por primera vez en [Guttag 76b].
Ahora será permisible incluir procedimientos en las especificaciones. Un procedimiento P cuyo primer argumento, x, se modifica como un resultado de su ejecución pero no su segundo argumento y, es declarada sintácticamente como P (var x, y). Si P es un procedimiento puro, es decir, no devuelve ningún valor, entonces esto se expresa sintácticamente escribiendo P (var x, y) ->. La definición del procedimiento P se incluirá en la especificación semántica del tipo de datos. Un procedimiento tiene cuerpo y una parte de valor opcional separada por un punto y coma, p. ej.
P (var x, uar y) - x * - F (x, y), y <- G (x); H (x, y).
es una posible definición de P donde F, G, H son funciones y H devuelve un valor, observe que la asignación simultánea a los parámetros ahora es permitido, pero seguimos adhiriéndonos a nuestro enfoque anterior al requerido que cada procedimiento sea expresado por funciones de un solo valor.
En algunos casos, estas últimas operaciones ya no serán accesibles por el usuario del tipo de datos. Las llamamos funciones ocultas e indíquelos colocando una estrella junto a su nombre.
Como ejemplo, damos en la Figura 3.1 la especificación de un cola de tamaño finito. Nótese que en comparación con la cola infinita de la Figura 2.2 se han agregado cuatro nuevas operaciones. ADDQ y DELETEQ ahora se designan como funciones ocultas y en su lugar el usuario aplicará el procedimiento puro ENQ y la función DEQ, los cuales tienen el efecto secundario de alterar su primer argumento. Observe también que hemos aumentado el valor INDEFINIDO operación permitiendo que sea calificado. Esto facilitará la manejo de errores distinguiendo su origen.
Otras direcciones
En este artículo hemos destacado el arte de la especificación de tipo de datos. Nuestro principal objetivo ha sido explorar una notación que sea especialmente atractiva para definir formalmente un tipo de datos sin tener en cuenta a su implementación. En esta sección queremos indicar brevemente cómo estas especificaciones se pueden utilizar para diseñar software confiable, pero para una discusión completa de especificación reservadas en [Guttag 76b].
El primer uso de una especificación axiomática es como una ayuda al diseñar e implementar el tipo. Se toma la decisión de elegir un forma particular de implementación. Esta implementación estará en términos de otros tipos de datos y asumimos que sus especificaciones ya existen. Para un tipo de datos complejo, este proceso puede continuar a través de varios niveles antes de que una implementación ejecutable sea lograda. La virtud de las especificaciones es que cada etapa se realiza más claro organizando los tipos, valores y operaciones que se pueden usar.
Un segundo uso de estas especificaciones y quizás su mayor importe, es para demostrar que una implementación es correcta.
Establecer la corrección ahora equivale a mostrar que los axiomas originales se satisfacen con la implementación recién desarrollada. A menudo es posible eludir la necesidad de inducción y, en cambio, una sencilla manipulación de la fórmula resulta suficiente. Esta el proceso también se presta con bastante facilidad a la automatización. Este trabajo es descrito en [Guttag 76b].
Otro uso de estas especificaciones es para pruebas tempranas. Eso sería muy deseable si uno pudiera diseñar un sistema de tal manera que podría probarse antes de comprometer a la gente a construirlo.
Dadas las restricciones adecuadas sobre la forma en que las ecuaciones axiomáticas puede tomar, un sistema en el que implementaciones y algebraicos se pueden construir de especificaciones de tipos de datos intercambiables.
En ausencia de una implementación, las operaciones del tipo de datos pueden interpretarse simbólicamente. Por lo tanto, a excepción de una pérdida significativa en eficiencia, la falta de una implementación se puede hacer completamente transparente para el usuario. Curiosamente no es necesario gastar muchos años-hombre desarrollando este sistema. La capacidad es esencialmente disponible en sistemas de manipulación de símbolos basados en LISP como SCRATCHPAD [Griesmer 71], REDUCE [Hearn 71] y MACSYMA [Martín 71]. El uso de REDUCE para este propósito se discute en [Guttag 76b], que también analiza las ideas esenciales de un patrón compilador de coincidencias diseñado especialmente para la compilación de axiomas algebraicos .
Agradecimientos
Varias personas hicieron comentarios valiosos sobre borradores anteriores de este paper, incluidos Ralph London, Mary Shaw, Tim Standish, Dave WIle y los árbitros. Agradecemos a Betty Randall por su experiencia. y paciencia para mecanografiar muchos borradores del documento.
Referencias
[Dahl 70] OJ Oahl, B. Myhrhaug y K. Nygaard, "The SIMULA 67 idioma base común, "Norwegian Computing Center, Oslo, Publicación S-22, 1970.
[Dahl 72] OJ Dahl, EW Dijkstra y CAR Hoare, Strctctred Programación, Londres: académico, 1972, págs. 1-82.
[Goguen 75] JA Goguen, JW Thatcher, EG Wagner y JB Wright, "Tipos de datos abstractos como álgebras iniciales y exactitud de las representaciones de datos, actas, conferencias sobre gráficos por computadora, reconocimiento de patrones y datos Estructura, mayo de 1975.
[Griesmer 71] JH Griesmer y RD Jenks, SCRATCHPAD / Z -Una instalación interactiva para las matemáticas simbólicas " Proc. Segundo Simposio de Simposio y Algebraico Manipulation, ACM, marzo de 1971, págs. 42-58.
[Guttag 75] JV Guttag, "La especificación y aplicación para programación de tipos de datos abstractos, "Ph. D. Thesis, Universidad de Toronto, Departamento de Ciencias de la Computación, 1975, disponible como Informe de investigación de sistemas informáticos CSRG-59.
[Guttag 76a] JV Guttag, "Tipos de datos abstractos y desarrollo de estructuras de datos, "Suplemento del Actas de la Conferencia SIGPLAN / SIGMOD sobre Datos: abstracción, definición y estructura, marzo de 1976, págs. 37-46.
[Guttag 76b] JV Guttag, E. Horowitz y DR Musser, "Tipos de datos abstractos y validación de software", USC Informe técnico del Instituto de Ciencias de la Información, 1976.
[Hearn 71] AC Hearn, "Reduce 2: un sistema y un idioma para manipulación algebraica, " Proc. Segundo Simposio sobre Manipulación simbólica y algebraica, ACM, marzo de 1971, págs. 128-133.
[Horowltz 76] E. Horowitz y S. Sahni, Fundamentos de datos Estructuras, Computer Science Press, junio de 1976.
[Liskov 75] BH Liskov y $. N. Zilles, "Especificación técnicas de abstracción de datos, " Transacciones IEEE en Ingeniería Softusare, Vol. SE-I, No. 1, marzo de 1975, págs. 7-18.
[Martin 71] WA Martin y RJ Fateman, "The MACSYMA sistema, " Proc. Segundo Simposio sobre Simbólicos y Algebraicos Manipulation, ACM, marzo de 1971, págs. 59-75.
[McCarthy 63] J. McCarthy, "Base para una teoría matemática de comlbutation, "en CotTtptLter Programming and Formal Systems, P. ~ Braffort y D. Hirchberg (eds.), North-Holland Publishing Compañía, 1963, págs. 33-70.
[Parnas 72] DL Parnas, "Una técnica para la especificación de módulos de software con ejemplos, " Comm. ACM, VoI. 15, págs. 330-336, mayo de 1972.
----------
Esta investigación fue apoyada en parte por Defense Research Agencia de Proyectos bajo contrato No. DAHC15 72 C 0308 y por el National Science Foundation bajo contrato No. MCS76-06089. Las opiniones expresadas son las de los autores.
* Departamento de Ciencias de la Computación, USC, Los Ángeles, CA 90007
** Instituto de Ciencias de la Información de la USC, 4676 Admiralty Way, Marina del Rey, CA 90291
