Usa: Declara si se utilizan otros TADs previamente definidos
Tipos: define el nombre de los tipos que se declararan en la especificación
Operaciones: describe las funciones que tendrán los tipos definidos, declarando los parámetros que tendrán de cada función, y el tipo del valor devuelto. Únicamente describe su sintaxis, sin entrar en su comportamiento.
Ecuaciones: Dadas las operaciones anteriores, describe su semántica. Es decir, con la declaración anterior una función puede tener cualquier comportamiento con tal de que respete los parámetros, sus tipos, y el tipo resultante, con las ecuaciones se describe cual será el comportamiento de dichas operaciones ante los datos.

        Especificación Booleanos
            tipos bool
            operaciones
                    cierto: -> bool                   significa que "cierto" es una operación que devuelve una booleano
                falso: -> bool
                y: bool x bool -> bool        significa que "y" recibe dos valores booleanos y devuelve otro booleano
                o: bool x bool -> bool
                no: bool -> bool
            ecuaciones
                y (cierto, x) = x
                y (falso, x) = falso
                o (cierto, x) = cierto
                o (falso, x) = x
                no (falso) = cierto
                no (cierto) = falso
        Fespecificación

No se ha definido el apartado "usa" ya que no se utiliza ningún otro tipo de datos dentro de la especificación. Se pueden definir diferentes especificaciones para un mismo tipo de datos (por ejemplo podríamos haber elegido otras ecuaciones u otros nombres para las operaciones), por ello a le especificación le damos un nombre, en nuestro caso Booleanos, y también damos un nombre al tipo declarado, bool en el ejemplo.

En la especificación anterior, si sólo dispusiéramos del apartado operaciones cualquier tipo de datos que cumpla la sintaxis dada sería válido; por ejemplo un tipo en el que y(falso,falso)=cierto o que no(cierto)=cierto sería válido ya que ambas ecuaciones respetan la sintaxis definida para las operaciones, pero no satisface el concepto de tipo booleano que tenemos. Para ello se añade el apartado de ecuaciones en que se describe la semántica del tipo, es decir se describe cómo deben comportarse las operaciones. Por ejemplo si tenemos la expresión booleana:

          cierto y  no (cierto  o  falso)

