Skip & Abort
Skip
- Execution of the skip command does nothing.
- It is equivalent to the empty command;
- It is the identity transformer
- wp(skip, R) = R
-
Abort
- wp(abort, R) = False
- Abort should never be executed as it may only be executed in a state satisfying False.