MATH.4:7 - Conformance Checklist

• Are the input constructors, supplied construction and parameter conditions stated?
• When different constructions represent one object, is any claimed function of that object independent of the construction or supported by a stated selection rule?
• Does each base case return an object satisfying the specification?
• Does every constructor clause use only supplied data and results justified for smaller inputs?
• When an auxiliary value or parameter is needed, do the strengthened specification, base and step agree?
• Are all case distinctions and witness-producing operations available for the claimed executable use?
• Do recursive calls descend through finite constituents, or is another termination argument supplied?
• Can the receiver obtain the witness and recover the property it uses?
• After a changed requirement, is the affected clause or missing construction identified?