Verification of Distributed Programs

Abstract

This article completes our series of four articles on the axiomatic verification of programas, which we propose within the framework of the CAETI project to build an environment to support software development. In particular, we conclude the analysis of concurrent programs begun in the previous publication, now considering the family of distributed programs, characterized by having processes with disjoint variables and that communicate through messages. As always,
we highlight the principle of using axiomatics as guides for obtaining correct programs by construction, and the observation that the fundamental notions of invariant predicate and variant function constitute the methodological basis in all programming paradigms