package esercizio4;

public class Magazzino {

	private /*@ spec_public */ int[] product;
	
	//invariante, per ogni prodotto ho sempre un numero di pezzi tra 0 e 100
	// public invariant (\forall int i; i >= 0 && i < 5; product[i]>=0 && product[i]<=100);

	//COSTRUTTORE
	//
	// devo assicurare che ogni prodotto sia inizializzato a 0
	//@ ensures product != null && product.length == 5 && (\forall int i; 0 <= i && i < product.length; product[i]==0);
	//@ diverges true;
	public Magazzino() {
		product = new int[5];
		int i = 0;
		//@ loop_invariant product!=null && product.length == 5  && (\forall int x; x >= 0 && x < i; product[i]==0);
		while(i < product.length) {
			product[i] = 0;
			i++;
		}
	}

	//esiste un prodotto con meno di 100 unità
	//@requires (\exists int i; i >= 0 && i < 5;  product[i]<100);	
	//@requires (product[productIndex]+addQuantity)<=100 && addQuantity<=10;		
	//postcondizione: le quantità diverse da product_index sono invariate
	//@ensures(\forall int i; i >= 0 && i <productIndex; product[i] == \old(product[i]) ); 
	//@ensures(\forall int i; i >productIndex && i <5; product[i] == \old(product[i]) );
	public boolean insert(int productIndex, int addQuantity) {
		if ((productIndex < 0 || productIndex > 4)
				|| (addQuantity < 0 || addQuantity > 10)
				|| (product[productIndex] + addQuantity) > 100) {
			return false;
		} else {
			product[productIndex] += addQuantity;
			return true;
		}
	}


	//precondizione: indice compreso tra 0 e 4 compresi
	//@requires productIndex<5 && productIndex>=0;		
	//postcondizione:se il prodotto ha 100 elementi assicurati che è pieno
	//@ensures product[productIndex]>=100 ==> \result== true;
	public boolean isFull(int productIndex) {
		if (productIndex < 0 || productIndex > 4)
			return false;
		else
			return product[productIndex] >= 100 ? true : false;
	}

	
	// postcondizione: se esiste un oggetto con quantità minore di 100 allora il metodo ritorna false
	//@ensures (\exists int i; i >= 0 && i < 5;  product[i]<100 ==> \result==false);
	public boolean isFull(){
		int total = 0;
		for (int i = 0; i < 5; i++)
			total += product[i];
		return total == 500 ? true : false;
	}
}
