Buscar este blog

jueves, 24 de febrero de 2011

Introduccion

Introducción
En este tema nos centraremos en el papel que desempeñan las especificaciones de los métodos. Éstas constituyen el eje del trabajo en equipo. No es posible delegar responsabilidad para implementar un método si no existe una especificación. La especificación funciona como un contrato: el implementador es el responsable del cumplimiento del contrato, y un cliente que utilice el método podrá confiar en el contrato. De hecho, veremos que al igual que los contratos reales legales, las especificaciones requieren exigencias por ambas partes: cuando la especificación posee una precondición, el cliente tiene también que afrontar responsabilidades.

Muchos de los peores errores de los programas surgen a causa de malentendidos en el comportamiento de las interfaces. Aunque cada programador tiene en mente las especificaciones, no todos ellos las escriben. Como resultado, cada programador de un equipo posee en mente una especificación distinta. Cuando el programa falla, resulta difícil determinar dónde está el error. Las especificaciones concretas en el código le permiten distribuir la responsabilidad (¡entre los fragmentos del código, no entre el personal!), así como ahorrarle la molestia de tener que darle vueltas a la cabeza para hallar dónde ubicar las correcciones.
Otra de las ventajas de las especificaciones es que ahorran al cliente la tarea de tener que leer el código. Si no está convencido de que la lectura de una especificación es más sencilla que la lectura del código, fíjese en algunas de las especificaciones estándar de Java y compárelas con el código fuente que las implementa. Por ejemplo, Vector, en el paquete java.util, posee una especificación simple, pero su código no lo es en absoluto.

Las especificaciones también benefician al implementador de un método porque le proporcionan libertad para cambiar la implementación sin avisar a los clientes. Las especificaciones pueden aligerar el código. En algunas ocasiones, una especificación débil hace que sea posible conseguir una implementación mucho más eficaz. En concreto, una precondición puede excluir ciertos estados en los que se podría haber invocado a un método y que podrían haber provocado un chequeo costoso que ya no es necesario.
Este tema está relacionado con lo que debatimos en las dos lecciones anteriores sobre el desacoplamiento y las dependencias. En éstas, nos ocupábamos únicamente de si existía una dependencia. Aquí, trataremos de investigar la forma que la dependencia debería adoptar. Al presentar sólo la especificación de un procedimiento, sus clientes se hacen menos dependientes de él y, por tanto, es menos probable que necesiten modificarse cuando el procedimiento cambie.

Especificacion formal

