3 ms·
Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes
by unboxed_type 9y ago
Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense.
Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.
- nickpsecurity 9y agoNo, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.