I am reading an article called The temporal semantics of concurrent programs .
A construction is then given for assigning to a program P a temporal formula W(P) which is true on all proper execution sequences of P.
In order to prove that a program P posseses a property R, one has only to prove the implication $$W(P)\supset R$$ My question is this: Didn't they get the containment the other way around ?
If I understand correctly, a property,R, is a set of traces, for P to hold the property each trace of P needs to be in R, hence $$W(P)\subset R$$
Do I understand something wrong here, or is there a mistake in the