2. Hoare logic

Hoare logic is concerned with the axiomatic properties of programming languages and the associated technologies for reasoning about programs in order to demonstrate their correct operation. These properties are defined on the basis of the language's syntactic constructs, as in the case of typing and behavioral properties. In this section, we recall the grammar of the language "L", with its typing properties and behavioral properties [H 3 880] . After detailing the axiomatic properties, we then show how it is possible to reason about programs in order...