4 ms·
Yeah but why not generate code from your specification? Or create a model of the specification that you can interrogate in code?
by shusson 8y ago
Yeah 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.