Implies
The implies boolean operator can feel a bit awkward to start with, as it is crafted for a very specific scenario: to be used in Invariants to a condition that is only relevant if another condition matched.
implies combines two boolean arguments. If the first argument is false, the result is true, otherwise, the result is the second argument. The idea is that the trueness of the second condition only matters if the first is true.
The following (contrived) example of a class representing a traffic light illustrates it:
type
PedestrianCrossing = class;
public
property CarLight: Color;
property PedLight: Color;
public invariants
CarLight = Color.Green implies = PedLight = Color.Red;
PedLight = Color.Green implies = CarLight = Color.Red;
end;
The invariant test here ensures that, if one direction's traffic light is green, then the other must be red, to avoid accidents. If it is not green, then the other light does not matter (it could be green, red, yellow or even purple, for as far as the test is concerned).
Essentially, x implies y translates to (not x) or y, but expresses the intent of the check much clearer.