a function is correct if, **given that its callees uphold their contracts**, it upholds its contract.