0
$\begingroup$

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

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ This is definitely not a research-level question. It's about ambiguity of notation. I have added an answer nonetheless. $\endgroup$ – Vijay D May 13 '13 at 23:08
2
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Thank you for your answer! I have edited the link in the question. I hope it works now. $\endgroup$ – Belgi May 13 '13 at 23:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.