FL is correct that it's easy to encode an SOS semantics in TLA+. But
if you're talking about a real language with concurrency, I'd be
surprised if it has an SOS semantics. For example, in Java, if b is a
boolean variable that can be accessed by multiple threads, I have no
idea what the meaning is of the statementb = ! b ;If the people who designed the semantics of Java did anything like the
designers of two memory systems I've looked at--Alpha and Itanium--the
semantics is quite complicated, almost impossible to understand,
and unlikely to be describable with SOS.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.