# 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

• This is definitely not a research-level question. It's about ambiguity of notation. I have added an answer nonetheless. – Vijay D May 13 '13 at 23:08

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$.