Hoare logic: https://en.wikipedia.org/wiki/Hoare_logic

> 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