Go backward to Assignment Statements
Go up to Top
Go forward to A Model of Program Execution

Quantified Assertions

For program F, we write quantified assertions

to denote that {p} s {q} holds for all statements (respectively for some statement) s in F.

Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine

Prev Up Next