@-statements

This commit is contained in:
Leen Dereu
2018-03-11 20:53:05 +01:00
parent 23a6fcd4b9
commit 78f195cccc

View File

@@ -50,6 +50,7 @@ public class Worm {
* @post the new radius of the worm is equal to the given radius * @post the new radius of the worm is equal to the given radius
* |new.getRadius() == radius * |new.getRadius() == radius
*/ */
@Raw
public Worm(Tuple<Double, Double> location, double orientation, String name, double radius) { public Worm(Tuple<Double, Double> location, double orientation, String name, double radius) {
this(location, orientation, name, radius, 0.25); this(location, orientation, name, radius, 0.25);
@@ -91,6 +92,7 @@ public class Worm {
* the given name is not a valid name for a worm * the given name is not a valid name for a worm
* |isValidName(name) * |isValidName(name)
*/ */
@Raw
public Worm(Tuple<Double, Double> location, double orientation, String name, double radius, double minRadius) public Worm(Tuple<Double, Double> location, double orientation, String name, double radius, double minRadius)
throws IllegalArgumentException { throws IllegalArgumentException {
@@ -128,7 +130,7 @@ public class Worm {
* the location of the worm expresses the place of the worm * the location of the worm expresses the place of the worm
* in the play area * in the play area
*/ */
@Basic @Basic @Immutable @Raw
public Tuple<Double, Double> getLocation() { public Tuple<Double, Double> getLocation() {
return this.location; return this.location;
} }
@@ -163,6 +165,7 @@ public class Worm {
* the given location is not a valid location for a worm * the given location is not a valid location for a worm
* |! isValidLocation(location) * |! isValidLocation(location)
*/ */
@Raw
private void setLocation(Tuple<Double, Double> location) throws IllegalArgumentException { private void setLocation(Tuple<Double, Double> location) throws IllegalArgumentException {
if (!isValidLocation(location)) if (!isValidLocation(location))
@@ -183,7 +186,7 @@ public class Worm {
* the orientation of a worm expresses the direction in which * the orientation of a worm expresses the direction in which
* the worm is looking * the worm is looking
*/ */
@Basic @Basic @Raw
public double getOrientation() { public double getOrientation() {
return orientation; return orientation;
} }
@@ -203,6 +206,7 @@ public class Worm {
* @post the new orientation of the worm must be equal to the given orientation * @post the new orientation of the worm must be equal to the given orientation
* |new.getOrientation() == orientation * |new.getOrientation() == orientation
*/ */
@Raw
private void setOrientation(double orientation) { private void setOrientation(double orientation) {
assert isValidOrientation(orientation); assert isValidOrientation(orientation);
this.orientation = orientation; this.orientation = orientation;
@@ -231,7 +235,7 @@ public class Worm {
* the radius of the worm expresses half of the * the radius of the worm expresses half of the
* width of the worm * width of the worm
*/ */
@Basic @Basic @Raw
public double getRadius() { public double getRadius() {
return this.radius; return this.radius;
} }
@@ -259,6 +263,7 @@ public class Worm {
* the given radius is not a valid radius for any worm * the given radius is not a valid radius for any worm
* |! canHaveAsMinRadius(radius) * |! canHaveAsMinRadius(radius)
*/ */
@Raw
public void setRadius(double radius) throws IllegalArgumentException { public void setRadius(double radius) throws IllegalArgumentException {
if (!canHaveAsRadius(radius)) if (!canHaveAsRadius(radius))
throw new IllegalArgumentException("Invalid radius"); throw new IllegalArgumentException("Invalid radius");
@@ -272,6 +277,7 @@ public class Worm {
* the minimum radius of the worm expresses the minimum length * the minimum radius of the worm expresses the minimum length
* of half of the width of the worm * of half of the width of the worm
*/ */
@Basic @Raw
public double getMinRadius() { public double getMinRadius() {
return this.minRadius; return this.minRadius;
} }
@@ -298,6 +304,7 @@ public class Worm {
* (or equal) and the radius is a number * (or equal) and the radius is a number
* |result == (radius >= this.minRadius && !Double.isNaN(radius)) * |result == (radius >= this.minRadius && !Double.isNaN(radius))
*/ */
@Raw
private boolean canHaveAsRadius(double radius) { private boolean canHaveAsRadius(double radius) {
return !Double.isNaN(radius) && radius >= getMinRadius(); return !Double.isNaN(radius) && radius >= getMinRadius();
} }
@@ -306,7 +313,7 @@ public class Worm {
* Return the mass of the worm * Return the mass of the worm
* the mass of the worm expresses the weight of the worm * the mass of the worm expresses the weight of the worm
*/ */
@Basic @Basic @Raw
public double getMass() { public double getMass() {
return this.mass; return this.mass;
} }
@@ -325,6 +332,7 @@ public class Worm {
* rho * (4 / 3 * Math.PI * Math.pow(radius, 3)) * rho * (4 / 3 * Math.PI * Math.pow(radius, 3))
* |new.getMass() == rho * (4 / 3 * Math.PI * Math.pow(radius, 3)) * |new.getMass() == rho * (4 / 3 * Math.PI * Math.pow(radius, 3))
*/ */
@Raw
private void setMass(double radius) { private void setMass(double radius) {
final double rho = 1062.0; final double rho = 1062.0;
@@ -345,7 +353,7 @@ public class Worm {
* Return the current action points of the worm * Return the current action points of the worm
* the action points identifies the energy of the worm * the action points identifies the energy of the worm
*/ */
@Basic @Basic @Raw
public long getActionPoints() { public long getActionPoints() {
return this.actionPoints; return this.actionPoints;
} }
@@ -354,7 +362,7 @@ public class Worm {
* Return the maximum of action points of the worm * Return the maximum of action points of the worm
* the maximum action points identifies the maximum energy of the worm * the maximum action points identifies the maximum energy of the worm
*/ */
@Basic @Basic @Raw
public long getMaxActionPoints() { public long getMaxActionPoints() {
return this.maxActionPoints; return this.maxActionPoints;
} }
@@ -374,6 +382,7 @@ public class Worm {
* | actionPoints = 0; * | actionPoints = 0;
* |this.actionPoints = actionPoints; * |this.actionPoints = actionPoints;
*/ */
@Raw
private void setActionPoints(long actionPoints) { private void setActionPoints(long actionPoints) {
if (actionPoints > getMaxActionPoints()) if (actionPoints > getMaxActionPoints())
actionPoints = getMaxActionPoints(); actionPoints = getMaxActionPoints();
@@ -416,6 +425,7 @@ public class Worm {
* @post when the maximum points change, the current points should change too * @post when the maximum points change, the current points should change too
* |setActionPoints(getActionPoints) * |setActionPoints(getActionPoints)
*/ */
@Raw
private void setMaxActionPoints(double maxActionPoints) { private void setMaxActionPoints(double maxActionPoints) {
this.maxActionPoints = round(maxActionPoints); this.maxActionPoints = round(maxActionPoints);
setActionPoints(getActionPoints()); setActionPoints(getActionPoints());
@@ -460,7 +470,7 @@ public class Worm {
* Return the name of the worm * Return the name of the worm
* the name of the worm expresses the identity of the worm * the name of the worm expresses the identity of the worm
*/ */
@Basic @Basic @Immutable @Raw
public String getName() { public String getName() {
return this.name; return this.name;
} }
@@ -506,6 +516,7 @@ public class Worm {
* the given name is not a valid name for any worm * the given name is not a valid name for any worm
* |! isValidName(name) * |! isValidName(name)
*/ */
@Raw
public void setName(String name) throws IllegalNameException { public void setName(String name) throws IllegalNameException {
int validName = isValidName(name); int validName = isValidName(name);