Propiedades Algebraicas y Decidibilidad del Transformador de Predicados wp sobre la Teoría de Conjuntos

Resumo

En este trabajo se presentan nuevas propiedades algebraicas del transformador de predicado wp sobre los operadores ∧, ∨, ¬, ⇒, ∀, ∃, min y max, demostrados independientemente del lenguaje de programación, usando propiedades generales de la semántica denotacional de los lenguajes. Adicionalmente se muestra un resultado que habla sobre la decidibilidad y cerradura del transformador de predicados wp sobre el lenguaje de programación GCL y usando aserciones escritas en el lenguaje de la teoría de conjuntos de Zermelo-Frankel-Skolem. En este trabajo se muestra que calcular wp de una instrucción de GCL y una aserción escrita en el lenguaje ZFS, es decidible y es otra aserción escrita en ZFS. No necesariamente se puede decidir el valor de verdad de dicha aserción resultante de calcular wp, aun teniendo todos los valores de sus variables libres, por lo que el resultado no contradice la indecidibilidad del problema de la parada.