Proving Programs Correct Using Plain Old Java Types什么鬼。。。表示orz，应该重新去看看TAPL ，然后看看ATAPL