10.7. Reads clauses🔗

(Also mentioned above under automated proof search.) A reads clause provides a lemma stating when the output of a deterministic procedure does not change. These particular reads lemmas work well in conjunction with modifies clauses to prove that particular procedure outputs have remained the same after the heap has been modified.

Reads clauses are useful to improve verification performance. The facts they provide work well together with the facts provided by modifies clauses, making it easier to prove which procedure values have remained unchanged after objects were modified.