class Point {
    int x;
    int y;

    Point(int p, int q) 
    /*@Point_pre@*/
    {
	x = p;
	y = q;
    }
    /*@Point_post@*/

    Point difference(Point p) 
    /*@difference_pre@*/
    {
	Point result = new Point(x - p.x, y - p.y);
	return result;
    }
    /*@difference_post@*/

    int counterClockwise(Point p1, Point p2) 
    /*@counterClockwise_pre@*/
    {
	Point d1 = p1.difference(this);
	Point d2 = p2.difference(this);
	int result = 0;
	int s = d1.x * d2.y;
	int t = d1.y * d2.x;
	if (s > t) result = +1;
	else if (s < t) result = -1;
	else if ((d1.x * d2.x < 0) || (d1.y * d2.y < 0)) result = -1;
	else {
	    int l1 = d1.x * d1.x + d1.y * d1.y;
	    int l2 = d2.x * d2.x + d2.y * d2.y;
	    if (l1 < l2) result = +1;
	}
	return result;
    }
    /*@counterClockwise_post@*/
}

class Line {
    Point a;
    Point b;

    Line(Point p, Point q) 
    /*@Line_pre@*/
    {
	a = p;
	b = q;
    }
    /*@Line_post@*/

    boolean intersects(Line l) 
    /*@intersects_pre@*/
    {
	int ccw1 = a.counterClockwise(b, l.a);
	int ccw2 = a.counterClockwise(b, l.b);
	int t1 =  ccw1 * ccw2;
	int ccw3 = l.a.counterClockwise(l.b, a);
	int ccw4 = l.a.counterClockwise(l.b, b);
	int t2 =  ccw3 * ccw4;
	boolean result = (t1 <= 0) && (t2 <= 0);
	return result;
    }
    /*@intersects_post@*/

    boolean onLine(Point p) 
    /*@onLine_pre@*/
    {
	Point d1 = p.difference(a);
	Point d2 = b.difference(a);
	boolean colinear = d1.y * d2.x == d1.x * d2.y;
	int l1 = d1.x * d1.x + d1.y * d1.y;
	int l2 = d2.x * d2.y + d2.x * d2.y;
//	int l2 = d2.x * d2.x + d2.y * d2.y;
	boolean result = colinear && (l1 <= l2);
	return result;
    }
    /*@onLine_post@*/

    static void demo() 
    /*@demo_pre@*/
    {
	Line l1 = new Line(new Point(2,1), new Point(5,3));
	Line l2 = new Line(new Point(0,5), new Point(5,0));
	boolean i12a = l1.intersects(l2);
	boolean i12b = l2.intersects(l1);

	Line l3 = new Line(new Point(1,1), new Point(-10,-8));
	Line l4 = new Line(new Point(-5,0), new Point(0,5));
	boolean i34a = l3.intersects(l4);
	boolean i34b = l4.intersects(l3);

	Line l5 = new Line(new Point(1,1), new Point(2,2));
	Line l6 = new Line(new Point(3,3), new Point(5,5));
	boolean i56a = l5.intersects(l6);
	boolean i56b = l6.intersects(l5);

	Line l7 = new Line(new Point(1,1), new Point(4,4));
	Line l8 = new Line(new Point(3,3), new Point(5,5));
	boolean i78a = l7.intersects(l8);
	boolean i78b = l8.intersects(l7);
    }
    /*@demo_post@*/
}

class Polygon {
    Point[] ps;
    int index;

    Polygon() 
    /*@Polygon_pre@*/
    {
	ps = new Point[10];
	index = 0;
    }
    /*@Polygon_post@*/

    void addPoint(Point p) 
    /*@addPoint_pre@*/
    {
	ps[index++] = p;
    }
    /*@addPoint_post@*/

    boolean contains(Point p, int max) 
    /*@contains_pre@*/
    {
	/* assumption: ps[0] has lowest x-coord. within points with lowest y-coord. */
	/* all points must be to the left of x=max */
	Line testLine = new Line(p, new Point(max, p.y));
	Line borderLine = new Line(null, null);
	ps[index] = ps[0];
	boolean inside = false;
	int j = 0;
	for(int i = 1; i < index; i++) {
	    if (!testLine.onLine(ps[i])) {
		borderLine.a = ps[i];
		borderLine.b = ps[j];
		j = i;
		if (testLine.intersects(borderLine))
		    inside = !inside;
	    }
	}
	return inside;
    }
    /*@contains_post@*/

    static void polyDemo() 
    /*@polyDemo_pre@*/
    {
	Polygon p = new Polygon();
	p.addPoint(new Point(1,1));
	p.addPoint(new Point(5,7));
	p.addPoint(new Point(-3,4));
	p.addPoint(new Point(0,2));
	Point t1 = new Point(2,3);
	boolean inside1 = p.contains(t1, 999);

	Point t2 = new Point(3,2);
	boolean inside2 = p.contains(t2, 999);

	Point t3 = new Point(2,1);
	boolean inside3 = p.contains(t3, 999);

	Polygon p2 = new Polygon();
	p2.addPoint(new Point(0,-3));
	p2.addPoint(new Point(0,1));
	p2.addPoint(new Point(1,5));
	p2.addPoint(new Point(2,0));
	p2.addPoint(new Point(3,5));
	p2.addPoint(new Point(4,0));

	boolean inside4 = p2.contains(t1, 999);
	boolean inside5 = p2.contains(t2, 999);
	boolean inside6 = p2.contains(t3, 999);
    }
    /*@polyDemo_post@*/
}