Una herramienta para el testeo de propiedades formales de programas basada en técnicas de demostración automática

Abstract

La aplicación permite demostrar la corrección de argumentaciones tanto en lógica proposicional como en lógica de primer orden por el método de los tableaux. El usuario puede introducir un conjunto de premisas o cláusulas y comprobar si de ellas se deduce una determinada propiedad que introducirá en la conclusión. La aplicación generará el árbol correspondiente y deducirá del mismo si la argumentación válida o falaz. Por otra parte, permite la demostración de propiedades muy sencillas de algunos programas. Comprueba (también con el método de los tableaux) si de una precondición, una postcondición y un cierto valor (o rango de valores) de las variables de un programa se puede inferir una propiedad. El uso de la aplicación es sencillo y está pensado para cualquier tipo de usuario interesado en el estudio de propiedades lógicas. No se requieren grandes conocimientos para poder hacer uso de ella. [ABSTRACT] The application allows to as much demonstrate the correction of argumentations in propositional logic as in logic of first order by the method of tableaux. The user can introduce a set of premises or clauses and verify if of them a certain property is deduced that will introduce in the conclusion. The application will generate the tree corresponding and will deduce if the argumentation is valid or not. On the other hand, it allows the demonstration of very simple properties of some programs. It verifies (also with the method of tableaux) if a precondition, a postcondition and a certain value (or rank of values) of the variables of a program can infer a property. The use of the application is simple and it is thought for any type of user interested in the study of logic properties. Great knowledge is not required to be able to make use of it.