|
Descripción
|
|
|---|---|
| En las últimas dos décadas, una variedad de sofisticadas herramientas de análisis de terminación se han desarrollado. Estos incluyen los analizadores para sistemas de reescritura de terminos , lógicos y los de lenguajes funcionales. El análisis de terminación puede considerarse como otro tipo de análisis de uso de recursos, y también se ha estudiado en el contexto de varios lenguajes de programación. Tradicionalmente, en el contexto de la programación declarativa y, recientemente, para lenguajes imperativos y orientados a objetos (OO). De hecho, existen analizadores de terminación para OO que son capaces de probar terminación de aplicaciones de tamaño medio a través de un análisis global, en el sentido de que se debe demostrar terminación para todo el código usado por esas aplicaciones. Sin embargo, el análisis global tiene desventajas importantes, tales como, su alto consumo de memoria y su falta de eficiencia. Ya que a menudo algunas partes del código tienen que ser analizadas una y otra vez, las librerías son un ejemplo primordial de ello. El análisis modular se ha estudiado en diferentes paradigmas desde la programación lógica a la programación orientada a objetos. La mayoría de los trabajos existentes que se centran en el análisis modular se aplican a los análisis específicos con propiedades particulares o dominios abstractos. Las herramientas de análisis de terminación se esfuerzan por encontrar pruebas de terminación para la mas amplia clase de programas (que terminen) como sea posible. Aunque existen varias herramientas que son capaces de probar terminación de programas no triviales, cuando se trata de aplicarlos a programas realistas, todavía hay una serie de problemas abiertos. En se identifican una serie de dificultades para resolverse con el fin de tratar los campos numéricos en la terminación y se proponer algunas ideas para un análisis ligero que es capaz de probar terminación de programas Java-like secuenciales en presencia de campos numéricos. Técnicas automatizadas para demostrar terminación se basan normalmente en los análisis que mantienen un registro del tamaño de la información, tales como el valor de los datos numéricos o el tamaño de las estructuras de datos. En particular, los análisis deben hacer un seguimiento de cómo (el tamaño de) los datos involucrados en el bucle cambian a través de sus iteraciones. Esta información se utiliza para especificar una ranking function para el bucle, que es una función que disminuye estrictamente en cada iteración del bucle, lo que garantiza que el bucle se ejecutará un número finito de veces. Algunos análisis sensible a los campos se han desarrollado en los últimos años. Para asignar estructuras de datos en el heap, el pathlength es un dominio abstracto que proporciona una aproximación segura de la longitud de la referencia más larga alcanzable desde las variables de interés. Esto permite probar terminación de los bucles que recorren las estructuras de datos acíclicos tales como listas enlazadas, árboles, etc. Sin embargo, las técnicas propuestas en para los campos numéricos no son efectivos para los campos de referencia. Porque para el seguimiento de los campos de referencia, replicar los accesos de campo por las variables locales, presenta problemas de aliasing no deseado entre los campos y variables locales. Por otro lado, el enfoque sensible al contexto que se presenta en es capaz de manejar los campos mediante una transformación polivariante. | |
|
Internacional
|
Si |
|
ISBN
|
|
|
Tipo de Tesis
|
Doctoral |
|
Calificación
|
Sobresaliente cum laude |
|
Fecha
|
18/02/2011 |