Introduction to Program Verification

Abstract

We start a series of four introductory articles regarding the axiomatic verification of programs in the context of imperative input/output programs. In this article, we introduce the axiomatic verification method for deterministic sequential programs, and we show some application examples. Although program verification is presented as an a posteriori activity (given a program
and a specification, verify that the program satisfies the specification), the main idea sustained in the article, and in the entire series, is to take into account the method axioms and rules both for programming as well as verifying, in order to obtain correct programs by construction. With this perspective, a systematic development of a program based on the studied axiomatics is presented at the end