Totality

An operation is total if it is defined on every state which

satisfies the state invariant

Enter1 is not total. We need to add additional specifications.

Previous slide

Next slide

Back to first slide

View graphic version