2 ms·
For people who have experience with TLA+ do you generate implementation code from the TLA+? Or is the idea to only use it for some formal design specifications?
by shusson 8y ago
For people who have experience with TLA+ do you generate implementation code from the TLA+? Or is the idea to only use it for some formal design specifications?
- aeneasmackenzie 8y agoTLA+ is only for specification. In one of the papers on it Lamport mentions just putting a copy of the specification in a comment above the implementation. If you get a bug you just need to find where your implementation differs from your specification which he finds is usually pretty easy. If your code doesn't have a specification (of course usually less precise), fixing bugs is incoherent. How can you say come behavior is a bug?
- shusson 8y agoYeah but why not generate code from your specification? Or create a model of the specification that you can interrogate in code?
- aeneasmackenzie 8y agoYou would need to include irrelevant details. TLA+ is an actual declarative language, so it's not executable, but it can be model-checked.