public class UnmannedCraft {
    private /*@ spec_public @*/ final int COLLIDING_DISTANCE = 10;

    private /*@ spec_public @*/ int x, y;

    private /*@ spec_public @*/ int speed;
    //@ public invariant speed >= 0;

    /*@ requires speed >= 0;
      @ ensures this.x == x;
      @ ensures this.y == y;
      @ ensures this.speed == speed; @*/
    public UnmannedCraft(int x, int y, int speed) {
        this.x = x;
        this.y = y;
        this.speed = speed;
    }

    /*@ ensures this.x == x;
      @ ensures this.y == y;
      @ ensures this.speed == 0; @*/
    public UnmannedCraft(int x, int y) {
        this(x, y, 0);
    }

    //@ ensures this.x == 0 && this.y == 0 && this.speed == 0;
    public UnmannedCraft() {
        this(0, 0, 0);
    }
    
    /*@ requires delta > 0;
      @ assignable speed;
      @ ensures speed == \old(speed) + delta; @*/
    public void accelerate(int delta) {
        this.speed += delta;
    }

    /*@ requires delta > 0; // && delta < speed;
      @ assignable speed;
      @ ensures speed == \old(speed) - delta; @*/
    public void decelerate(int delta) {
        this.speed -= delta;
    }

    //@ ensures \result == x;
    public /*@ pure @*/ int getX() {
        return x;
    }

    //@ ensures \result == y;
    public /*@ pure @*/ int getY() {
        return y;
    }

    //@ ensures \result == speed;
    public /*@ pure @*/ int getSpeed() {
        return speed;
    }
    
    //@ ensures \result == speed > 0;
    public boolean isMoving() {
        return speed > 0;
    }

    /*@ old int dx = this.x - x;
      @ old int dy = this.x - x;
      @ ensures \result == Math.sqrt(dx * dx + dy * dy); @*/
    public /*@ pure @*/ double distanceFrom(int x, int y) {
        int dx = this.x - x;
        int dy = this.y - y;
        dx = dx * dx;
        dy = dy * dy;
        return Math.sqrt(dx + dy);
    }

    //@ ensures \result == distanceFrom(other.x, other.y);
    public /*@ pure @*/ double distanceFrom(UnmannedCraft other) {
        return distanceFrom(other.x, other.y);
    }

    /*@ requires speed != 0;
      @ ensures \result == (int) (distanceFrom(x, y) / speed); @*/
    public /*@ pure @*/ int timeToReach(int x, int y) {
        return (int) (distanceFrom(x, y) / speed);
    }

    //@ ensures \result == distanceFrom(other) <= COLLIDING_DISTANCE;
    public /*@ pure @*/ boolean isColliding(UnmannedCraft other) {
        return distanceFrom(other) <= COLLIDING_DISTANCE;
    }
 }