package esercizio6;

// versione 0: voglio provare cha lmeno l'arrya non è null
// non riesco a provare nulla senza invariante
//
public class ArrayInClass0 {	
	
	int array[];
	
	//@ ensures array != null;
	//@ diverges true;
	ArrayInClass0() {
		array = new int[5];
		int i = 0;
		while (i < array.length) {
			array[i] = 0;
			i++;
		}
	}

}
