<p>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 </p>

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

<p>See the Wikipedia page on <a href="http://en.wikipedia.org/wiki/Material_conditional" rel="nofollow">material implication</a> for other notation for implication.</p>

CC BY-SA 3.0
2013-05-13T23:07:22.183Z
Thank you for your answer! I have edited the link in the question. I hope it works now.
Belgi
CC BY-SA 3.0
2013-05-13T23:03:27.097Z
2013-05-13T23:03:27.097Z
Vijay D
<p>I am reading an article called <a href="http://www.sciencedirect.com/science?_ob=MiamiImageURL&amp;_cid=271538&amp;_user=32321&amp;_pii=0304397581901109&amp;_check=y&amp;_origin=article&amp;_zone=toolbar&amp;_coverDate=31-Dec-1981&amp;view=c&amp;originContentFamily=serial&amp;wchp=dGLzVlV-zSkWb&amp;md5=2073f527aa2be434886953d7aaa0f7d3&amp;pid=1-s2.0-0304397581901109-main.pdf" rel="nofollow noreferrer">The temporal semantics of concurrent programs</a>
.</p>
<blockquote>
<p>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.</p>
<p>In order to prove that a program P posseses a property R, one has only
to prove the implication <span class="math-container">$$W(P)\supset R$$</span>
My question is this: Didn't they get the containment the other way
around ?</p>
</blockquote>
<p>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 <span class="math-container">$$W(P)\subset R$$</span></p>
<p>Do I understand something wrong here, or is there a mistake in the</p>

CC BY-SA 3.0
2013-05-13T23:08:47.540Z
This is definitely not a research-level question. It's about ambiguity of notation. I have added an answer nonetheless.
Vijay D
<program-analysis>
The meaning of: a program P posseses a property R
Belgi
# The meaning of: a program P posseses a property R

(Asked by: username_0 on 2013-05-13)

I am reading an article called [The temporal semantics of concurrent programs](http://www.sciencedirect.com/science?_ob=MiamiImageURL&_cid=271538&_user=32321&_pii=0304397581901109&_check=y&_origin=article&_zone=toolbar&_coverDate=31-Dec-1981&view=c&originContentFamily=serial&wchp=dGLzVlV-zSkWb&md5=2073f527aa2be434886953d7aaa0f7d3&pid=1-s2.0-0304397581901109-main.pdf)
.

> 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

**Tags:** program-analysis
> **Comments:**
> **username_1**: This is definitely not a research-level question. It's about ambiguity of notation. I have added an answer nonetheless.  

---

## 1 answers

### Answer by username_1 on 2013-05-13. Score: 2 | Accepted answer

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](http://en.wikipedia.org/wiki/Material_conditional) for other notation for implication.

> **Comments:**
> **username_0**: Thank you for your answer! I have edited the link in the question. I hope it works now.  

---

