Summary

Problems

• difficult to choose the correct invariant and assertions

• infeasible for large and complex programs

• too theoretical

Motivation

• clarifies thinking during design stage

• formal mathematical way of proving programs

• theories are the basis for programming tools