The UNITY Programming Logic

Logic for

• Specification,
• Design,
• Verification.

• Execution of statement $s$.
• If $p$ holds before $s$,
• then $q$ holds after $s$.

• We do not say what $P$ is.
• We say what we can expect from $P$.