To be able to write postconditions for mutating functions, we might need to "capture" the input, copying it before it is mutated so that we can use it the post condition. E.g. in sort!(x), we want to say that after computation, x is the sorted version of x before the computation.
Implement variable capturing for post conditions.
To be able to write postconditions for mutating functions, we might need to "capture" the input, copying it before it is mutated so that we can use it the post condition. E.g. in
sort!(x), we want to say that after computation,xis the sorted version ofxbefore the computation.