Relational Semantics

A relational semantics for an Imperative Programming Language $\mathcal{L}$ is an interpretation of the statements of $\mathcal{L}$ into a Relations $S\to S\to\Omega$ on some set of states $S$.