Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revisionBoth sides next revision
people:etanter:tipos [2013/05/17 20:39] – etanterpeople:etanter:tipos [2013/05/17 21:47] – etanter
Line 14: Line 14:
 ------- -------
  
-El campo de la verificación de programas es por ende un pozo sin fin, un eterno compromiso entre la expresividad requerida para lo que se quiere verificar, y la amenaza de la indecidibilidad. Lo que se traduce en la práctica principalmente en sistemas de verificación conservadores, que se dedican a la semi-decidabilidad. Es decir, sistemas que sólo reportan que un programa cumple una cierta propiedad cuando lo pudieron demostrar, pero que rechazan programas donde no se puede demostrar dicha propiedad, a pesar de que posiblemente el programa la cumpla (Figura 1c).+El campo de la verificación de programas es por ende un pozo sin fin, un eterno compromiso entre la expresividad requerida para lo que se quiere verificar, y la amenaza de la indecidibilidad. En la práctica, muchas veces uno quiere la garantía absoluta que todos los programas malos son rechazados. Esto significa que los sistemas de verificación son conservadores: sólo reportan que un programa cumple una cierta propiedad cuando lo pudieron demostrar, pero inevitablemente van a rechazar algunos programas que sí cumplen la propiedad (Figura 1c). 
 Mientras que las técnicas más avanzadas de verificación de software, como el análisis formal y la verificación de modelos, no han tenido mucha aceptación en la industria de software--excepto en áreas críticas donde la correctitud absoluta es una necesidad vital (automóviles, cohetes, etc.)--existe una forma liviana de métodos formales que cada programador usa día a día, muchas veces sin preguntarse mucho de qué se trata: los sistemas de tipos. Mientras que las técnicas más avanzadas de verificación de software, como el análisis formal y la verificación de modelos, no han tenido mucha aceptación en la industria de software--excepto en áreas críticas donde la correctitud absoluta es una necesidad vital (automóviles, cohetes, etc.)--existe una forma liviana de métodos formales que cada programador usa día a día, muchas veces sin preguntarse mucho de qué se trata: los sistemas de tipos.