Further, in your examples with old and new functions - they don't have any postconditions, because you don't state any. For example, in Dafny, you have to be explicit about them, and you may want to omit certain pre/postconditions (to not overload the spec, or simply because they are implementation details). If the spec for old said !out.contains_keys('c'), and the spec for new removed this clause, then it would have a weaker postcondition. Likewise, if old didn't mention it and new guaranteed the presence of 'c' in keys, then new would have stronger postconditions. You really must be explicit about what you promise, not just what you return. Though, if you want to guarantee that both functions return the same value for all inputs, that can often be done as well.
Further, in your examples with
oldandnewfunctions - they don't have any postconditions, because you don't state any. For example, in Dafny, you have to be explicit about them, and you may want to omit certain pre/postconditions (to not overload the spec, or simply because they are implementation details). If the spec foroldsaid!out.contains_keys('c'), and the spec fornewremoved this clause, then it would have a weaker postcondition. Likewise, ifolddidn't mention it andnewguaranteed the presence of'c'in keys, thennewwould have stronger postconditions. You really must be explicit about what you promise, not just what you return. Though, if you want to guarantee that both functions return the same value for all inputs, that can often be done as well.