假设现在有方法如下：
public int add(int a, int b){ return a+b； }
那么这个方法的
前置条件：调用者传入两个参数，两个参数都是int型
后置条件：调用者接收到一个int型返回值，值为a与b的和
不变量：a与b
ArrayList的add方法
这个方法的
前置条件：这个ArrayList对象还有剩余空间；add方法参数不为空，参数的类型正确；
后置条件：这个ArrayList对象的size增加1，在索引为size-1处多了一个刚才添加的对象
不变量：ArrayList声明时的总长度
原文：http://www.cnblogs.com/shuada/p/3554810.html