Introduccion
La calidad del software es una de las problematicas mas importantes en los procesos de desarrollo de software. Garantizar el correcto funcionamiento bajo situaciones no determinadas es una tarea que tiene que ser realizada con cuidado extremo. En algunos casos, este tipo de pruebas son de mayor importancia, ya que involucran ambientes sensibles e informacion critica en donde es necesario garantizar que cada uno de los componentes involucrados (hardware, software y componentes humanos) actue de manera correcta ante situaciones especificas, con una variedad de ejemplos que cubren areas tan diversas como planeacion de trafico, aplicaciones militares y sistemas medicos, entre muchas otras.
Los modelos formales presentan una alternativa practica para solucionar estos problemas. Constituyen un enfoque analitico para la especificacion, diseño y verificacion de sistemas de hardware y software. Su caracteristica principal es la rigurosidad en la que sus modelos se encuentran basados, con fundamentos en solidos principios matematicos que permiten definir con precision y sin temor a ambiguedades las necesidades de un sistema. Gracias a estos fundamentos, el software generado mediante metodos formales puede ser verificado mediante el cumplimiento de propiedades derivadas de la especificacion. Este enfoque ha resultado ser exitoso frente a otras tendencias, encontrando errores en diseño que dificilmente habrian podido ser considerados usando otras tecnicas.
Definiciones: Metodos Formales
Una de las metas de la Ingenieria del Software es lograr que los desarrolladores construyan sistemas confiables independientemente de su complejidad. Una forma de alcanzar esta meta es a través del uso de Métodos Formales (MF): técnicas, lenguajes y herramientas definidos matemáticamente, para especificar y verificar tales sistemas. El uso de MF propicia la confiabilidad y la seguridad de un sistema, al aumentar la comprensión acerca de un sistema revelando inconsistencias, ambigüedades e incompletitudes, que de otra manera pasan desapercibidas. [L. Mendoza, M. Pérez y M. Capel]
Los métodos formales que se utilizan para desarrollar sistemas de computadoras son técnicas de base matemática para describir las propiedades del sistema. Estos métodos formales proporcionan marcos de referencia en el seno de los cuales las personas pueden especificar, desarrollar y verificar los sistemas de manera sistemática, en lugar de hacerlo ad hoc. [John J. Marciniak]
Los metodos formales representan un conjunto de tendencias de desarrollo de software y hardware en donde la especificacion, verificacion y diseño de componentes se realiza mediante notaciones, lenguajes, herramientas y tecnicas basadas en teorias con solida fundamentacion matematica. El uso de notaciones y lenguajes formales permite plantear de manera clara los requerimientos de un sistema, generando especificaciones que definen el comportamiento en terminos del “que debe hacer” y no del “como lo hace”. [Hugo A. Lopez A.]
Los metodos formales permiten al ingeniero del software crear una especificación sin ambigüedades que sea más completa y constante que las que se utilizan en los métodos convencionales u orientados a objetos. La teoría de conjuntos y las notaciones lógicas se utilizan para crear una sentencia clara de hechos (o de requisitos). Esta especificación matemática entonces se puede analizar para comprobar que sea correcta y constante. Como esta especificación se crea utilizando notaciones matemáticas inherentemente es menos ambigua que los nodos informales de presentación. [Roger Pressman]
En Ingenieria del Software un método formal es un camino a la construcción y análisis de modelos matemáticos que permitan una automatización del desarrollo de sistemas informáticos. Los métodos formales se caracterizan por emplear técnicas y herramientas matemáticas para lograr una facilitación a la hora de encarar la construcción o el análisis de un modelo matemático de un sistema. [Wikipedia]
Los diez mandamientos de los metodos formales
La decisión de hacer uso de los métodos formales en el mundo real no debe de adoptarse a la ligera. Bowen y Hinchley  han acuñado los diez mandamientos de los métodos formales, como guía para aquellos que estén a punto de embarcarse en este importante enfoque de la Ingenieria del Software.
  1. Seleccionarás la notación adecuada. Con objeto de seleccionar eficientemente dentro de la amplia gama de lenguajes de especificación formal existente, el ingeniero del software deberá considerar el vocabulario del lenguaje, el tipo de aplicación que haya que especificar y el grado de utilización del lenguaje.
  2. Formalizarás, pero no de más. En general, resulta necesario aplicar los métodos formales a todos los aspectos de los sistemas de cierta envergadura. Aquellos componentes que sean críticos para la seguridad serán nuestras primeras opciones, e irán seguidos por aquellos componentes cuyo fallo no se pueda admitir (por razones de negocios).
  3. Estimarás los costes. Los métodos formales tienen unos costes de arranque considerables. El entrenamiento del personal, la adquisición de herramientas de apoyo y la utilización de asesores bajo contrato dan lugar a unos costes elevados en la primera ocasión. Estos costes deben tenerse en cuenta cuando se esté considerando el beneficio obtenido frente a esa inversión asociada a los métodos formales.
  4. Poseerás un experto en métodos formales a tu disposición. El entrenamiento de expertos y la asesoría continua son esenciales para el éxito cuando se utilizan los métodos formales por primera vez.
  5. No abandonarás tus métodos formales de desarrollo. Es posible, y en muchos casos resulta deseable, integrar los métodos formales con los métodos convencionales y/o con métodos orientados a objetos. Cada uno de estos métodos posee sus ventajas y sus inconvenientes. Una combinación de ambos, aplicada de forma adecuada, puede producir excelentes resultados.
  6. Documentarás suficientemente. Los métodos formales proporcionan un método conciso, sin ambigüedades y consistente para documentar los requisitos del sistema. Sin embargo, se recomienda que se adjunte un comentario en lenguaje natural a la especificación formal, para que sirva como mecanismo para reforzar la comprensión del sistema por parte de los lectores.
  7. No comprometerás los estándares de calidad. Los métodos formales no tienen nada de mágico, y por esta razón, las demás actividades de SQA deben de seguir aplicándose cuando se desarrollen sistemas.
  8. No serás dogmático. El ingeniero de software debe reconocer que los métodos formales no son una garantía de corrección. Es posible (o como algunos probablemente dirían) que el sistema final, aun cuando se haya desarrollado empleando métodos formales, siga conteniendo pequeñas omisiones, errores de menor importancia y otros atributos que no satisfagan nuestras expectativas.
  9. Comprobarás, comprobarás y volverás a comprobar. Los métodos formales no absuelven al ingeniero del software de la necesidad de llevar a cabo unas comprobaciones exhaustivas y bien planeadas.
  10. Reutilizarás cuanto puedas. A la larga, la única forma racional de reducir los costes del software y de incrementar la calidad del software pasa por la reutilización. Los métodos formales no modifican esta realidad. De hecho, quizás suceda que los métodos formales sean un enfoque adecuado cuando es preciso crear componentes para bibliotecas reutilizables.
