Programas que usan punteros

Abstract

Se estudian dos enfoques distintos para el razonamiento sobre programas que manipulan punteros. Uno de los enfoques, propuesto por Reynolds, se basa en la separación espacial de las celdas en el heap. El otro, propuesto por Bornat, se basa en la sustitución de componentes, análogo al tratamiento de arreglos en la lógica de Floyd/Hoare. Como contribución de este trabajo, se definen predicados inductivos para trabajar con estructuras de datos sobre el heap (listas, árboles binarios de búsqueda y árboles generales) y se describe un método para construir programas verificados, iterativos, con punteros, a partir de una función recursiva final. También se verifican algoritmos de ejemplo con el fin de utilizar las estructuras definidas y comparar las lógicas presentadas.