Hoare Triple

Hoare Triple(Q) is the primitive of Hoare logic for describing a computable function.

Wikipedia Excerpt

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.