jueves, noviembre 10, 2005
La herramienta secreta de Microsoft contra los bugs
Cuentan en un artículo de Wired que Microsoft tiene una herramienta secreta contra los bugs: un analizador estático de código. Si no entendí mal el artículo (no tengo ganas de leerme los más serios que hay en el sitio de SLAM, que es como se llama el invento), es un analizador estático de código. Se basa en hacer una especificación formal del software a analizar.
Hacer especificaciones formales de cualquier programa no trivial es muy difícil. La herramienta está pensada sólo para los controladores de dispositivos, que por lo visto tienen unas reglas muy específicas. Imagino que lo único que puede probar es que no te van a tirar el sistema, no que hacen lo que tienen que hacer de verdad.
Como dijo Donald Knuth: «Beware of bugs in the above code. I have only proved it correct, not tried it.» :-)
Hacer especificaciones formales de cualquier programa no trivial es muy difícil. La herramienta está pensada sólo para los controladores de dispositivos, que por lo visto tienen unas reglas muy específicas. Imagino que lo único que puede probar es que no te van a tirar el sistema, no que hacen lo que tienen que hacer de verdad.
Como dijo Donald Knuth: «Beware of bugs in the above code. I have only proved it correct, not tried it.» :-)
Comentarios:
Publicar un comentario
