Class Point

java.lang.Object
  Point

public class Point

extends java.lang.Object

Caractérisation de la notion usuelle de point en geometrie dans un espace en deux dimensions. C'est a dire un objet caracterise par une abcisse et une ordonnee.

Version:

18 février 2002, 11 mars 2004

Author:

Marc Champesme

Class Specifications

Specifications inherited from class Object

represents objectState <- JMLDataGroup.IT;

Model Field Summary

 

Model fields inherited from class java.lang.Object

objectState

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

Point()           Initialise un point de coordonees (0, 0)

Point(int xy)           Initialise un point dont l'abcisse et l'odonnee sont identiques et egales a la valeur donnee en parametre

Point(int x, int y)           Initialise un point dont l'abcisse et l'odonnee sont donnees en parametre.

Point(Point unPoint)           Clonage d'un point.

 

Method Summary
double	distanceA(Point autrePoint)           Calcule la distance du point courant au point passé en argument.
boolean	equals(java.lang.Object obj)           Test d'égalité
int	getX()           Renvoie l'abcisse du point
int	getY()           Renvoie l'ordonnee du point
boolean	isOrigine()           Teste si le point courant est l'origine du repère.
Point	symetrie()           Cree un nouveau point symetrique du point courant par rapport a l'axe des ordonnees
java.lang.String	toString()           Description of the Method
Point	translater(int deltaX, int deltaY)           Cree un nouveau point par translation de deltaX selon l'axe des abcisses et de deltaY selon l'axe des ordonnées.

 

Methods inherited from class java.lang.Object

clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Constructor Detail

Point

public Point()

Initialise un point de coordonees (0, 0)

Specifications:

ensures this.isOrigine();

Point

public Point(int xy)

Initialise un point dont l'abcisse et l'odonnee sont identiques et egales a la valeur donnee en parametre

Parameters:

xy - La valeur de l'abcisse et de l'ordonnee du nouveau point

Specifications:

ensures (this.getX() == xy)&&(this.getY() == xy);

Point

public Point(int x,
             int y)

Initialise un point dont l'abcisse et l'odonnee sont donnees en parametre.

Parameters:

x - Description of Parameter

y - Description of Parameter

Specifications:

ensures (this.getX() == x)&&(this.getY() == y);

Point

public Point(Point unPoint)

Clonage d'un point.

Parameters:

unPoint - le point a cloner

Specifications:

requires unPoint != null;
ensures this.equals(unPoint);

equals

public boolean equals(java.lang.Object obj)

Test d'égalité

Overrides:

equals in class java.lang.Object

Parameters:

obj - Description of the Parameter

Returns:

true si les deux points ont les memes coordonnées false sinon

Specifications: pure

     also

ensures ((obj == null)||!(\typeof(obj) == \type(Point))) ==> (\result == false);
ensures ((obj != null)&&(\typeof(obj) == \type(Point))) ==> \result == (this.getX() == ((Point)obj).getX())&&(this.getY() == ((Point)obj).getY());

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires obj != null&&\typeof(this) == \type(Object);
ensures \result <==> this == obj;

     also

ensures obj == null ==> !\result ;

getX

public int getX()

Renvoie l'abcisse du point

Returns:

L'abcisse du point

Specifications: pure

getY

public int getY()

Renvoie l'ordonnee du point

Returns:

L'ordonnee du point

Specifications: pure

symetrie

public Point symetrie()

Cree un nouveau point symetrique du point courant par rapport a l'axe des ordonnees

Returns:

Un point symetrique

Specifications: pure

ensures \fresh(\result );
ensures \result .getX() == -this.getX();
ensures \result .getY() == this.getY();

translater

public Point translater(int deltaX,
                        int deltaY)

Cree un nouveau point par translation de deltaX selon l'axe des abcisses et de deltaY selon l'axe des ordonnées.

Parameters:

deltaX - valeur a ajouter a l'abcisse

deltaY - valeur a ajouter a l'ordonnées

Returns:

Description of the Return Value

Specifications: pure

ensures \fresh(\result );
ensures \result .getX() == this.getX()+deltaX;
ensures \result .getY() == this.getY()+deltaY;

isOrigine

public boolean isOrigine()

Teste si le point courant est l'origine du repère.

Returns:

Vrai si le point est l'origine du repère, faux sinon.

Specifications: pure

ensures \result == ((this.getX() == 0)&&(this.getY() == 0));

distanceA

public double distanceA(Point autrePoint)

Calcule la distance du point courant au point passé en argument.

Parameters:

autrePoint - Point dont on souhaite connaitre la distance du point courant

Returns:

Distance du point courant au point autrePoint

Specifications: pure

requires autrePoint != null;

toString

public java.lang.String toString()

Description of the Method

Overrides:

toString in class java.lang.Object

Returns:

Description of the Return Value

Specifications: pure

     also

ensures \result != null;

Specifications inherited from overridden method in class Object:

public normal_behavior
assignable objectState;
ensures \result != null&&(* \result is a string representation of this object *);

     also

public normal_behavior
requires \typeof(this) == \type(Object);
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public model_program { ... }

    implies_that

ensures \result != null;