Mixing TLA+ and SOS

[Behrooz Nobakht]

Hi there,

Structural operational semantics (SOS) [1] is a formal method to specify the semantics of a programming language esp. at runtime

using transition systems for program state. 

Suppose that for programming language L, there exists an SOS spec. One of the main features of L is concurrency.

I am wondering and curious if TLA+ can be used to specify such a programming language, and thus the runtime 

that a running programming in L would create. The goal is to be able to prove/disprove certain properties of the runtime

of the language in regards with concurrency, such as dead locks or live locks.

I am very new to TLA so excuses if the question lacks certain prerequisites.

Thanks,

Behrooz

[1]: https://www.alice.virginia.edu/~weimer/2006-655/reading/plotkin81structural.pdf

[fl]

Hi Behrooz,

obviously yes you can. A semantic is specified with a series of functions F: E X. S --> S or inference rules

where E are expressions and S is a state (variables with their values). Here you specify your expressions

thanks to records in a treeish way (this avoids the need to parse your expressions). And your state by TLAPLUS

variables. And the functions by functions and inference rules by TLAPLUS actions.

--

FL

[Leslie Lamport]

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.

Leslie

[Behrooz Nobakht]

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

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--

-- Behrooz Nobakht