4 ms·
Yeah. And TLA+ can confirm that the design is sound, but it can’t confirm that the implementation conforms to the design. QuickCheck style tests can’t solve tha
by bunderbunder 20d ago
Yeah. And TLA+ can confirm that the design is sound, but it can’t confirm that the implementation conforms to the design. QuickCheck style tests can’t solve that problem, but perhaps they can mitigate it.
- agentultra 18d agoI think it might be possible to write a TLA+ parser and generate QuickCheck tests from it that will exercise invariants at least.