// @(#)$Id: extra.txt,v 1.3 1997/02/13 00:20:47 leavens Exp $

Extra credit problems:

(a)
Write out the equivalent of your specification of Points,
using Figure 4.10 in Guttag and Horning as a guide.

(b)
Prove the implications in the trait.

(c)
The form you could use in the assertions was again limited
for this problem.  Another way to specify this example might be
as follows. Fill in the parts indicated by the dots (...)

	answer1: trait
	  includes Integer(int for Int)
	  Point tuple of x:int, y:int
	  introduces
	    origin: -> Point
	    __+__: Point, Point -> Point
	  asserts
	    \forall i,j: int, p1,p2: Point
	      origin.x == ...;
	      origin.y == ...;
	      p1 + p2 == ...;
	  implies
	    \forall p,p1,p2:Point
	      origin.x == 0;
	      origin.y == 0;
	      origin+p == p;
	      (p1+p2).x == p1.x + p2.x;
	      (p1+p2).y == p1.y + p2.y;


(d)
Could you use the two equations in the implications section
that describe + as the specification of +?

(f)
What other arithmetic or other operations would be good to specify
for Point?  Can you specify them?

(g)
Try specifying a sort Vector, of (x,y,z) coordinates,
as in physics.

(h)
Specify vector spaces.