Example (from Reddit user thiez):
#[postcond = "self.x=\old(self.x)+1"]
fn inc(&mut self) {
self.x += 1;
}
The /old function in this example allows us to speak about the old state of self.x.
Need to figure out the best syntax for this, perhaps allowing some variables to be introduced and filled with the old values. This probably needs to be opt-in since there will be a cost of the copy.
Example (from Reddit user thiez):
The
/oldfunction in this example allows us to speak about the old state ofself.x.Need to figure out the best syntax for this, perhaps allowing some variables to be introduced and filled with the old values. This probably needs to be opt-in since there will be a cost of the copy.