Hoare logicHoare logic is the fundamental formalism introduced by C.A.R. Hoare in 1969 for reasoning about the correctness of imperative programs, building on first-order logic. We will now study Hoare logic for simple While programs. The logic deals with the notion of correctness vis a specification that consists of apreconditionprecondition and apostconditionpostcondition. The correctness of a program with respect to a givenspecificationin Hoare logicspecification is asserted by constructing a derivation in the inference system of Hoare logic. While doing so, one must identify an invariant for every loop in the program.