[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Mixing TLA+ and SOS

Thanks for the explanation and hints to start. 

The work that I am following to start is actually about a modeling language that is designed for
concurrent objects/systems. In this language, there's a principle of Run-To-Completion which I 
think will prevent the example in Java. But, more interestingly, there's great interest in translating
the models into equivalent Java which brings back the question. 

The language is ABS, http://link.springer.com/10.1007%2F978-3-642-25271-6_8

On Fri, Jul 15, 2016 at 7:36 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:
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 statement

   b = ! 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.

-- Behrooz Nobakht