/*
 * sum of the n first integers
 */
class Sum {

	/*@ requires (n == 10);
	  @ ensures s == 45;
	  @*/
	static int sum (int n) {
		int s = 1;
		int i = 0;
		while (i < n) {
			s = s + i;
			i = i + 1;			
		}
		return s;
	}


}