Los siete mitos sobre los metodos formales
Los siete mitos mas generalizados sobre los metodos formales son variaciones de los siguientes:
  1. Los metodos formales garantizan que el software esta perfecto. El mito mas importante es que los metodos formales serian todopoderosos, si nosotros humildes mortales pudiesemos aplicarlos. Este mito es pernicioso porque nos lleva a expectativas irreales y a la idea de que los metodos formales son de alguna forma todo o nada.
  2. Los metodos formales se centran en demostrar correccion. En los Estados Unidos, gran parte del trabajo desarrollado en metodos formales se ha concentrado en la verificacion de programas. Esto ha hecho que los metodos formales parezcan muy dificiles y no muy relevantes para la vida real.
  3. Los metodos formales son utiles solo para sistemas criticos. Esta creencia se basa en la percepcion de la dificultad que implica la aplicacion de metodos formales. La verdad es que los sistemas criticos requieren un uso mas acucioso de metodos formales, pero cualquier sistema puede beneficiarse con el uso de algunas tecnicas de especificacion formal.
  4. Los metodos formales requieren matematicos entrenados. Los metodos formales se basan en notaciones matematicas, y muchas personas creen que esto los hace dificiles para la practica de los ingenieros de software. Este mito, a su vez, se basa en la percepcion de que las matematicas son intrinsicamente dificiles.
  5. Los metodos formales aumentan el costo del desarrollo. Se acostumbraba decir que a pesar que el costo que significaba usar metodos formales era muy alto, de todas formas era conveniente porque resultaba en menores costos de mantenimiento del software.
  6. Los metodos formales son incomprensibles para los usuarios. Una especificacion formal esta llena de simbolos matematicos que resultan incomprensibles para cualquiera que no este familiarizado con la notacion. De ahi que se suponga que son inutiles para clientes no matematicos.
  7. Los metodos formales no se usan en grandes proyectos reales. Los metodos formales se asocian comunmente con departamentos academicos y organizaciones de investigacion. Se piensa que solo estas organizaciones tienen la capacidad necesaria para usar metodos formales y que estos solo son apropiados para las aplicaciones idealizadas que estos grupos desarrollan.
