Publicado en
Me da gusto estar retomando esta columna, luego de un receso de varios años en los que estuvo a cargo de Berenice Ruiz.
En el pasado SG Conference & Expo ofrecí la plática “La prueba de software y los special purpose languages”. Dado que al terminar varias personas me sugirieron abundar en el tema, aprovecharé este espacio para hacerlo durante esta y varias entregas más de esta columna.
A través de los años, el “estado del arte” de la disciplina del software ha estado fuertemente influenciado por el desarrollo de los lenguajes de programación. Es así que hemos pasado por lenguajes con distintos niveles de abstracción, distintos paradigmas (procedural, orientado a objetos, funcional), y ahora también con lenguajes de documentación, de especificación, y de arquitectura, entre otros. Una de las vertientes del estado del arte tiene que ver con lo que desde hace décadas se denomina como “Métodos Formales” (MF).
En términos generales, los MF son una tecnología mediante la cual:
- Se escribe la especificación del sistema a desarrollar utilizando un lenguaje formal1 (L1) probablemente del paradigma declarativo2, que luego es verificada con intervención humana y procesada mediante un compilador para así generar el código en otro lenguaje formal L2 , el cual representa un diseño de alto nivel.
- Este diseño a su vez es verificado con intervención humana y procesado mediante un compilador que genera el código en otro lenguaje formal L3 (usualmente del paradigma imperativo).
- Este código se procesa mediante un compilador para obtener finalmente el sistema ejecutable. Las verificaciones mencionadas suelen ser demostraciones matemáticas de que el código escrito en L1 o L2 tiene ciertas propiedades, por ejemplo que los requerimientos en L1 son consistentes (no existen contradicciones entre ellos) y completos (no quedan “huecos” en los requerimientos).
Podríamos decir que en el desarrollo de software siempre se utiliza un tipo de MF, pues finalmente se escribe el código en algún lenguaje Lx, que es procesado por un compilador Cx, el cual usualmente genera código ejecutable en un Ly. Sin embargo, esta transformación suele realizarse solamente para la fase final de las arriba descritas, la generación del código ejecutable a partir del programa escrito en un lenguaje de programación (usualmente imperativo), no para todo el ciclo de desarrollo Requerimientos->Diseño->Programación. Los métodos formales pueden abordar el ciclo completo, y se han utilizado principalmente para desarrollar sistemas críticos (aquellos en los que literalmente, si el software falla, hay personas que mueren), pues permiten entregar software que se demuestra que es libre de defectos.
Como ustedes sabrán, en e-Quallity nos especializamos en la prueba de software. Sin embargo ya desde el primer artículo que escribimos en SG hace 10 años (mayo de 2005)[1] escribíamos que es muy importante estar al tanto del desarrollo de la disciplina de los métodos formales, pues eso puede tener un enorme impacto en la manera no solo en la que realizamos pruebas, sino también en la que desarrollamos software.
La aplicación de métodos formales nos abre la posibilidad de desarrollar lenguajes propietarios para incrementar la productividad y la calidad en el desarrollo de software, pues vemos que el diseño y la implementación de lenguajes han sido muy poco explotados en nuestro país, aún cuando es algo que puede tener un gran impacto en nuestra competitividad.
En las siguientes entregas de esta columna veremos con más detalle “con qué se come” eso de desarrollar lenguajes propietarios, pero en general estaremos hablando de aplicar dos conceptos muy generales pero bastante poderosos: lenguajes y patrones. La ciencia puede verse como el descubrimiento y/o la invención de patrones que explican o describen cosas.
Para el siguiente lenguaje/patrón, consideren la sustitución planteada en la figura 1.
Figura 1. Ejemplo de patrón de sustitución
Lo que está a la izquierda del símbolo “=>” debe sustituirse por lo que está a su derecha. La sustitución ocurre siempre “en paralelo”; es decir: que todas las apariciones de lo que está a la izquierda de “=>” deben sustituirse por lo que está a la derecha simultáneamente. Partiendo de “|”, realicen 3 ciclos de sustituciones y piensen qué podría representar ese patrón/lenguaje.
En el siguiente número platicaremos más sobre este tipo de lenguajes/patrones y cómo se relacionan con los métodos formales.
Luis Vinicio León Carrillo es socio director y fundador de e-Quallity. Fue profesor-investigador en la universidad ITESO, y realizó una estancia de posgrado en Alemania, donde se dedicó a la investigación del Testing y los métodos formales.
- Log in to post comments