package esercizio4;

public class Magazzino24 {

	private /*@ spec_public  @*/int[] product;

	// invariante, per ogni prodotto ho sempre un numero di pezzi tra 0 e 100
	//@ public invariant product != null && product.length == 5; 
	//@ public invariant (\forall int i; 0 <= i && i < 5 ;  0 <= product[i] & product[i] <= 500); 

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

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

	// precondizione: indice compreso tra 0 e 4 compresi
	// postcondizione:se il prodotto ha 100 elementi assicurati che è pieno
	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
	public boolean isFull() {
		int total = 0;
		//@ loop_invariant 0 <= total <= 500;
		for (int i = 0; i < 5; i++)
			total += product[i];
		return total == 500 ? true : false;
	}
}
