An algorithm and tool to infer practical postconditions
John L. Singleton, Gary T. Leavens, Hridesh Rajan, David R. Cok · 2018
Manually writing pre- and postconditions to document the behavior of a large library is a time-consuming task; what is needed is a way to automatically infer them. Conventional wisdom is that, if one has preconditions, then one can use the strongest postcondition predicate transformer (SP) to infer postconditions. However, we have performed a study using 2,300 methods in 7 popular Java libraries, and found that SP yields postconditions that are exponentially large, which makes them difficult to use, either by humans or by tools.