Verifying a Machine Routine

Planned post. This page is a stub.

Preconditions, postconditions, calling conventions, faults, and termination.

Planned Coverage

Prove that a routine returns with the required result while respecting its execution contract.

Examples, definitions, and exercises will be developed here as the course progresses. See the course table of contents for the suggested reading order.