Vague postconditions and proving correctness of algorithmsDebugging and testing with precise postconditions.