Application invariants: Design by Contract augmented with deployment correctness logic

El Diseño por Contracto es un método para el desarrollo de software orientado-a-objeto robusto. El DbC (por sus siglas en inglés Design by Contract), involucra precondiciones (son los requerimientos que el cliente debe satisfacer a su proveedor, dicho de otra manera, es lo que el proveedor espera del cliente), poscondiciones (es lo que el cliente espera del proveedor) e invariantes de clase que son condiciones que corresponden a axiomas que deben ser cumplidos por cada instancia válida de la clase.

En este contexto, Savidis [1] propone invariantes de alcance a toda la aplicación. En este artículo, el autor propone tres roles distintos para las invariantes de aplicación: locales (están asociadas a una instancia en particular de la clase proveedor), grupales (asociadas únicamente a un conjunto de instancias de la clase proveedor) e invariantes de aplicación de tipo global (asociadas a todas las instancias de la clase Proveedor).

El autor propone una implementación en C++ para este tipo de invariantes de aplicación y concluye que éstas (invariantes de aplicación) revelan la cooperación bilateral fundamental entre las clases cliente y las clases proveedoras, para convergir en la correctitud orientada a la aplicación y correctitud de la instancia proveedora. Invariantes de aplicación guardan la correctitud lógica, la cual, aunque definida por las clases cliente, conciernen principalmente a las instancias proveedoras.

Savidis, menciona además que, sin invariantes de aplicación, la verificación manual de la correctitud lógica dentro de las clases cliente es un patrón de software que introduce un gran número de llamadas a aserciones replicadas fusionadas con código cliente, lo que implica incrementar la complejidad del código fuente para lograr la granularidad dinámica de la correctitud de las pruebas de unidad. En este contexto, invariantes de aplicación claman hacer esto, ofreciendo un placeholder bien definido para, dinámicamente, guardar tal correctitud lógica dentro de la instancia proveedora, de una manera modular y reusable, con el mínimo de injections dentro del código fuente del cliente.

Referencias

[1] A. Savidis. Application invariants: Design by Contract augmented with deployment correctness logic. Softw. Pract. Exper. 2006; 36:255–282. Published online 15 September 2005 in Wiley InterScience (www.interscience.wiley.com). DOI: 10.1002/spe.695
http://www.ics.forth.gr/hci/files/plang/app_invariants.pdf

Verificación modular de código con SAT

Dennis et al. [1] someten a verificación 6 distintas implementaciones en Java de la estructura de datos Lista Enlazada. Para ello, los autores aplican un análisis modular, en el cual cada método de la clase es analizado de manera independiente al resto de métodos de la misma clase. El análisis involucra una reducción automática de dos fases: primero, a una forma intermedia en lógica relacional, y posteriormente, una conversión a formula booleana (empleando técnicas existentes), la cual es entonces manipulada por un solucionador SAT.

Los resultados presentados en este trabajo demuestran violaciones dentro de las implementaciones de varias librerías de acuerdo a la especificación abstracta de LinkedList y revelan también errores en la especificación de JML (Java Modeling Language).

Como trabajo futuro los autores proponen evaluar el análisis modular vs. análisis completo de un sistema. Finalmente concluyen con la aseveración que la técnica que presentan parece ser viable, aunque todavía queda mucho trabajo por hacer. Consideran que el obstáculo mayor para extender el análisis a todos los métodos de la interfase List es el manejo de colecciones genéricas en métodos tales como addAll.

Referencias

[1] G. Dennis, F. ShengHo Chang and D. Jackson. Modular verification of Code with SAT. ISSTA’06, July 17–20, 2006.
http://sdg.csail.mit.edu/pubs/2006/dennis_modular.pdf

Estado del arte

Para el desarrollo de una tesis la investigación del estado del arte (trabajos relacionados, antecedentes, o como se le quiera llamar) es una actividad de suma importancia cuyo objetivo es demostrar la relevancia de nuestra investigación propuesta y/o demostrar que nuestra propuesta es única.

Para dicha tarea, en mi tesis de maestría me encargaré de estudiar lo referente a la verificación y validación de sistemas orientados a objetos aplicando métodos formales, por lo que mediante este espacio, presentaré sinopsis de los artículos, tesis y demás trabajos de investigación que den soporte al estado del arte de mi tesis en desarrollo. De esta manera, en mi siguiente post les dejaré la sinopsis del artículo titulado "Modular verification of Code with SAT" de Dennis et al. [1].

Referencias

[1] G. Dennis, F. ShengHo Chang and D. Jackson. Modular verification of Code with SAT. ISSTA’06, July 17–20, 2006.
http://sdg.csail.mit.edu/pubs/2006/dennis_modular.pdf