Sure, here are some postconditions for ChangeOil(): - engine has appropriate amount of oil in it - oil filter in place - drain plug torqued correctly - dip

Sure, here are some postconditions for ChangeOil(): - engine has appropriate amount of oil in it - oil filter in place - drain plug torqued correctly - dip stick present - oil cap on No matter what the outcome of the operation (ie error paths or happy path), ChangeOil promises to return with the car in a state that fulfills those conditions. In order to do that, some preconditions need to be fulfilled too: - car has some amount if oil in engine - car is able to start - no major noises