3 ms·

So how amenable is tla+ to automatic translation to an existing programming language?

ahelwer 10y ago
Amenable? Probably fairly amenable. It hasn't been done yet, though. It likely wouldn't be translation so much as proving that the existing code refines a TLA+ spec.
- pron 10y ago
  Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter). C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_14 http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1... Java: http://ieeexplore.ieee.org/document/6042069 http://ieeexplore.ieee.org/document/6042069 The C work seems more thorough.
  - ahelwer 10y ago
    Amazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.
hwayne 10y ago
IMO not very. It's easy in TLA+ to write things like "randomly select some bijective function from the power set of N to [0, 1]", which can be really handy for speccing but isn't exactly programming-friendly. I personally think of this as a good thing, actually. TLA+ can be simpler and more expressive than it would be if it had to also be translatable. So you can't guarantee your implementation matches your spec. All the more reason to write unit tests!
- pron 10y ago
  That is not such a big problem. Many operators in TLA+ -- like division -- are defined in terms of CHOOSE, but that doesn't stop TLC from implementing them efficiently. It's very easy to supply efficient implementations for various built in constructs, and tell you that you shouldn't use CHOOSE in your own definitions that you want to be automatically translated. So the data and data operations aren't the big problem; the control state is a bigger problem: It is hard to translate TLA+ constructs to programming language idioms like subroutines, loops and threads.
a-saleh 10y ago
You might want to investigate the Bloom project. That is the only language I know that uses temporal logic as its base while still viable for writing actual running services. Didn't use it, but watch a few presentations, i.e: https://channel9.msdn.com/Events/Lang-NEXT/Lang-NEXT-2012/Bloom-Disorderly-Programming-for-a-Distributed-World https://channel9.msdn.com/Events/Lang-NEXT/Lang-NEXT-2012/Bl...

Amenable? Probably fairly amenable. It hasn't been done yet, though. It likely wouldn't be translation so much as proving that the existing code refines a TLA+ spec.

pron 10y ago
Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter). C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_14 http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1... Java: http://ieeexplore.ieee.org/document/6042069 http://ieeexplore.ieee.org/document/6042069 The C work seems more thorough.
- ahelwer 10y ago
  Amazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.

hwayne 10y ago

IMO not very. It's easy in TLA+ to write things like "randomly select some bijective function from the power set of N to [0, 1]", which can be really handy for speccing but isn't exactly programming-friendly. I personally think of this as a good thing, actually. TLA+ can be simpler and more expressive than it would be if it had to also be translatable. So you can't guarantee your implementation matches your spec. All the more reason to write unit tests!

pron 10y ago
That is not such a big problem. Many operators in TLA+ -- like division -- are defined in terms of CHOOSE, but that doesn't stop TLC from implementing them efficiently. It's very easy to supply efficient implementations for various built in constructs, and tell you that you shouldn't use CHOOSE in your own definitions that you want to be automatically translated. So the data and data operations aren't the big problem; the control state is a bigger problem: It is hard to translate TLA+ constructs to programming language idioms like subroutines, loops and threads.

a-saleh 10y ago

You might want to investigate the Bloom project. That is the only language I know that uses temporal logic as its base while still viable for writing actual running services. Didn't use it, but watch a few presentations, i.e: https://channel9.msdn.com/Events/Lang-NEXT/Lang-NEXT-2012/Bloom-Disorderly-Programming-for-a-Distributed-World https://channel9.msdn.com/Events/Lang-NEXT/Lang-NEXT-2012/Bl...