The meaning of: a program P posseses a property R 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
I cannot see the article and have to guess. The text makes clear that they are using the symbol $\supset$ as notation for implication. So you could read it as 


  In order to prove that a program $P$ possesses a property $R$, one has only to prove the implication 
  $W(P) \implies R$.


See the Wikipedia page on material implication for other notation for implication.