class Polynom {
    int a[];
    
    Polynom(int n) 
    /*@polynom_pre@*/
    {
	a = new int[n];
    }
    /*@polynom_post@*/
    
    int getCoeff(int index) 
    /*@getCoeff_pre@*/
    {
	return a[index];
    }
    /*@getCoeff_post@*/
    
    void setCoeff(int index, int value) 
    /*@setCoeff_pre@*/
    {
	a[index] = value;
    }
    /*@setCoeff_post@*/

    int evaluate(int x)
    /*@evaluate_pre@*/
    {
	int y = 0;
	int xexp = 1;
	for(int i = 0; i < a.length; i++) {
	    y += a[i] * xexp;
	    xexp *= x;
	}
	return y;
    }
    /*@evaluate_post@*/

    Polynom derive() 
    /*@derive_pre@*/
    {
	int dim = a.length - 1;
	Polynom d = new Polynom(dim);
	for(int i = 1; i <= dim; i++)
	    d.a[i-1] = i * a[i];
	return d;
    }
    /*@derive_post@*/

    Polynom add(Polynom p) 
    /*@add_pre@*/
    {
	int dimself = a.length;
	int dimp = p.a.length;
	int dimmax = dimself > dimp ? dimself : dimp;
	Polynom s = new Polynom(dimmax);
	for(int i = 0; i < dimself; i++)
	    s.a[i] = a[i];
	for(int i = 0; i < dimp; i++)
	    s.a[i] += p.a[i];
	return s;
    }
    /*@add_post@*/

    Polynom multiply(Polynom p) 
    /*@multiply_pre@*/
    {
	int dim = a.length;
	int dimp = p.a.length;
	Polynom m = new Polynom(dim + dimp - 1);
	for(int i = 0; i < dimp; i++) 
//	for(int i = 0; i < dim; i++) 
	    for(int j = 0; j < dimp; j++)
		m.a[i+j] += a[i] * p.a[j];
	return m;
    }
    /*@multiply_post@*/

    int findZero(int x1, int x2) 
    /*@findZero_pre@*/
    {
	int valueA = evaluate(x1);
	int valueB = evaluate(x2);
	int solution = -1;
	if (valueA == 0) solution = x1;
	else if (valueB == 0) solution = x2;
	else if ((valueA > 0 && valueB < 0) ||
		 (valueA < 0 && valueB > 0)) {
	    int pos, neg;
	    if (valueA >= 0) {
		pos = x1;
		neg = x2;
	    }
	    else {
		pos = x2;
		neg = x1;
	    }

	    /*@findZero_l1@*/
	    while (pos != neg && (pos != (neg + 1)) && (neg != (pos + 1))) {
		int half = (pos + neg) / 2;
		int valueH = evaluate(half);
		if (valueH == 0) {
		    solution = half;
		    pos = half;
		    neg = half;
		}
		else {
		    if (valueH < 0) neg = half;
		    else pos = half;
		}
	    }
	}
	return solution;
    }
    /*@findZero_post@*/

    static void demo()
    /*@demo_pre@*/
    {
	Polynom p = new Polynom(4);
	p.setCoeff(0,1);
	p.setCoeff(1,9);
	p.setCoeff(2,-6);
	p.setCoeff(3,1);

	int values[] = new int[5];
	for(int i = 0; i < 5; i++)
	    values[i] = p.evaluate(i);

	Polynom d = p.derive();

	int maxX = d.findZero(0,2);
	int maxY;
	if (maxX != -1) maxY = p.evaluate(maxX);
	else maxY = -1;

	int minX = d.findZero(2,6);
	int minY;
	if (minX != -1) minY = p.evaluate(minX);
	else minY = -1;
    }
    /*@demo_post@*/

    static Polynom buildPoly() 
    /*@buildPoly_pre@*/
    {
	Polynom p0 = new Polynom(2);
	p0.setCoeff(0,-20);
	p0.setCoeff(1,1);

	Polynom p1 = new Polynom(3);
	p1.setCoeff(0,0);
	p1.setCoeff(1,-11);
	p1.setCoeff(2,1);
	Polynom p2 = new Polynom(1);
	p2.setCoeff(0,24);
	Polynom p3 = p1.add(p2);

	Polynom p = p3.multiply(p0);

	return p;
    }
    /*@buildPoly_post@*/

    static void demo2() 
    /*@demo2_pre@*/
    {
	Polynom p = new Polynom(4);
	p.a[0] = -480;
	p.a[1] = 244;
	p.a[2] = -31;
	p.a[3] = 1;

	int values[] = new int[5];
	for(int i = 0; i < 5; i++)
	    values[i] = p.evaluate(7*i);

	int x0 = p.findZero(0,5);
	int x1 = p.findZero(6,10);
	int x2 = p.findZero(11,30);
	int x3 = p.findZero(10,12);
    }
    /*@demo2_post@*/
}