Avances en Documentación de Software

Una de las razones por las que he tenido esto un poco parado tiene que ver con grandes avances en documentación de software. En concreto gracias a los chicos de Microsoft Research que se encargan de Spec Explorer y Asml.

La cosa es que esta semana he tenido que dar una charla sobre el tema para una clase de especificación formal de software, y he meado un poco de sangre. ¿Que por qué? Pues muy sencillo. Resulta que estos chicos consideran documentación un simple pantallazo de un cuadro de diálogo para configurar. ¿Que quieres documentar la configuración de los tests? Pues nada mejor que un pantallazo y ya está :-s

Pero lo mejor de todo es encontrarse páginas enteras que sólo tienen títulos y, de vez en cuando, el típico to do: talk here about… whatever. En fin… que la cosa parece interesante, pero ya les vale. Básicamente se trata de especificar matemáticamente las interfaces de los componentes software, de forma que se pueda comprobar en tiempo de compilación si un programa funciona o no (aunque hay ciertos problemas para comprobar teoremas porque son problemas NP). Eso se puede hacer con Resolve bastante bien, pero con Asml es un poco aventurado decir eso. Sin embargo está curioso para crear modelos de software en base a máquinas de estado, a partir de las cuales se puede testear software, pero no comprobar en tiempo de compilación.