The Formal System of Dijkstra and Scholten

Abstract

The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding this logic to the point in which, for some time, it was not considered a logic, as logicians use the word. The main objections arise from the fact that: (i) symbolic manipulations seem to be based on the meaning of the terms involved, and (ii) some notation and the proof style of the logic are different, to some extent, from those found in the traditional use of logic. This paper presents the Dijkstra-Scholten logic as a formal system, and explains its proof-theoretic foundations as a formal system, thus avoiding any confusion regarding term manipulation, notation, and proof style. The formal system is shown to be sound and complete, mainly, by using rewriting and narrowing based decision and semi-decision procedures for, respectively, propositional and first-order logic previously developed by C. Rocha and J. Meseguer.

Se ha demostrado que la lógica de EW Dijkstra y CS Scholten es útil en las pruebas de corrección de programas y ha atraído a muchos seguidores en la investigación, la enseñanza y la programación. Sin embargo, existe confusión respecto a esta lógica hasta el punto de que, durante algún tiempo, no se consideró una lógica, como los lógicos usan la palabra. Las principales objeciones surgen del hecho de que: (i) las manipulaciones simbólicas parecen estar basadas en el significado de los términos involucrados, y (ii) alguna notación y el estilo de prueba de la lógica son diferentes, hasta cierto punto, de los que se encuentran en el uso tradicional de la lógica. Este artículo presenta la lógica de Dijkstra-Scholten como un sistema formal y explica sus fundamentos teóricos de prueba como un sistema formal, evitando así cualquier confusión con respecto a la manipulación de términos, la notación y el estilo de prueba. El sistema formal se muestra sólido y completo, principalmente, mediante el uso de procedimientos de decisión y semidecisión basados ​​en reescritura y estrechamiento para la lógica proposicional y de primer orden, respectivamente, desarrollados previamente por C. Rocha y J. Meseguer.