¹However, iff a modifiesclause lists some object variable, the task of verifying that the other variables of the object are not modified, is added to the verification of the method’s postcondition