package batNavale;

/** Representation d'une case contenant un bateau, qui peut etre visee
 * au cours du jeu.
 * @author M . Nebut
 */

public class Case {

    /** la position de cette case */
    //@ public model Position saPosition;
    //@ private represents saPosition <- position;
    private final Position position; //@ in saPosition;

    /** Cette case a ete visee par un tir. */ 
    //@ public model boolean deja_touche;
    //@ private represents deja_touche <- estTouche;
    private boolean estTouche; //@ in deja_touche;

    //@public invariant saPosition != null;

    /** Construit une case qui n'a pas encore ete visee, dont la
     *	position est passee en parametre.
     *	@param p sa position
     */
    /*@ requires p != null;
      @ assignable \everything;
      @ ensures ! deja_touche;
      @ ensures saPosition == p;
      @*/
    public Case (Position p) {
	// COMPLETER
	this.position = null;
    }


    /** Cette case a-t-elle ete visee par un tir ?
     * @return true si cette case a ete visee par un tir 
     */
    /*@ ensures \result <==> this.deja_touche;
      @*/
    public /*@ pure @*/ boolean estTouchee() {
	// COMPLETER
	return false;
    }

    /** Indique que cette case a ete visee.
     */
    /*@ ensures this.deja_touche;
      @*/
    public void toucher() {
	// COMPLETER
    }
    
    /** Retourne la position de cette case.
     * @return la position de cette case.
     */
    /*@ ensures \result == this.saPosition;
      @*/
    public /*@ pure @*/ Position getPos() {
	// COMPLETER
	return null;
    }


}