2 ms·
That's a post-condition not an invariant.
by im3w1l 4y ago
That's a post-condition not an invariant.
- Bjartr 4y agoThe invariant form would be something like: for any program state, there is eventually a state that will be reached that contains the ordered set containing input elements. My phrasing is rough, but it is an invariant that can be expressed by TLA+