class Point extends Matrix {
    Point(int x, int y) {
	super(2,1);
	a[0][0] = x;
	a[1][0] = y;
    }

    Point transform(Matrix m) {
	Matrix result = m.multiply(this);
	return new Point(result.a[0][0],result.a[1][0]);
    }
}

class Matrix {
    int a[][];
    int cols, rows;
    
    Matrix(int r, int c) 
    /*@matrix_pre@*/
    {
	rows = r;
	cols = c;
	a = new int[r][c];
    }
    /*@matrix_post@*/

    Matrix multiply(Matrix m) 
    /*@multiply_pre@*/
    {
	int q = m.cols;
	Matrix p = new Matrix(rows,q);
	int n = cols;
	for (int r = 0; r < rows; r++)
	    for (int c = 0; c < q; c++)
		for (int k = 0; k < n; k++)
		    p.a[r][c] += a[r][k]*m.a[k][c];
	return p;
    }
    /*@multiply_post@*/

    void scale(int scalar) 
    /*@scale_pre@*/
    {
	for (int r = 0; r < rows; r++)
	    for (int c = 0; c < cols; c++)
		a[r][c] *= scalar;
    }
    /*@scale_post@*/

    void add(Matrix m) 
    /*@add_pre@*/
    {
	for (int r = 0; r < rows; r++)
	    for (int c = 0; c < cols; c++)
		a[r][c] += m.a[r][c];
    }
    /*@add_post@*/

    Matrix transpose() 
    /*@transpose_pre@*/
    {
	Matrix t = new Matrix(cols, rows);
	for(int r = 0; r < cols; r++)
	    for(int c = 0; c < rows; c++) 
		t.a[r][c] = a[c][r];
	return t;
    }
    /*@transpose_post@*/

    int findPivot(int start) 
    /*@findPivot_pre@*/
    {
	int max = start;
	for (int r = start + 1; r < rows; r++) {
	    int e = a[r][start];
	    e = e >= 0 ? e : -e;
	    int m = a[max][start];
	    m = m >= 0 ? m : -m;
	    if (e > m) max = r;
	}
	return max;
    }
    /*@findPivot_post@*/

    void swapRows(int r1, int r2) 
    /*@swapRows_pre@*/
    {
	if (r1 == r2)
//	if (r1 != r2)
	    for (int c = 0; c < cols; c++) {
		int t = a[r1][c];
		a[r1][c] = a[r2][c];
		a[r2][c] = t;
	    }
    }
    /*@swapRows_post@*/
    
    void eliminate() 
    /*@eliminate_pre@*/
    {
	for (int r = 0; r < rows; r++) {
	    int p = findPivot(r);
	    swapRows(p,r);
	    int pivot = a[r][r];

	    for(int i = r + 1; i < rows; i++) {
		int factor = a[i][r]; // to avoid division by pivot
		                      // multiply with pivot
		for(int c = r; c < cols; c++) 
		    a[i][c] = pivot * a[i][c] - a[r][c] * factor;
	    }
	}
    }
    /*@eliminate_post@*/

    void substitute() 
    /*@substitute_pre@*/
    {
	for (int r = rows - 1; r > 0; r--) {
	    int pivot = a[r][r];

	    for(int i = r - 1; i >= 0; i--) {
		int factor = a[i][r];       // to avoid division by pivot
		for(int c = i; c < r; c++)  // multiply row with pivot
		    a[i][c] *= pivot; 
		a[i][r] = 0;
		int c = cols - 1;
		a[i][c] = pivot * a[i][c] - a[r][c] * factor;
	    }
	} 
    }
    /*@substitute_post@*/

    void simplify() 
    /*@simplify_pre@*/
    {
	for(int r = 0; r < rows; r++) {
	    int d = gcd(a[r][r],a[r][cols-1]);
	    a[r][r] /= d;
	    a[r][cols-1] /= d;
	}
    }
    /*@simplify_post@*/
    
    static int gcd(int a, int b) 
    /*@gcd_pre@*/
    {
	while (b != 0) {
	    int t = a % b;
	    a = b;
	    b = t;
	}
	return a;
    }
    /*@gcd_post@*/

    static Matrix demo() 
    /*@demo_pre@*/
    {
	Matrix m = new Matrix(3,4);
	m.a[0][0] = 1;
	m.a[0][1] = 3;
	m.a[0][2] = -4;
	m.a[0][3] = 8;

	m.a[1][0] = 1;
	m.a[1][1] = 1;
	m.a[1][2] = -2;
	m.a[1][3] = 2;

	m.a[2][0] = -1;
	m.a[2][1] = -2;
	m.a[2][2] = 5 ;
	m.a[2][3] = -1;
	/*@demo_init@*/

	m.eliminate();
	/*@demo_eliminate@*/
	/* 1  3 -4  8
           0 -2  2 -6
           0  0 -4 -8 */

	m.substitute();
	/*@demo_substitute@*/
	/* -32 0  0 -32
             0 8  0  40
             0 0 -4  -8 */

	m.simplify();
        /* 1 0 0 1
           0 1 0 5
           0 0 1 2 */

	return m;
    }
    /*@demo_post@*/


    static void geomTransform() 
    /*@geomTransform_pre@*/
    {
	Point a = new Point(-1,0);
	Point b = new Point(1,0);
	Point c = new Point(0,1);
	a.scale(3);
	b.scale(3);
	c.scale(3);
	Point trans = new Point(5,5);
	a.add(trans);
	b.add(trans);
	c.add(trans);
	Matrix rot = new Matrix(2,2);
	rot.a[0][0] = 0; //cos90
	rot.a[0][1] = -1; //-sin90
	rot.a[1][0] = 1; //sin90
	rot.a[1][1] = 0; //cos90
	Point a1 = a.transform(rot);
	Point b1 = b.transform(rot);
	Point c1 = c.transform(rot);
    }
    /*@geomTransform_post@*/
}