Verificación de Programas Paralelos

Abstract

In this third article of the series that we have been presenting on the axiomatic verification of
programs (in its variant of Hoare´s Logic), a task undertaken within the framework of the CAETI
project for the construction of an environment to assist in software development, we begin to deal
with the concurrent paradigm, for which the use of a rigorous proof method is most justified. We work with the model of parallel programs, concurrent programs with processes that share variables and communicate through them (despite the common issue, for space reasons we leave for the fourth and last article the model of distributed programas, concurrent programs
whose processes are disjoint and communicate through messages). As in previous publications, we stress the idea of using the described axiomatics as guides to obtain correct programs by construction. We also highlight that the fundamental notions of axiomatic verification observed when we analyzed sequential programs, mainly invariant predicates and variant functions, are preserved in the concurrent context, despite having to consider a greater variety of program
classes, properties and aspects (methodological, semantic, metatheoretical)