lo representaremos en la sintaxis definida como

           y (cierto, no (o (cierto, falso))

y si aplicamos las ecuaciones definidas podemos concluir:

            y (cierto,  no (o (cierto, falso))
            y (cierto,  no ( cierto           )        aplicando la tercera ecuación
            y (cierto,        falso             )        aplicando la última ecuación
                                   falso                       aplicando la primera ecuación

Por tanto la expresión puesta como ejemplo es equivalente a falso que es lo que esperaríamos en un tipo booleano.

Clasificación de las operaciones

En primer lugar distinguiremos entre los diferentes tipos de operaciones, lo que nos facilitará posteriormente la definición de ecuaciones:

Operaciones constructoras: operaciones que devuelven valores del tipo que se está especificando
Operaciones consultoras: operaciones con al menos un argumento del tipo en especificación pero que devuelven valores de otro tipo.

Generadoras: operaciones necesarias para generar todos los valores del tipo especificado, y que si se excluye alguna no es posible generar todos. Puede haber diferentes conjuntos de generadoras.
Modificadoras: constructoras no generadoras

puro: todo par de términos diferente generado únicamente por las generadoras denota valores diferentes
impuro: dos o más términos diferentes denotan un mismo valor

       Especificación MisNaturales
       usa Booleanos            utilizaremos el tipo bool definido en el TAD Booleanos
            tipos natural
            operaciones
                    cero: -> natural
                suc: natural -> natural
                suma: natural x natural -> natural
                igual: natural x natural -> bool
       ecuaciones
                ...
      Fespecificación

Puede verse fácilmente que las tres primeras operaciones son constructoras, ya que devuelven valores de tipo "natural", y la última es modificadora, ya que devuelve un valor de tipo booleano. Además interpretando "cero" como el valor habitualmente representamos como 0, y "suc" como el sucesor de un número dado, con dichas operaciones pueden generarse todos los valores de los  naturales: cero-0, suc(cero)-1, suc(suc(cero))-2, .... Teniendo en cuenta además que omitiendo cualquiera de ellas no podemos generar todos los valores, queda claro que dichas dos operaciones son generadoras. La operación "suma" por tanto es modificadora; y por último, "igual", al devolver un valor de tipo booleano, es consultora.

Por otro lado las generadoras son puras porque cada término producido por las generadoras es único, es decir, no hay dos términos diferentes que representen valores iguales, es decir, cero =/= suc(cero) =/= suc(suc(cero)) =/= ....

Nota: Cuando utilicemos varios TAD en el apartado "usa" puede darse el caso de que varios utilicen un mismo nombre para una misma operación, o que uno de ellos utilice un nombre igual a una operación del tipo que se está definiendo. Para evitar ambigüedades siempre que se haga referencia a una operación o tipo de otro TAD deberíamos antecederlo por el nombre de la especificación (p.e. Booleanos.bool, Booleanos.no, ...), pero para mayor legibilidad lo omitiremos cuando no sea ambiguo (p.e. bool, no, ...).

Escritura de ecuaciones

Para escribir las ecuaciones seguiremos el siguiente proceso:

1. Identificar el conjunto de operaciones constructoras generadoras, si hay varios conjuntos posibles elegir uno
2. Si no es puro, seleccionar los términos que representen cada clases, es decir elegir el término que actúe como canónico. A continuación escribir las ecuaciones que hagan congruentes los términos generados por las generadores, es decir que iguale los términos que representan los mismos valores igualando los términos no canónicos con los canónicos. Las ecuaciones únicamente utilizarán operaciones generadoras.
3. Si el conjunto de generadoras es puro, no hay que escribir ecuaciones entre ellas.
4. Para cada una de las operaciones modificadoras se deben escribir ecuaciones para hacer los términos generados por ellas congruentes con términos formados por generadoras. Es decir hay que hacer que cada término que usa modificadoras se pueda transformar en un término que únicamente contenga generadoras, o modificadoras para las cuales ya hemos escrito ecuaciones y podemos transformarlas en generadoras.
5. Para cada consultora se debe escribir ecuaciones para que los términos sean congruentes con las constructoras de su tipo, es decir, se debe hacer lo mismo que en el punto anterior para el tipo que se genera.

        sean "x" e "y" dos naturales

            suma (cero, x) = x
            suma (suc (x), y) = suma (x, suc (y))

con estas dos ecuaciones cualquier término que utilice la operación "suma" puede transformarse en un término formado sólo por generadoras. Si el primer parámetro es de la forma "suc(suc(suc(....suc(cero)...)))" aplicamos sucesivamente la segunda ecuación hasta que dicho parámetro se convierta en "cero", en cuyo momento aplicamos la primera ecuación, desapareciendo la modificadora.

Por ejemplo:

            suma (suc (suc (cero)),     suc (cero))
            suma (suc (cero)), suc (suc (cero)))
            suma (cero,    suc (suc (suc (cero)))
            suc (suc (suc (cero)))

por tanto los términos "suma(suc(suc(cero)), suc(cero))" y "suc(suc(suc(cero)))" son congruentes, es decir representan el mismo valor (visto numéricamente suma(2,1)=3 ).

Ejercicio: Escribir una ecuación alternativa para la segunda ecuación de la suma. Solución

Ejercicio: rellenar las ecuaciones siguientes de la igualdad entre naturales

            igual (cero, cero) =
            igual (suc (x), cero) =
            igual (cero, suc (x)) =
            igual (suc(x), suc (y))=

        y escribir una alternativa a la tercera ecuación, utilizando la conmutatividad. Solución

Ejercicio: crear una nueva operación "menor" y escribir las 3 ecuaciones que la definen.

Puede comprobarse la potencia de la especificación ecuacional, viendo cómo se ha definido el conjunto infinito de los números naturales únicamente con dos operaciones (cero y suma), y cómo simplemente por medio de dos ecuaciones se ha definido completamente la suma de dos naturales.

Ejercicio: el alumno debe especificar los naturales utilizando la sintaxis habitual con 10 símbolos constantes (0, 1, ...9), dando las reglas de combinación de dichos símbolos para crear nuevos naturales (22, 112, 69) y resolviendo la ambigüedad de los números equivalentes (1 = 0001), y a continuación deberá describir completamente las suma entre naturales, por ejemplo dando tanto las tablas de suma entre números simples, y las reglas de suma entre números de varias cifras. Por último deberá comparar las hojas utilizadas para dicha especificación con las 5 líneas de la especificación ecuacional.

Supongamos que especificamos los enteros con las siguientes operaciones:

            cero: -> entero
            uno: -> entero
            suc: -> entero
            pred: -> entero
            suc2: -> entero
            pred2: -> entero
            ...

interpretándose que "uno" es el sucesor de cero, "pred" devuelve el predecesor de un número y que "suc2" y "pred2" devuelven valores 2 veces superiores o inferiores, p.e.: suc2(5)=7

Evidentemente hay varios posibles conjuntos de generadoras: {cero, suc, pred}, {uno, suc, pred}, {cero suc, pred2}, ... por tanto primero debemos elegir uno.

El conjunto {cero, uno, suc, pred} no sería generador, porque si bien puede generar todos los posibles valores podemos eliminar una operación, uno o cero y seguir generando todos los valores. El conjunto {cero, pred2, suc2} tampoco lo es porque no permite generar todos los posibles valores.

Elijamos como generadoras {cero, pred, suc}.

Ejercicio: ¿Son generadoras puras o impuras? demostrarlo y/o poner un ejemplo que lo demuestre. Solución

Ya que cada clase de términos equivalentes tiene infinitos posibles representantes, elegiremos como términos canónicos, representantes de la clase, a los más sencillos, es decir: cero, pred(cero)), pred(pred(cero)), ... suc(cero), suc(suc(cero)), ... es decir que no aparezcan la operaciones predecesor y sucesor en el mismo término.

Comenzamos escribiendo ecuaciones para las generadoras, es decir hay que hay que escribir ecuaciones que permitan demostrar por ejemplo que pred(pred(suc(cero))) = pred(cero)

Podemos escribir la ecuación

        pred (suc (cero)) = cero

el problema es que así escrita es muy restrictiva y no es aplicable por ejemplo en pred(suc(pred(cero))) porque la ecuación únicamente se aplica si "suc" antecede a cero. Para ello utilizaremos variables cuantificadas universalmente, con lo que la ecuación queda como:

           pred (suc (x)) = x

Ejercicio: ¿es suficiente esta ecuación para igualar todos los términos equivalentes? demostrarlo y/o poner un ejemplo que lo demuestre. Solución

Por tanto definimos las siguientes ecuaciones para las operaciones generadoras:

        pred (suc (x)) = x
        suc (pred (x)) = x

Ejercicio: definir una ecuación alternativa a la segunda. Solución

A continuación se han de definir ecuaciones para las modificadoras:

        uno = suc (cero)
        pred2 (x) = pred (pred (x))
        suc2 (x) = suc (suc (x))

poniendo las modificadoras en función de las generadoras, nos permite demostrar que son equivalentes términos como pred2(cero) y pred2(pred(suc2(pred(cero))) ya que aplicando las ecuaciones a ambos términos podemos igualarlos a su término canónico pred(pred(cero)).

Y por último se definirían las ecuaciones para las consultoras.

Ejemplo: TAD conjuntos

Especificar el tipo de datos conjunto de naturales, con las operaciones de pertenencia, unión, intersección, cardinal (nº de elementos) y consulta si el conjunto está vacío. Se recuerda que en los conjuntos no hay orden entre los elementos y tampoco hay elementos repetidos, es decir añadir dos veces un elemento es como hacerlo una sola vez.

Ejercicio: escribir las operaciones. Solución

Definidas las operaciones de ha de identificar las generadoras: vacío y añadir.

Ejercicio: ¿Son generadoras puras o impuras? demostrarlo y/o poner un ejemplo que lo demuestre. Solución

La primera ecuación para las generadoras puede ser:

      " C, C2 Î conjunto, " x, y Î natural
        añadir (x, añadir (y, C)) = añadir (y, añadir (x, C))

Ejercicio: ¿hay más términos equivalentes que todavía no queden igualados por las ecuaciones?. Solución

La segunda ecuación sería:

        añadir (x, añadir (x, C)) = añadir (x, C)

que teniendo en cuenta la primera de las ecuaciones no es necesario que los elementos repetidos se introduzcan consecutivamente.

Ejercicio: ¿hay más términos equivalentes que todavía no queden igualados por las ecuaciones?. Solución

A continuación se definen las ecuaciones para la primera de las modificadoras, la Unión.

        unión (vacío, C) =
        unión (añadir (x, C), C2) =

Ejercicio: rellenar las ecuaciones anteriores. Solución

Para especificar la intersección añadiremos precondiciones a la ejecución de las ecuaciones y utilizaremos la operación "pertenece", que lógicamente no podrá utilizar la intersección en su definición u otra operación que dependa de la ella.

Para definir la operación "pertenece" utilizaremos la operación "igual" previamente definida para los naturales, y la operación "no" definida para los booleanos. Por legibilidad a partir de ahora la igualdad entre naturales se expresará como x=y en lugar de "igual(x,y)", y la desigualdad como x=/=y en lugar de "no(igual(x,y))

        pertenece (x, vacío) =
        pertenece (x, añadir (x, C)) =
        x=/=y  ==> pertenece (x, añadir (y, C)) =

Ejercicio: completar las ecuaciones anteriores. Solución

Se debe añadir la precondición de la última ecuación porque al ser para todo "x" e "y", si no se pusiera la precondición también podría aplicarse para el caso de que "x" e "y" fueran iguales, y en dicho caso sólo debería aplicarse la segunda ecuación, donde al poner en ambos lados la "x" es como si se pusiera la precondición "x=y"

Las ecuaciones de la intersección quedan:

        intersección (vacío, C) =
        pertenece (x, C2) ==> intersección (añadir (x, C), C2) =
        no pertenece (x, C2) ==> intersección (añadir (x, C), C2) =

Ejercicio: completar las ecuaciones anteriores. Solución

A continuación escribiremos las ecuaciones para calcular el número de elementos de un conjunto:

        cardinal (vacío) = cero
      cardinal (añadir (x, C)) = suc (cardinal (C))

Por comodidad y legibilidad a partir de ahora se utilizará "0" en lugar de "cero" y "a+b" en lugar de "suma(a,b)".

Ejercicio: La segunda ecuación de cardinal es incorrecta. Justificar cuando y porqué, poner un ejemplo que lo demuestre, y corregirla. Solución

Ejercicio: Escribir las ecuaciones necesarias para decidir si un conjunto está vacío. Solución

Para finaliza escribimos toda la especificación de conjuntos. Debido a que una especificación que únicamente sirva para conjuntos de naturales sería muy restrictiva, y nos obligaría hacer una especificación para cada tipo de elemento que queramos usar, definiremos una especificación para un tipo genérico "elemento", especificación que después podrá ser instanciada para el tipo concreto que se desee. Supondremos que siempre que se instancie un conjunto para un elemento determinado, previamente se ha especificado dicho elemento y contiene la operación de igualdad.

        Especificación Conjuntos (elemento)
            usa Misnaturales, Booleanos
            tipos conjunto
           operaciones
                vacío: -> conjunto
                añadir: elemento x conjunto -> conjunto
                unión: conjunto x conjunto -> conjunto
                intersección: conjunto x conjunto -> conjunto
                pertenece: elemento x conjunto -> bool
                cardinal: conjunto -> natural
                esvacío: conjunto -> bool
           ecuaciones     " C, C2 Î conjunto, " x, y Î elemento
                añadir (x, añadir (y, C)) = añadir (y, añadir (x, C))
                   añadir (x, añadir (x, C)) = añadir (x, C)
                    unión (vacío, C) = C
                unión (añadir (x, C), C2) = unión (C, añadir (x, C2))
                pertenece (x, vacío) = falso
                pertenece (x, añadir (x, C)) = cierto
                x=/=y ==> pertenece (x, añadir (y, C)) = pertenece (x, C)
                intersección (vacío, C) = vacío
                pertenece (x, C2) ==> intersección (añadir (x, C), C2) = añadir (x, intersección (C, C2))
                no pertenece (x, C2) ==> intersección (añadir (x, C), C2) = intersección (C, C2)
                cardinal (vacío) = 0
                pertenece (x, C) ==> cardinal (añadir (x, C)) = cardinal (C)
                no pertenece (x, C) ==> cardinal (añadir (x, C)) = cardinal (C) + 1
                esvacío (vacío) = cierto
                esvacío (añadir (x, C) = falso
        Fespecificación

Cuando en un TAD deseemos utilizar el tipo conjunto, en lugar de añadir simplemente el nombre de la especificación al apartado "usa" deberemos instanciar el TAD para el tipo deseado, y darle un nuevo nombre. Para utilizar los tipos y operaciones del TAD genérico deberemos antecederlos por el nombre del TAD instanciado (aunque lo omitiremos si no hay ambigüedad)

Por ejemplo si deseamos utilizar un conjunto de naturales pondremos:

         usa Conj_nat=Conjuntos (naturales)

donde Conj_nat es un nombre cualquiera, que utilizamos para identificar el nuevo tipo, y para referirnos al tipo y las operaciones deberíamos escribir "Conj_nat.conjunto", "Conj_nat.vacío", "Conj_nat.añadir", ...

Ampliación de la sintaxis de las especificaciones

En algunos casos puede interesar crear una operación que facilite la escritura de las ecuaciones, pero dicha operación no tiene por que ser accesible fuera de la especificación, es decir, una operación exclusivamente para la escritura de la especificación misma. En ese caso diremos que la operación es "privada". Puede añadirse tantas operaciones privadas como se necesite.

Por ejemplo, si no tuviéramos la operación "pertenece" en los conjuntos, al resultarnos muy útil podemos añadirla al apartado de "operaciones", antecediéndola por la palabra "privada":

         privada pertenece: elemento x conjunto -> bool

Por otro lado, puede darse el caso de que ciertas operaciones no puedan aplicarse en determinadas ocasiones. Para ello antes de las ecuaciones se añadirá un apartado de errores especificando los términos para los cuales sería un error aplicar una operación. La evaluación de las operaciones de error es previa a cualquier otra, es decir, antes de aplicar cualquier ecuación, se comprobará si el término no da lugar a error.

Por ejemplo, si en los conjuntos añadir dos veces un elemento fuera un error, en lugar de simplemente tratarse como una sola inserción, lo pondríamos como:

      error
            añadir (x, añadir (x, C))