> The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form {P}C{Q} where P and Q. are assertions and C is a command.
> P is named the precondition and Q the postcondition: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic.
> Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language.
[...]
> Partial and total correctness
> Using standard Hoare logic, only partial correctness can be proven. Total correctness additionally requires termination, which can be proven separately or with an extended version of the While rule