> how do you do it actually for nontrivial preconditions like "this list must be sorted"? This depends on your data model, of course. But for a list of integer

> how do you do it actually for nontrivial preconditions like "this list must be sorted"? This depends on your data model, of course. But for a list of integers you could do the following: 1. Have a unique data type that is the list of Deltas, plus the initial element (So for instance the list [5, 3, 6] would be encoded as (3, [2, 1]). 2. Provide a sort function that creates such a sorted list. 3. Make the sorted list your input parameter. This is obviously oversimplified, but I hope you get the idea. A cheaper alternative is to 1. Make an opaque datatype "sorted list", together with a function that translates this type to a normal list. Implemen this type just as a list, but keep the implementation private. 2. Provide a function sort, that is the only function that can yield that type. 3. Demand that type as input.