3 ms·
Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area
by p_l 5y ago
Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
- dandotway 5y agoThe SPARK example I found uses singly-linked lists and says doubly-linked lists and graphs with cycles are not supported: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)