package batNavale;

/** Representation d'une position cartesienne generale.
 * @author M. Nebut
 * @version 05/05
 */
public class Position {

    /** position en abcisse */ 
    //@ public model int x; 
    //@ private represents x <- posx; 
    private int posx; //@ in x;

    /** position en ordonnee */
    //@ public model int y;  
    //@ private represents y <- posy; 
    private int posy; //@ in y;

    /** Construit une position. 
     * @param px son abscisse
     * @param py son ordonnee
     */
    /*@ assignable x,y;
      @ ensures this.x == px;
      @ ensures this.y == py;
      @*/
    public Position(int px, int py) {
	// COMPLETER
    }

    /** Retourne l'abscisse de cette position.
     * @return le champ x de cette position
     */
    /*@ ensures \result == this.x;
      @*/
    public /*@ pure @*/ int getX() {
	// COMPLETER
	return 0;
    }

    /** Retourne l'ordonnee de cette position.
     * @return le champ y de cette position
     */
    /*@ ensures \result == this.y;
      @*/
    public /*@ pure @*/ int getY() {
	// COMPLETER
	return 0;
    }

    /** Compare la position p a cette position.
     * @param p la position a comparer a cette position 
     * @return vrai si p a les memes coordonnees que cette position
     */
    /*@ also
      @ ensures (o == null || ! (o instanceof Position)) ==> ! \result;
      @ ensures o == this ==> \result;
      @ ensures (o != null && o != this && o instanceof Position) 
      @   ==> (\result <==> 
      @               ((Position)o).x == this.x &&  
      @               ((Position)o).y == this.y);
      @*/
    public /*@ pure @*/ boolean equals(/*@ nullable @*/ Object o) {
	// COMPLETER
	return false;
    }

    /** Retourne la distance entre la position passee en parametre et
     * cette position.   
     * @param p la position dont on veut la distance 
     * @return la distance entre p et cette position
     */
    /*@ requires p != null;
      @*/
    public /*@ pure @*/ double distance(Position p) {
	return Math.sqrt(Math.pow(this.getX()-p.getX(),2) +
			 Math.pow(this.getY()-p.getY(),2));
    }


    /** Retourne une valeur de hachage pour cette position.
     * @return une valeur de hachage pour cette position.
     */
    /*@ also
      @ ensures \result == (this.x + this.y);
      @*/
    public int hashCode() {
	// COMPLETER
	return 0;
    }

    public /*@ pure @*/ String toString() {
	return "(" + getX() + "," + getY() + ")";
    }
}