XJML (Ramírez et al., 2012) es una plataforma modular externa para la verificación y validación de clases Java empleando el lenguaje de modelado de Java (JML, Java Modeling Language) a través de contratos escritos en XML. Uno de los problemas que se enfrentaron durante el desarrollo de XJML fue la integración de la técnica de verificación denominada Full Static Program Verification (FSPV). En este artículo se presentan los experimentos y resultados que permitieron definir qué herramienta se integra en XJML para ejecutar FSPV.
XJML (Ramírez et al., 2012) is a modular external platform for Verification and Validation of Java classes using the Java Modeling Language (JML) through contracts written in XML. One problem faced in the XJML development was how to integrate Full Static Program Verification (FSPV). This paper presents the experiments and results that allowed us to define what tool to embed in XJML to execute FSPV.
JML fue creado por Gary T. Leavens y es el Behavioral Interface Specification Language (BISL) más popular para Java (Chalin et al., 2008; Chalin et al., 2007), soportando Runtime Assertion Checking (RAC), Extended Static Checking (ESC) y Full Static Program Verification (FSPV), de hecho, es el único BISL soportado por estas tres tecnologías de verificación (Chalin et al., 2008; Chalin et al., 2007).
Desde la concepción de JML se han efectuado múltiples avances en el desarrollo de herramientas para su soporte. Esto nos conduce a una gran cantidad de herramientas, duplicación de trabajo (esfuerzos) y una alta y colectiva sobrecarga para el mantenimiento de JML y sus herramientas de soporte. Sin embargo, la evolución de Java como lenguaje de programación, y las mejoras aplicadas a las herramientas y aplicaciones de JML, obliga a la comunidad de JML a mantenerse al día, que es una tarea difícil en donde se producen muchas variantes y alternativas de dichas herramientas y aplicaciones.
Estas razones y el hecho de que aún no existe una herramienta que brinde soporte total a RAC, ESC y FSPV tal como se presenta en Ramírez et al. (2012) fue lo que impulsó el diseño y desarrollo de XJML. XJML es, hasta donde sabemos, la primera propuesta para embeber un contrato para una clase Java usando JML y XML. XJML 1.0 logra integrar:
- a)
RAC empleando como base JML4 (Chalin et al., 2008), sobre todo los componentes jml4c y jml4rt
- b)
ESC a través de ESC/Java2 (Flanagan et al., 2002), versión 2.0.5
Si bien la integración de estas herramientas soportadas a través de XML representó un reto interesante, fue aún mayor el problema que se encontró al integrar FSPV en XJML 1.0. Dicho esto, el objetivo de este trabajo es presentar los experimentos y resultados que permitieron determinar la herramienta que da soporte a FSPV en XJML 1.0, FSPVRunner como se denomina a dicho componente en XJML 1.0 (Ramírez et al., 2012).
Marco referencialComo se ha indicado en la sección anterior, JML es un lenguaje para la verificación de clases Java que soporta las técnicas de Verificación de Aserciones en Tiempo de Ejecución (RAC, Runtime Assertion Checking), Verificación Estática Extendida (ESC, Extended Static Checking) y la Verificación de Programas Completamente Estática (FSPV, Full Static Program Verification). Pero, ¿qué son estas técnicas de verificación, cuál es su función u objetivo primordial?
RAC consiste en la verificación en tiempo de ejecución de las aserciones expresadas en algún lenguaje de especificación (para el caso de este trabajo, en JML). Las aserciones son una de las técnicas automatizadas más usadas para la detección de fallos en sistemas computacionales a la vez que proveen información sobre su localización, inclusive para fallas (faults) que se producen durante la ejecución, pero no conducen a errores significativos (failures).
Las aserciones tienen una larga y distinguida historia en los anales de la ingeniería de software y el diseño de lenguajes de programación. Inicialmente se desarrollaron como un medio para expresar las propiedades deseadas de un programa como un paso necesario en la construcción de pruebas formales y deductivas para la corrección de programas.
Las aserciones han tenido muchas otras aplicaciones en la ingeniería de software a través de los años (Clarke y Rosenblum, 2006), aunque primordialmente en las etapas posteriores de desarrollo, en particular en el desarrollo y ejecución del código fuente. Son un elemento importante de la verificación de modelos (model checking), una técnica alternativa y activamente estudiada de la verificación de programas (program verification), en el cual el espacio de estados resultante de la ejecución de un programa se verifica contra aserciones lógicas que expresan propiedades de seguridad temporal (temporal safety) y de tiempo de vida o vitalidad de un programa (liveness) (Clarke y Rosenblum, 2006).
ESC es la verificación estática de las aserciones expresadas en JML. Es una técnica experimental de verificación de programas en tiempo de compilación (Flanagan et al., 2002). Una de las herramientas más conocidas para esta verificación en Java es ESC/Java, la cual emplea un generador de condiciones de verificación (verification-condition generation) y técnicas de demostración automática de teoremas (Flanagan et al., 2002). Provee a los programadores, a través de un lenguaje simple de anotaciones, decisiones de diseño que pueden expresarse formalmente.
ESC/Java examina el programa anotado y notifica inconsistencias entre las decisiones de diseño expresadas en las anotaciones y el código actual (implementación) y también advierte sobre errores potenciales en tiempo de ejecución del código.
FSPV es una técnica de verificación que emplea demostradores de teoremas (theorem provers) (Karabotsos et al., 2008). Esta técnica de verificación de programas puede emplear demostradores automáticos de teoremas, como por ejemplo1: Alt-ergo, Simplify, Z3, Yices, CVC3, CVCL, Gappa, Eprover, haRVey, Zenon, SPASS, Vampire y veriT, o bien, emplear asistentes o demostradores interactivos (requieren la intervención humana) de teoremas, tales como1 Coq, PVS, Isabelle/HOL, HOL 4, HOL Light y Mizar.
La demostración automática de teoremas (ATP, automated theorem proving) que también puede llamarse deducción automatizada, es actualmente el sub-campo más desarrollado del razonamiento automático, y se encarga de la demostración de teoremas matemáticos mediante programas de ordenador.
Así, un demostrador automático de teoremas (automatic theorem prover) es un programa de cómputo desarrollado para la deducción automática de teoremas, ampliamente estudiado y utilizado en la verificación y validación de sistemas de cómputo.
Por otro lado, un asistente de pruebas (proof assistant) o demostrador interactivo de teoremas (interactive theorem prover) es una herramienta de software para asistir en el desarrollo de demostraciones formales mediante la colaboración hombre-máquina. Esto involucra algún tipo de editor interactivo de demostraciones, o alguna otra interfaz, con la cual un humano puede guiar la búsqueda de demostraciones.
Se preguntará: ¿qué tiene que ver todo esto con XJML o incluso con este trabajo?, ¿qué es Krakatoa, qué relación y cuál es su importancia en este trabajo?
XJML 1.0 adopta la plataforma Why para efectuar FSPV, ya que esto es posible gracias al complemento (plug-in) Krakatoa que forma parte de la plataforma Why. Krakatoa es una herramienta de FSPV para clases Java anotadas con JML (Karabotsos et al., 2008) y es similar a FSPV Theory Generator (FSPV TG) (James y Chalin, 2009, Chalin et al., 2008), (Karabotsos et al., 2008), en el sentido que traduce programas Java a un programa intermedio. Sin embargo, los programas en Why se traducen en una teoría específica usando el compilador Why escrito en Objective CAML.
XJML 1.0 soporta Why 2.30 y Why3. Why 2.30 es una plataforma para la verificación de software que contiene varias herramientas2:
- •
Why, un Generador de Verificación de Condición (VCG, Verification Condition Generator) de propósito general, el cual se utiliza como herramienta de fondo (back-end) por otras herramientas de verificación (Krakatoa y Caduceus) pero también puede usarse de manera directa para la verificación programas.
- •
Krakatoa3, una herramienta para la verificación de programas Java.
- •
• Caduceus4, herramientas para la verificación de programas hechos en el lenguaje C; sin embargo Caduceus es ahora obsoleto y en su lugar, los usuarios deben cambiar a Frama-C5.
Por otra parte, Why36 es la siguiente generación de la plataforma Why para la verificación de software. Separa claramente la parte puramente lógica de la especificación y la generación de verificación de condiciones de los programas.
Why3 se desarrolla en el proyecto de equipo ProVal7, el cual está conformado por INRIA Saclay-Île-de-France, en conjunto con el Laboratorio de Investigación en Informática de París (Laboratoire De Recherche En Informatique) y la Universidad del Sur de París (University of Paris Sud).
En este trabajo se presenta un conjunto de experimentos que ayudaron a determinar la herramienta que da soporte a FSPV en XJML 1.0, FSPVRunner como se denomina a dicho componente en XJML 1.0 (Ramírez et al., 2012) y que pueden considerarse como una extensión dentro del proyecto XJML.
Para concluir con esta sección resta describir, de manera breve, qué es FSPVRunner. FSPVRunner es un componente del subsistema Runners de XJML, que se encarga de ejecutar FSPV a través de la herramienta Krakatoa de la plataforma Why. La plataforma XJML es descrita con mayor detalle en Ramírez et al. (2012).
El nombre FSPVRunner se conforma por el prefijo FSPV, el cual corresponde a dicha técnica de verificación, y el sufijo Runner se debe a que FSPVRunner es un componente que forma parte del subsistema lanzadores (Runners) de XJML 1.0. Dicho esto, FSPVRunner se encarga de ejecutar FSPV y su arquitectura y funcionamiento es descrito con mayor detalle en Ramírez et al. (2012).
MétodoTodos los experimentos se llevaron a cabo en un equipo de cómputo con las siguientes características en hardware y software:
- •
Notebook Dell Vostro 1520
- •
Procesador Intel(R) Core(TM) 2 Duo CPU T6670 a 2.20Ghz
- •
- •
Sistema Operativo GNU/Linux Ubuntu 10.04 (lucid) de 32 bits, núcleo Linux 2.6.32-34- generic con GNOME 2.30.2
- •
Java Development Kit 6.0 update 29
- •
Eclipse SDK versión 3.7.0, build id I20110613-1736
Se otorgaron 30 segundos para la ejecución de cada experimento y el proceso para determinar la herramienta que da soporte a FSPV en XJML 1.0 consistió, primero en probar los módulos FSPV para JML4, JMLEclipse y OpenJML, los cuales son los últimos esfuerzos de la comunidad de JML para desarrollar un entorno integrado de verificación (integrated verification environment) (Chalin et al., 2010). Respecto a JML4 FSPV TG Theory Generator (James y Chalin, 2009; Chalin et al., 2008; Karabotsos et al., 2008), se descartó debido a su inestabilidad observada en las pruebas al momento de instalar y configurar los módulos requeridos8.
Las conclusiones sobre la inestabilidad y etapa de desarrollo de JML4 y JMLEclipse están fundamentadas en las páginas Web principales de los respectivos proyectos9. Puede observarse cómo en dichas páginas se menciona que el lanzamiento de una primera versión oficial (no beta) está pendiente por determinarse.
Otra herramienta con la que se efectuaron pruebas fue OpenJML. OpenJML es la siguiente generación del núcleo de JML y será soportado por Java 1.7. Está basada en OpenJDK, por lo que desafortunadamente la instalación fallará (Cok, 2011) si la VM de Java no es una versión compatible con Java 1.7. Además, aún hay mucho trabajo por hacer respecto a OpenJML y sus características como un plug-in de Eclipse aún no están definidas (Cok, 2011). En resumen, OpenJML tampoco está listo para utilizarse de manera estable.
Como ya se mencionó, integrar RAC y ESC en XJML 1.0 no presentó mayor dificultad en comparación con FSPV, tal como hemos presentado. Ahora bien, si JML4, JMLEclipse y OpenJML no pudieron proveer un módulo de FSPV estable, fue necesario buscar alguna herramienta o plataforma que pudiera soportar tal técnica de verificación en XJML 1.0. En la tabla 1 se presenta una comparación de herramientas para FSPV, lo que aunado con los argumentos presentados, permitieron determinar la plataforma Why (Christophe y Marché, 2007) como herramienta de soporte de FSPV para XJML 1.0.
Comparación de herramientas FSPV para Java (Karabotsos et al., 2008)
Para su mejor comprensión se describe a continuación cada leyenda de las filas de la tabla 1.
- •
Maintained: indica si a la herramienta aún se le da soporte o se mantiene en desarrollo.
- •
Open source: indica si la herramienta es de código abierto.
- •
Proven sound: indica si se ha demostrado que la herramienta es consistente10.
- •
Proven complete: indica si se ha demostrado que la herramienta es completa (nos referimos a la completitud en el campo de lógica computacional).
- •
Above two proofs done: indica en qué herramienta, técnica o método fue demostrada la consistencia y completitud de la herramienta.
- •
VC generation done in prover: indica si la herramienta es capaz de generar sus propias condiciones de verificación (VC es acrónimo de verification-condition).
- •
Termination of recursive functions: indica si la herramienta tiene la capacidad de tratar con funciones recursivas.
Con la determinación de la plataforma Why para dar soporte a FSPV en XJML 1.0, fue necesario delimitar qué versión de la plataforma Why soportaría XJML 1.0, así como cuáles demostradores automáticos de teoremas (Automatic Theorem Provers) se utilizarían para verificar el comportamiento de FSPV en XJML 1.0.
Se efectuaron pruebas con Why 2.30 (Christophe, 2003) y Why3 0.71 (Bobot et al., 2011) que son las versiones disponibles hasta el momento de la redacción de este trabajo. Para cada versión de la plataforma Why se realizaron experimentos con sus respectivos demostradores automáticos de teoremas soportados, de acuerdo con la documentación disponible para cada versión de Why (Christophe, 2011).
Los experimentos consistieron en verificar la clase Isqrt.java (figura 1), la cual es una implementación que calcula la raíz cuadrada de un número entero.
La implementación de la clase Isqrt es breve, pero a la vez creemos que fue lo suficientemente completa para emitir la conclusión que permitió seleccionar las herramientas que dieron soporte a FSPV en XJML 1.0. Así, la clase Isqrt contiene al menos una precondición (línea 10 de la figura 1), postcondición (línea 11, figura 1), invariante de clase (líneas 2 a 8 en la figura 1) y de ciclo (líneas 16 a 18, figura 1), las cuales son los tipos de aserciones más comunes en la verificación y validación de sistemas computacionales.
Será necesario presentar los distintos demostradores automáticos de teoremas y demostradores interactivos de teoremas (proof assistant o interactive theorem prover) que se usaron para realizar los experimentos con la clase Isqrt, mismos experimentos que permitieron seleccionar qué versión de la plataforma Why, demostradores automáticos de teoremas y demostradores interactivos de teoremas emplear para efectuar los experimentos con el módulo FSPV de XJML 1.0. Se efectuaron experimentos con Why 2.30 y Why3 0.71 con los demostradores automáticos de teoremas:
- •
Alt-ergo 0.93
- •
Simplify 1.5.4
- •
Z3 2.2 y 3.2
- •
Yices 1.0.17 y 1.0.31
- •
CVC3 versión development y 2.4.1
- •
CVCL versión development y 2.4.1
- •
Gappa 0.12.0 y 0.15.1
- •
Eprover 1.4 Namring
- •
haRVey 0.5.10
- •
Zenon 0.6.3
- •
SPASS 3.7
- •
Vampire 0.6
- •
veriT 201107
Se efectuaron experimentos con Why 2.30 y Why3 0.71 empleando los siguientes demostradores interactivos de teoremas
- •
Coq 7.4 y 8.3pl2
- •
PVS 5.0
- •
Isabelle/HOL 2011-1
- •
HOL 4 (Kananaskis 7)
- •
HOL Light 100110
- •
Mizar 7.12.01
Al igual que con los demostradores automáticos de teoremas listados, la lista de los demostradores interactivos de teoremas se obtuvo de la documentación y páginas Web de Why 2.30 y Why3 0.71, por lo que es posible que existan más de estos, con los cuales no fue posible efectuar experimentos debido a que no se encuentran en la lista de los soportados por Why.
Resultados y discusiónLas tablas 2 y 3 muestran la URL de descarga de los demostradores automáticos de teoremas y demostradores interactivos de teoremas empleados en los experimentos.
URL de descarga de los demostradores automáticos de teoremas empleados en los experimentos
URL de descarga de los demostradores interactivos de teoremas empleados en los experimentos
| Demostrador interactivo de teoremas | Versión | URL de descarga |
| Coq | 7.4 | ftp://ftp.inria.fr/INRIA/Projects/LogiCal/coq/V7.4/coq-7.4-Linux-i386.tar.gz |
| 8.3pl2 | http://coq.inria.fr/distrib/V8.3pl2/files/coq-8.3pl2.tar.gz | |
| PVS | 5.0 | http://pvs.csl.sri.com/cgi-bin/downloadlic.cgi?file=pvs-5.0-ix86-Linux-allegro.tgz |
| Isabelle/HOL | 2011-1 | http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/Isabelle2011-1_bundle_x86-linux.tar.gz |
| HOL 4 | HOL 4 | http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7.tar.gz/download (Kananaskis 7) |
| HOL Light | 100110 | http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_100110.tgz |
| Mizar | 7.12.01 | ftp://mizar.uwb.edu.pl/pub/system/i386-linux/mizar-7.12.01_4.166.1132-i386-linux.tar |
Ahora bien, las tablas 4 y 5 muestran, respectivamente, los distintos demostradores automáticos de teoremas y demostradores interactivos de teoremas utilizados para efectuar experimentos iniciales con el fin de observar el comportamiento de Why 2.30 y Why3 0.71 con cada uno de ellos y posteriormente experimentar con la clase Isqrt.
Versiones de la plataforma Why y sus respectivas salidas al detectar distintos demostradores automáticos de teoremas
| Plataforma Why | Demostrador automático de teoremas | Versión | Versión Recomendada | Compilado | Binario | Información mostrada |
| Why 2.30 | Alt-ergo | 0.931 | 0.8 | Sí | No | None |
| Why3 0.71 | Ok | |||||
| Why 2.30 | Simplify | 1.5.42 | 1.5.4 | No | Sí | None |
| Why3 0.71 | Ok | |||||
| Why 2.30 | Z3 | 2.23 | 1.34 | No | Sí | (obsolete) |
| Why3 0.71 | is quite old… | |||||
| Why 2.30 | 3.25 | No | Sí | (not supported) | ||
| Why3 0.71 | is not known to be supported… | |||||
| Why 2.30 | Yices | 1.0.17 | 1.0.17 | No | Sí | (obsolete) |
| Why3 0.71 | ||||||
| Why 2.30 | 1.0.316 | 1.0.17 | No | Sí | (not supported) | |
| Why3 0.71 | is not known to be supported… | |||||
| Why 2.30 | CVC3 | devel7 | 1.5 | No | Sí | (not supported) |
| Why3 0.71 | is not known to be supported, use it at your own risk! | |||||
| Why 2.30 | 2.4.18 | Sí | No | (not supported) | ||
| Why3 0.71 | is not known to be supported… | |||||
| Why 2.30 | CVCL | devel1 | 1.5 | No | Sí | (not supported) |
| Why3 0.71 | ||||||
| Why 2.30 | 2.4.12 | Sí | No | (not supported) | ||
| Why3 0.71 | is not known to be supported… | |||||
| Why 2.30 | Gappa | 0.12.0 | 0.12.0 | Sí3 | No | (obsolete) is quite old, please consider |
| Why3 0.71 | upgrading to a newer version | |||||
| Why 2.30 | 0.15.14 | none | ||||
| Why3 0.71 | ok | |||||
| Why 2.30 | Eprover | 1.4 Namring | No se especifica | Sí | No | none5 |
| Why3 0.71 | ok | |||||
| Why 2.30/ | haRVey6 | 0.5.10 | No se especifica | No | No | none |
| Why3 0.71 | ||||||
| Why 2.30/ | Zenon7 | 0.6.3 | No se especifica | Sí | No | none |
| Why3 0.71 | ||||||
| Why 2.30 | SPASS | 3.7 | No se especifica | Sí | No | none8 |
| Why3 0.71 | ok | |||||
| Why 2.30 | Vampire | 0.6 | No se especifica | No | Sí9 | none |
| Why3 0.71 | ok | |||||
| Why 2.30 | veriT10 | 201107 | No se especifica | Sí | No | undetected |
| Why3 0.71 | is not known to be supported… |
A la fecha del 20 de noviembre de 2011 no encontramos en el sitio versión previa para realizar pruebas.
A la fecha del 20 de noviembre de 2011 no encontramos la versión 1.3 en el sitio http://research.microsoft.com/en-us/um/redmond/projects/z3/older_z3.html. Existen paquetes MSI para las versiones 1.3.3, 1.3.5 y 1.3.6, más sin embargo no fueron probadas debido al sistema operativo.
No logramos compilar la versión development (1.5) debido a errores en el proceso, por ello, descargamos el binario pre-compilado en http://www.cs.nyu.edu/acsys/cvc3/download/1.5/linux32/cvc3-optimized.
Para compilar el código fuente se necesitan satisfacerse las siguientes dependencias: GNU/Flex, GNU/Bison, GNU/GMP. Más información en http://cs.nyu.edu/acsys/cvc3/doc/INSTALL.html.
No logramos compilar la versión development (1.5) debido a errores en el proceso, por ello, descargamos el binario pre-compilado en http://www.cs.nyu.edu/acsys/cvc3/download/1.5/linux32/cvc3-optimized.
Para compilar el código fuente se necesitan satisfacer las siguientes dependencias: GNU/Flex, GNU/Bison, GNU/GMP. Más información en http://cs.nyu.edu/acsys/cvc3/doc/INSTALL.html.
Para compilar el código fuente se necesitan satisfacer las siguientes dependencias: GNU/MPFR (instalado desde repositorio, con nombre libmpfr-dev, versión 2.4.2-3ubuntu1) y bibliotecas de Boost C++ (instalado desde repositorio, con nombre libboost1.40-dev, versión 1.40.0-4ubuntu4). Más información en http://lipforge.ens-lyon.fr/www/gappa/doc/index.html.
Proyecto aún en etapa de desarrollo tal como lo especifica su página principal http://harvey.loria.fr/.
Proyecto aún en etapa de desarrollo tal como lo especifica su página principal http://zenon-prover.org/.
No soportado por Why2.x, solo soportado por Why3 tal como se especifica en http://krakatoa.lri.fr/.
A través del sitio solo puede descargar archivos binarios para distintas plataformas debido al acuerdo de licencia especificado en http://www.vprover.org/license.cgi.
Es el sucesor de haRVey y se encuentra en arduo desarrollo como lo especifica su página principal http://www.verit-solver.org/.
Versiones de la plataforma Why y sus respectivas salidas al detectar distintos demostradores interactivos de teoremas
| Plataforma Why | Demostrador interactivo de teoremas | Versión | Versión recomendada | Compilado | Binario | Información mostrada |
| Why 2.30 | Coq | 7.41 | Al menos 7.4 | No | Sí | (obsolete) |
| Why3 0.71 | is not known to be supported, use it at your own risk! | |||||
| Why 2.30 | 8.3pl2 | Sí | No | (not supported) | ||
| Why3 0.71 | Ok | |||||
| Why 2.30 | PVS | 5.0 | No especifica | Sí | No | (not supported) |
| Why3 0.71 | Ok | |||||
| Why 2.30 | No | Sí | (not supported) | |||
| Why3 0.71 | None 20 | |||||
| Why 2.30/ | Isabelle/HOL | 2011-1* | No especifica | No | No | None |
| Why3 0.71 | ||||||
| Why 2.30/ | HOL 4 | HOL 4 (Kananaskis 7)* | No especifica | No | No | None |
| Why3 0.71 | ||||||
| Why2.30/ | HOL Light | 100110* | No especifica | No | No | None |
| Why3 0.71 | ||||||
| Why 2.30/ | Mizar | 7.12.01* | No especifica | Sí | No | None |
| Why3 0.71 |
Las columnas de las tablas 4 y 5 se describen a continuación:
- •
Plataforma Why. Versión de la plataforma Why en la que se utilizó el demostrador automático de teoremas o el demostrador interactivo de teoremas.
- •
Versión. Versión del demostrador automático de teoremas o demostrador interactivo de teoremas.
- •
Versión recomendada. De acuerdo con la documentación de la plataforma Why, se indica la versión que se recomienda para el demostrador automático de teoremas o demostrador interactivo de teoremas.
- •
Compilado. Indica si el demostrador automático de teoremas o demostrador interactivo de teoremas fue compilado en la misma máquina donde se realizaron los experimentos.
- •
Binario. Si el demostrador automático de teoremas o demostrador interactivo de teoremas no fue compilado en la misma máquina donde se realizaron los experimentos, entonces, se utilizó una versión precompilada del mismo. Se trata de una versión compilada en otro equipo, distinto al que fue utilizado para realizar los experimentos.
- •
Información mostrada. Se incluye la salida presentada por cada versión de la plataforma Why al detectar los demostradores automáticos de teoremas o demostradores interactivos de teoremas soportados.
De acuerdo con los resultados presentados en las tablas 4 y 5 se seleccionaron los demostradores automáticos de teoremas y demostradores interactivos de teoremas donde el valor de la columna Información mostrada sea Ok o None (sin ninguna nota informativa o de advertencia). La tabla 6 muestra la codificación utilizada para tabular los resultados de las tablas 7 y 8, las cuales presentan los demostradores interactivos de teoremas y demostradores automáticos de teoremas, respectivamente, que se emplearon para probar la clase Isqrt.java. Estos experimentos permitieron seleccionar con qué versión de la plataforma de Why, con cuáles demostradores automáticos de teoremas y cuáles demostradores interactivos de teoremas se realizaron los experimentos para verificar el módulo FSPVRunner de XJML 1.0.
Codificación para tabular los resultados de los experimentos con Why, demostradores automáticos de teoremas y demostradores interactivos de teoremas
| Codificación | Representa |
| * | A la fecha del 20 de Noviembre de 2011 es la última versión disponible y estable |
| N/S | No soportado |
| ? | Indeterminado, ya que entre múltiples ejecuciones los resultados no siempre fueron los mismos |
| CME | Consistente entre múltiples ejecuciones (3 ejecuciones) |
| NTV/NTT | Número de teorías válidas/Número de teorías totales |
| NTI/NTT | Número de teorías inválidas/número de teorías totales |
| NTETEV | Número de teorías que excedieron el tiempo establecido de validación |
| NTNVOR | Número de teorías que no pudieron validarse por otras razones |
| N/E | No editada |
Demostradores automáticos de teoremas seleccionados para probar la clase Isqrt.java
| Plataforma Why | Demostrador interactivo de teoremas | Versión | CME | NTV/NTT | NTI/NTT | NTETEV | NTNVOR |
| Why 2.30 | Alt-ergo | 0.93* | Sí | 6/6 | 0/6 | 0/6 | 0/6 |
| Why3 0.71 | Sí | 5/6 | 0/6 | 1/6 | 0/6 | ||
| Why 2.30 | Simplify | 1.5.4* | Sí | 4/6 | 0/6 | 0/6 | 2/6 |
| Why3 0.71 | Sí | 0/6 | 2/6 | 4/6 | 0/6 | ||
| Why 2.30 | Gappa | 0.15.1* | Sí | 0/6 | 6/6 | 0/6 | 0/6 |
| Why3 0.71 | Sí | 2/6 | 4/6 | 0/6 | 0/6 | ||
| Why 2.30 | Eprover | 1.4 Namring* | N/S | N/S | N/S | N/S | N/S |
| Why3 0.71 | Sí | 4/6 | 0/6 | 2/6 | 0/6 | ||
| Why 2.30 | haRVey21 | 0.5.10* | N/S | N/S | N/S | N/S | N/S |
| Why3 0.71 | N/S | N/S | N/S | N/S | N/S | ||
| Why 2.30 | Zenon22 | 0.6.3* | N/S | N/S | N/S | N/S | N/S |
| Why3 0.71 | N/S | N/S | N/S | N/S | N/S | ||
| Why 2.30 | SPASS | 3.7* | N/S | N/S | N/S | N/S | N/S |
| Why3 0.71 | Sí | 3/6 | 0/6 | 3/6 | 0/6 | ||
| Why 2.30 | Vampire | 0.6* | Sí | 4/6 | 0/6 | 2/6 | 0/6 |
| Why3 0.71 | No | ?/6 | ?/6 | ?/6 | ?/6 |
Proyecto aún en etapa de desarrollo tal como lo especifica su página principal http://harvey.loria.fr/
Proyecto aún en etapa de desarrollo tal como lo especifica su página principal http://zenon-prover.org/
Los experimentos y resultados presentados pueden servir como base para investigadores que deseen obtener información sobre el comportamiento de la plataforma Why 2.30 y Why3 0.71, con sus respectivos demostradores automáticos de teoremas y demostradores interactivos de teoremas. Por otro lado, y sin olvidar el objetivo que da origen a este trabajo, los resultados permitieron determinar qué versión o versiones de la plataforma Why soportaría XJML 1.0.
Finalmente, la versión de la plataforma de Why así como los demostradores automáticos de teoremas y demostradores interactivos de teoremas fueron seleccionados de acuerdo con los criterios mostrados en la tabla 9.
Criterios para seleccionar la plataforma de Why que dará soporte a FSPVRunner
| Criterio | Why 2.30 | Why3 0.71 |
| Consistencia de resultados | Sí | No1 |
| Soporte continuo de la plataforma | No | Sí |
| Soporte para múltiples demostradores automáticos deteoremas y demostradores interactivos de teoremas | No | Sí |
| Los resultados son estables | Sí | No |
Debido a la gran discrepancia de resultados entre las dos versiones de la plataforma Why con distintos demostradores automáticos de teoremas (tablas 6 y 7), se decidió realizar los experimentos con ambas versiones de la plataforma Why empleando únicamente aquellos demostradores automáticos de teoremas soportados por ambas versiones lo que permitió emitir conclusiones sobre dichas discrepancias en los resultados.
Dicho esto, XJML 1.0 soporta, a través de FSPVRunner, las siguientes versiones de la plataforma Why: Why 2.30 y Why3 0.71.
Actualmente se trabaja con experimentos, empleando la clase CuentaBancaria (Oriat, 2005). La clase será verificada en XJML 1.0 empleando las técnicas de verificación: RAC, ESC y FSPV. Después de esto, nos aseguraremos que no existan alteraciones entre los resultados presentados por XJML 1.0 y los resultados de cada técnica de verificación, ejecutadas por separado.
Cabe destacar que los resultados de este trabajo, permitieron delimitar los demostradores de teoremas (tanto automáticos como interactivos) que serán utilizados para los experimentos con la clase CuentaBancaria. De esta manera, los experimentos con la clase CuentaBancaria serán realizados con Alt-ergo 0.93, Simplify 1.5.4 y Gappa 0.15.1. No obstante, FSPVRunner no limita los demostradores automáticos de teoremas y/o demostradores interactivos de teoremas que puede emplear Why, más bien esta característica es determinada por el soporte que cada versión de la plataforma Why ofrezca.
Trabajos relacionadosEl lenguaje de modelado de java (JML) es quizás el lenguaje mejor conocido para el modelado de clases Java. Ha evolucionado a través de los años, pasando de JML2, JML3, JML4, JML5, JMLEclipse, y OpenJML, el cual es, hasta donde sabemos, el último esfuerzo de la comunidad de JML para producir un Entorno Integrado de Verificación.
Respecto a JMLEclipse, el primer lanzamiento (release) oficial aún está por determinarse11. Por otra parte, OpenJML, que es la siguiente generación de herramientas del núcleo de JML y soporta Java 1.7, está basado en OpenJDK y desafortunadamente la instalación falla si la máquina virtual de Java (JVM) no es la adecuada versión 1.712. Por ello, existe mucho trabajo por hacer, y las características u opciones de la interfaz gráfica de usuario (GUI) del complemento (plug-in) de Eclipse aún no están definidas13
XJML emplea el Lenguaje de Marcas Extensible (XML, Extensible Markup Language) como lenguaje para escribir el contrato para una clase Java. El uso de XML se debe a su importante papel en el intercambio de una gran variedad de datos. En este sentido, PiXL (Protocol Interchange using XML Languages) (Del-Mar et al., 2007) es un claro ejemplo de cómo las tecnologías y estándares basados en XML pueden utilizarse para la integración de herramientas de análisis. Sin embargo, PiXL no tiene soporte para JML.
Existe una comunidad de JML experimentando con el lenguaje, y los últimos esfuerzos se centran en construir un Entorno Integrado de Verificación (Chalin et al., 2008), el cual soporte e integre RAC, ESC y FSPV.
De estas tres técnicas de verificación, FSPV parece ser la más difícil de integrar y el último intento por lograr esto (OpenJML) aún no está listo. Creemos que XJML es el primero en su tipo, donde las expresiones del lenguaje pueden ser embebidas en un archivo XML (el contrato) para una clase Java, en lugar de la misma clase. Además, hasta donde sabemos XJML es la primera herramienta que integra RA, ESC y FSPV, y es este último el componente de interés en este trabajo, y que a diferencia de JML4 y JMLEclipse, XJML emplea la plataforma Why gracias al componente FSPVRunner del subsistema Runners de XJML.
En este último aspecto, creemos que este es el primer trabajo donde se realizan experimentos y se analizan los resultados del componente FSPVRunner de XJML y que puede ser el primero de una serie de experimentos para verificar la eficiencia y eficacia de XJML, con el fin de identificar puntos débiles o áreas de trabajo que apoyen en la verificación de programas Java.
Trabajos futurosActualmente se trabaja en experimentos con la clase CuentaBancaria y el componente FSPVRunner. Después de esto se analizarán y compararán los resultados asegurando que no existan alteraciones entre los resultados y la ejecución de FSPV a través de la plataforma Why.
Respecto a XJML 1.0 cabe destacar que soporta precondiciones, postcondiciones e invariantes de clase, así que se espera que en las siguientes actualizaciones de XJML podamos ofrecer soporte para más expresiones de JML. La tercera cosa por hacer es construir una Interfaz Gráfica de Usuario para XJML.
Respecto a FSPVRunner y las pruebas presentadas en este trabajo, se ejecutarán los experimentos en al menos un equipo más, con más de 4GB de RAM, un microprocesador con más de dos núcleos y velocidad mayor de 2.20GHz.
Para los experimentos deberá asignarse un tiempo mayor a 30 segundos, que fue el tiempo asignado en este trabajo, por lo que se recomienda se ejecuten primordialmente en Why3 0.71 con Alt-ergo 0.93, debido a que fueron los de mayor éxito en FSPV.
Este trabajo fue parcialmente patrocinado por el proyecto: Desarrollo de una infraestructura tecnológica como apoyo a la Comisión de Derechos Humanos del Estado de Tabasco, usando herramientas de software de vanguardia en atención a grupos vulnerables, en atención a un proyecto de Fondos Mixtos y en atención a la convocatoria del CONACYT 2008. Clave del proyecto: TAB–2008–C03–95740.
Queremos agradecer también a Gary T. Leavens, Kuat Yessenov, Greg Dennis, y Homero Alpuín por todo su apoyo, respuestas de correo electrónico, sugerencias y más.
Edgar Darío Ramírez-de León. Maestro en sistemas computacionales y licenciado en sistemas computacionales por la División Académica de Informática y Sistemas (DAIS) de la Universidad Juárez Autónoma de Tabasco (UJAT). Profesor-Investigador en la DAIS-UJAT. Miembro del Sistema Estatal de Investigadores (SEI) del estado de Tabasco. Ingeniero de Software. Áreas de interés: verificación y validación de sistemas, model checking, inteligencia de negocios, data warehouse y data mining.
Oscar Chávez-Bosquez. Profesor-investigador de la división académica de informática y sistemas de la Universidad Juárez Autónoma de Tabasco. Maestro en sistemas computacionales, ha escrito diversos artículos tratando temas modelos formales de desarrollo de software, y de optimización combinatoria en el área de metaheurísticas aplicadas a problemas NP-Completos. Ha participado en proyectos con financiamiento externo. Actualmente cuenta con el perfil PROMEP y es miembro del Sistema Estatal de Investigadores.
Julián Javier Francisco-León. Desarrollo y transferencia de tecnología en sectores productivos con necesidades en el área de multimedia. Integran soluciones tecnológicas utilizando elementos multimedios, animación así como sistemas inmersivos 3D y realidad virtual. Ha participado en proyectos desarrollando sistemas para los museos Parque Museo de La Venta y Museo Regional de Antropología Carlos Pellicer Cámara.
En la sección de resultados y discusión encontrará la URL de descarga de cada uno de ellos.
Tal como se especifica en http://sourceforge.net/apps/trac/jmlspecs/wiki/JML4%20Setup y http://sourceforge.net/apps/trac/jmlspecs/wiki/JML4%20HowTo%20Run%20Tests.
http://sourceforge.net/apps/trac/jmlspecs/wiki/JML4 y http://sourceforge.net/apps/trac/jmlspecs/wiki/JmlEclipse.
10 Las propiedades de solidez o consistencia (soundness) y completitud (completness) son las que se piden a cualquier método de validación. La propiedad de solidez nos garantiza que el método solo nos dará conclusiones válidas y la completitud nos garantiza que podremos obtener todas las conclusiones derivables.
Vampire 0.6 no siempre arroja los mismos resultados
Como se indica en http//sourceforge.net/apps/trac/jmlspecs/wiki/JmlEclipse
Tomado de The OpenJML User Guide, página 13, disponible en http://jmlspecs.sourceforge.net/OpenJMLUserGuide.pdf