The schema for DoEnter1 is total because it specifies what happens no matter what values its inputs and before variables have.

• The schema for DoEnter1 is total because it specifies what happens no matter what values its inputs and before variables have.

• Note, that the values of the before variables have to satisfy the before state invariant

Previous slide

Next slide

Back to first slide

View graphic version