Verificación de Programas Paralelos

Resumen

En este tercer artículo de la serie que venimos presentando sobre la verificación axiomática de
programas (en su variante de la Lógica de Hoare), tarea emprendida en el marco del proyecto del CAETI de construcción de un ambiente para asistir en el desarrollo de software, comenzamos a tratar el paradigma concurrente, para el que más se justifica el empleo de un método de prueba riguroso. Trabajamos con el modelo de los programas paralelos, programas concurrentes con procesos que comparten variables y se comunican a través de ellas (a pesar de la problemática común, por razones de espacio dejamos para el cuarto y último artículo el modelo de los programas distribuidos, programas concurrentes cuyos procesos son disjuntos y se comunican por medio de
mensajes). Como en las publicaciones anteriores, remarcamos la idea de utilizar las axiomáticas
descriptas como guías para obtener programas correctos por construcción. Destacamos además
que las nociones fundamentales de la verificación axiomática observadas cuando analizamos los
programas secuenciales, principalmente los predicados invariantes y las funciones variantes. se preservan en el contexto concurrente, a pesar de tener que considerarse una mayor variedad de clases de programas, propiedades y aspectos (metodológicos, semánticos, metateóricos)