Program Verification

Pre- and post-conditions

Invariants (loop, class?)

Hoare Logic?