If a dog is hungry, necessarily the dog is slobbering. Fido is hungry. Fido is not slobbering. should lead either to an error or else changing Fido's state to not hungry
If a dog is hungry, necessarily the dog is slobbering.
Fido is hungry.
Fido is not slobbering.
should lead either to an error or else changing Fido's state to not hungry