Design by Contract
Design by Contract makes responsibilities explicit: what must be true before a call, what is guaranteed after it, and what always stays true.Design by Contract 不是多写 if,而是把调用者和被调用者的责任写清楚:调用前必须满足什么,调用后保证什么,过程中一直保持什么。
Precondition
Must be true before the call调用前必须成立
setMark(mark) may require 0 <= mark <= 100.比如 setMark(mark) 要求 0 <= mark <= 100。
Postcondition
Guaranteed after the call调用后保证成立
If the input is valid, getGrade(mark) guarantees a correct grade.输入合法时,getGrade(mark) 保证返回正确 grade。
Invariant
A rule that always remains true对象一直保持的规则
A circle radius should always be positive.Circle 的 radius 永远必须大于 0。
Write the contract next to the code把 contract 写成代码旁边的规则
// precondition: 0 <= mark <= 100
// postcondition: returns a valid grade
String gradeFor(int mark) {
if (mark < 50) return "FL";
if (mark < 65) return "PS";
if (mark < 75) return "CR";
if (mark < 85) return "DN";
return "HD";
}