RefinementErrors.dfy(30,17): Error: a refining method is not allowed to add preconditions RefinementErrors.dfy(31,15): Error: a refining method is not allowed to extend the modifies clause RefinementErrors.dfy(34,14): Error: a predicate declaration (abc) can only refine a predicate RefinementErrors.dfy(35,8): Error: a field re-declaration (xyz) must be to ghostify the field RefinementErrors.dfy(37,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F RefinementErrors.dfy(38,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C') RefinementErrors.dfy(38,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A') RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B') RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq' instead of 'set') RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G 11 resolution/type errors detected in RefinementErrors.dfy