Initial State Proof Obligation:
One of the things that we need to prove or at least convince ourselves of in some other way, about every specification that we write is that an initial state exists.
In the case of the classroom system this proof obligation is expressed by the formula ?Class1’ ? InitClass1’
?d’: P Person | #d’ <= Max ? #d’ <= Max ? d’ = ?
? < restricted existential is equivalent to the unrestricted form>
?d’: P Person ? #d’ <= Max ? #d’ <= Max ? d’ = ?