Buscar este blog

jueves, 24 de febrero de 2011

Especificacion algebraica

Método axiomático o algebráico 

La semántica de las operaciones se define a través de un conjunto de axiomas.
Un axioma es una regla que establece la igualdad de dos expresiones: <Expresión 1> = <Expresión 2>
Por ejemplo:




Suma (dos, dos) = Producto (dos, dos)

Supongamos un TAD, T. Los tipos de operaciones son:
  • Constructores: conjunto mínimo de operaciones del TAD, a partir del cual se puede obtener cualquier valor del tipo T.
  • Modificación: a partir de un valor del tipo obtienen otro valor del tipo T, y no son constructores.
  • Consulta: devuelven un valor que no es del tipo T.
Ademas, una especificación es :
  • completa si de cualquier expresión se puede encontrar otra más sencilla, con operaciones de construcción.
  • correcta si a partir de una expresión sólo se puede obtener un resultado final.
Para conseguir que una especificación sea completa y correcta, hay que definir los axiomas suficientes para relacionar las operaciones de modificación y consulta con los constructores. Y no incluyendo axiomas que se puedan deducir de los otros ya descritos.
Ejemplo: TAD Números Naturales:
NOMBRE natural CONJUNTOS N conjunto de naturales, B conjunto de valores booleanos SINTAXIS
cero: → N
   sucesor: N → N
   escero: N → B
   igual: N x N → B
   suma: N x N → N
semantica para todo m y n pertenecientes a N
1. escero (cero) = true
     2. escero (sucesor (n)) = false
     3. igual (cero, n) = escero (n)
     4. igual (sucesor (n), cero) = false
     5. igual (sucesor (n), sucesor (m)) = igual (n, m)
     6. suma (cero, n) = n
     7. suma (sucesor (m), n) = sucesor (suma (m, n))



ESPECIFICACIÓN ALGEBRAICA DE TIPOS ABSTRACTOS DE
DATOS.


TIPO DE DATOS: Es un conjunto de estados o valores permitidos, junto con las
operaciones que trabajan sobre tales estados, cuando pertenecen a ese tipo concreto.
Esto es así porque un mismo estado puede pertenecer a tipos diferentes; p.ej., el nº 4,
puede ser un entero, un real, un complejo, un racional o un natural.
El usuario puede construir sus propios tipos de datos en un lenguaje determinado,
mediante las construcciones sintácticas que se le den para ello.
Así, las estructuras de datos se crean usando constructores predefinidos, (de especial
utilidad son los registros y matrices), junto con los tipos que suministra el lenguaje: REAL,
INTEGER, CARDINAL, BOOLEAN, etc. Los tipos de datos definidos por el usuario también
se pueden usar para crear otras estructuras de datos más complejas. Ej.:
TYPE
Persona = RECORD
Nombre : ARRAY [0..23] OF CHAR;
Apellidos : ARRAY [0..29] OF CHAR;
DNI : ARRAY [0..9] OF CHAR;
END;
VAR
Censo : ARRAY [1..1000] OF Persona;
La variable Censo es una estructura más compleja formada sobre otra (Persona), definida
por el usuario.
Un TIPO ABSTRACTO DE DATOS permite la construcción de casi cualquier tipo de
datos, atendiendo sólo a criterios de comportamiento, y sin relacionarlo para nada con la
representación subyacente que nos permita su puesta en ejecución según las funcionalidades
particulares que un lenguaje de programación dado nos pueda suministrar. Su objetivo es hacer
referencia a una clase de objetos (conjunto de estados) definidos por una especificación

independiente de la representación. La implementación del tipo se oculta al usuario del
programa.
La diferencia entre Tipo de Datos y T.A.D. es que el TAD se centra sólo en el
comportamiento, no en la implementación. Es algo así como una caja negra. Dice el qué y no el
cómo, aunque por supuesto, el qué tiene que ser viable. Así, se pueden utilizar diferentes cómos,
dando al programador la potestad para seleccionar el que más le convenga, pero sin alterar en
ningún momento el comportamiento del TAD, ni, por supuesto, su interfaz con el exterior, que
será siempre la misma, (ya que formalmente se trata del mismo tipo de datos). Así pues, la
separación de la especificación de la implementación de un TAD permitiría la existencia de
varias implementaciones equivalentes, dándole al programador la posibilidad de cambiar la
implementación sin que esto tenga ningún efecto en el resto del sistema.
Juegan un papel muy importante en el desarrollo de software seguro, eficiente y flexible,
ya que cuando usamos un TAD definido por otro programador, podemos concentrarnos en las
propiedades deseadas de los datos, y en la funcionalidades que nos suministran. Por cuestiones
de Correctitud y fiabilidad, es muy importante la correción formal de un TAD; también hay que
prestar especial atención a la definición formal en el caso de precondiciones anómalas por
cuestiones de Robustez.
Nosotros vamos a utilizar una notación formal para especificar el comportamiento de los
TADes.
La primera ventaja que se consigue usando TADes en el diseño de programas es que
conllevan el conseguir programas estructurados y modulares. Este tipo de modularidad asegura
que las tareas lógicas y los datos se agrupan para formar un módulo independiente cuya
especificación funcional es visible a otros programas que lo usan. Estas aplicaciones no necesitan
información detallada de cómo están implementadas las tareas y los datos. Esto hace que
podamos implementar estas operaciones y tipos de datos de diferentes formas, siempre que se
ajusten a las especificaciones. Esta separación de especificaciones e implementación asegura que
muchas decisiones de diseño, como eficiencia, consenso entre velocidad y ocupación de
memoria, etc., puedan tomarse en una etapa posterior, cuando se ha probado que las propiedades
lógicas de los tipos de datos y sus operaciones satisfacen la aplicación. Para todo ello es muy útil
la compilación separada, que nos permite verificar la corrección de los interfaces definidos,
antes de proceder a la implementación propiamente dicha de los TADes.
En definitiva, con el concepto de TAD conseguimos crear una especificación formal
mediante la cual el implementador no tenga duda alguna sobre las características del producto
software que se le está pidiendo que desarrolle. La siguiente figura ilustra a grandes rasgos este
proceso.

No hay comentarios:

Publicar un comentario