// @(#)$Id: exercise.txt,v 1.1 1995/09/18 05:25:19 leavens Exp $

Be sure you have read section 4.8 of
``Larch: Languages and Tools for Formal Specification''
by John V. Guttag, James J. Horning, et al. (Springer-Verlag, 1993).

Fill in the following trait outline with a specification of
a sort Point, and some operations on Point values.
To simplify things, think of a Point as being used as
the cooprdinates on a computer screen, for example;
thus points can be modeled by their x and y coordinates, which are ints.
(That is, use Cartesian coordinates.)

	answer1: trait
	  includes Integer(int for Int)
	  Point tuple of ...
	  introduces
	    origin: -> Point
	    __+__: Point, Point -> Point
	  asserts
	    \forall i,j: int, p: Point
	      origin == ...;
	      [i,j] + p == ...;
	  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;

Your exercise is to fill in the missing part indicated by the dots (...) above.
Your answer should be consistent with the implications (following "implies").
Try using the LSL checker (it may be the command named lsl on your system)
to check your work for syntax and type problems.
To do this, put your LSL specification in a file answer1.lsl (in some other
directory, as you probably can't write into our answer file).
Then type (on Unix anyway)
	lsl answer1.lsl
to check the file.
If it just says ``Finished checking LSL traits'', then your work was fine.