Hoare logic specifies what a command guarantees when it starts in a state satisfying a given assumption.

A Hoare triple

$${P}\ C\ {Q}$$

means: if precondition $P$ holds before command $C$ and $C$ terminates, then postcondition $Q$ holds afterward. This is a statement of partial correctness; termination is a separate obligation unless the logic explicitly includes it.

For assignment, the rule

$${Q[e/x]}\ x:=e\ {Q}$$

works backward from the desired postcondition. To prove

$${x=3}\ x:=x+1\ {x=4},$$

substitute $x+1$ for $x$ in the postcondition $x=4$, obtaining the required precondition $x+1=4$, equivalent to $x=3$.

Sequencing composes triples:

$$\frac{{P}C_1{R}\qquad {R}C_2{Q}} {{P}C_1;C_2{Q}}.$$

Conditionals prove the two branches under assumptions that the condition is true or false. Loops additionally require an invariant preserved by every iteration.

Hoare logic is an axiomatic semantics: instead of saying how a program executes, it defines rules for proving properties of its executions. It connects specifications, assertions and program structure in a form suitable for verification.