3 ms·
Sometimes the invariants are obvious. For example, some sorting algorithms are very complex in the details of their implementation - but they all have the qual
by michaelt 4y ago
Sometimes the invariants are obvious.
For example, some sorting algorithms are very complex in the details of their implementation - but they all have the quality that given an input, the output should be the same set of elements, in order.
- im3w1l 4y agoThat'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+