Principales Metodos Formales utilizados en el desarrollo de software
  • Metodos formales basados en Lógica de Primer Orden: Z, B, VDM, Object-Z, Z++ y VDM++.
  • Metodos formales basados en Formalismos Algebraicos: HOSA (Hidden Order Sorted Algebras), TROLL, OBLOG, Maude y AS-IS (Algebraic Specifications with Implicit States).
  • Metodos formales basados en Redes de Petri: CO-OPN (Concurrent Object-Oriented Petri Nets)
  • Metodos formales basados en Lógica Temporal: TRIO, OO-LTL y ATOM.
  • Metodos Semiformales: Syntropy, Statemate, UML y OCL (Object Constraint Language)

Especificacion basada en modelos

ESPECIFICACIONES BASADAS EN MODELOS:  

Consisten en especificar un sistema en términos de su estado y las transformaciones de ese estado:
  • El estado del sistema se define por un conjunto de variables
  • Las transformaciones del estado se definen mediante un conjunto de operaciones.
  • El estado del sistema es modelado usando entidades matemáticas
    • Ej., conjuntos, funciones, relaciones, secuencias, etc.
 Lenguajes de especificación basados en modelos:
  • VDM (Vienna Development Method)
  • Notación Z

LA NOTACION Z:
  • Está basada en la teoría de conjuntos y la lógica de predicado ó1er. orden.
  • Desarrollada por el Grupo de Programación de la Universidad de Oxford, Inglaterra.
  • Una especificación elaborada en Z consiste de una colección de esquemas.
  • Un esquema en Z es un constructo usado para representar las propiedades estáticas o dinámicas de los tipos de objetos del dominio de aplicación del sistema.
 Se emplean dos tipos de esquemas para cada tipo de objeto modelado:
  • Un esquema estático que modela las propiedades estáticas del tipo de objetos, incluyendo sus estados y las relaciones invariantes que se preservan ante los cambios de estado.

  • Uno o más esquemas dinámicos, cada uno de los cuales modela una operaciones del tipo de objeto.
Validación de requerimientos
  • "...es el proceso de determinar que la especificación es consistente con la definición de los requerimientos; esto es, la validación asegura que los requerimientos satisfacerán las necesidades del cliente". [PFL98].
  • Involucra, al menos, tres pasos:
    • Asegurar que cada especificación del DER está asociado a un requerimiento del DDR.
    • Verificar el DDR para asegurarse que cada requerimiento está vinculado con las especificaciones del DER.
    • Asegurarse, a través de una revisión de requerimientos, que tanto la definición (DDR) como la especificación (DER) cumple los criterios de calidad de requerimientos indicados anteriormente 
        
      Técnicas de validación de requerimientos:
    • Técnicas manuales:
      1. Lectura del DDR y DER
      2. Verificación de las referencias cruzadas entre ambos documentos
      3. Entrevistas
      4. Revisión de requerimientos
      5. Listas de chequeo o verificación
      6. Modelos manuales para verificar funciones y relaciones
      7. Escenarios
      8. Pruebas matemáticas
         
    Técnicas automatizadas:
  •   Verificación automática de referencias cruzadas 
  • Prototipos
Aspectos de la Revisión de Requerimientos:
  • Revisar las metas y objetivos establecidos para el sistema en desarrollo
  • Comparar los requerimientos definidos con las metas y objetivos establecidos.
  • Describir el ambiente en el cual operará el sistema,
  • Revisar las interfaces del sistema con otros sistemas, sus flujos de información, su estructura funcional y sus restricciones.
  • Establecer los riesgos involucrados en el desarrollo del sistema.
  • Definir los medios y las técnicas para verificar los requerimientos
Modelos del proceso de software 
  •  Cascada: Separa y distingue las diferentes fases de especificación y desarrollo 
  •  Evolutivo: La especificación y el desarrollo son alternados. 
  • Transformaciones Formales: Un modelo matemático del sistema se trasforma formalmente en una implementación 
  •  Basados en Reusabilidad: El sistema se ensamble a partir de componentes existentes 

    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.