3 ms·
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+
by 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 agoShowing 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 agoAmazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.