Section 1.1 says the fourth line of a contract, what is not promised, is a judgement about calls nobody has made. Section 1.6 says no test can check that line, because a test runs on values you choose and the line is a claim about values the procedure never sees. The field has partial machinery for closing the gap: types that rule out whole classes of input, assertions checked at run time, exhaustive generation when the input space is finite, and proof for the cases where a specification is written formally. None of it settles the general case, and every one of those tools still relies on a person choosing what to state.
Take a position on this question: can the fourth line of a contract ever be established by a machine rather than by an argument?
In your answer: state a criterion that would count as success; apply the criterion to a procedure you invent and describe in one paragraph; say where the criterion stops working or what it quietly assumes; and name the evidence that would change your position.
Rubric. Tick each criterion your answer meets, then save the self-assessment. The platform does not grade it.
Worked solution
There is no single correct answer, so this is a model of the shape a complete answer takes, not a key. A level-3 answer picks a procedure, writes its four lines, and then makes the boundary visible. For a converter from whole seconds to whole minutes, the first three lines are easy to state and to check on chosen values. The fourth line might read "nothing is promised for a count of seconds that is negative or above 86,400". A machine can enumerate every admitted input when the range is finite, and it can check the claim on all of them. What the machine cannot do by enumeration is justify the choice of 86,400 itself, and that choice is the fourth line. The answer should say whether "all 86,401 admitted values were checked" counts as establishing the line or only as establishing a larger second line. A strong answer then takes a side: either the line is established relative to a stated input space, in which case the machine checks the relative claim and the person supplies the space, or the line is never established and remains a judgement that no amount of running removes. Either side is acceptable when the criterion, the example and the cost are stated. The answer that scores 0 is the one that says testing is incomplete and stops there.