Verification of Nondeterministic Programs

Abstract

We continue with our series of introductory articles on the axiomatic verification of programs.
In this second work, we focus on the nondeterministic sequential paradigm, always within the framework of imperative input/output programs. As nondeterminism is manifested in concurrency, the article also serves as an introduction to the verification of concurrent programs, in which a formal treatment of correctness verification is more justified due to their complexity. We work with a classic programming language, with nondeterministic conditional selections and repetitions, and then incorporating random assignments. For the verification of the programs we propose an adaptation of the verification axiomatic method described in the previous publication, limited to deterministic sequential programming. We present examples of the application of the method and a systematic program development is also included, emphasizing again the approach of using the axioms and rules for programming as well as verifying, in order to obtain correct programs by
construction. Finally, we introduce the concept of fairness, which effect is to reduce the degree of
nondeterminism of a program based on certain equity criteria in the execution environment, and we describe a couple of adaptations in the verification rules to contemplate this aspect