Class Position - SpartanRefactoring/Main GitHub Wiki

public final class Position implements Comparable<Position>, Serializable, Checkable { 
    /*
     * Forge (1)
     */
        Position(int line, int column); 
    /*
     * Type (11)
     */
        final int line; 
        final int column; 
        void invariant(); 
        String toString(); 
        boolean equals(Object o); 
        boolean equals(Position p); 
        int hashCode(); 
        int compareTo(Position p); 
        boolean before(Position p); 
        Position nextColumn(); 
        Position nextLine(); 
} 

// SSDLPedia
package il.ac.technion.cs.ssdl.parsing;

import static il.ac.technion.cs.ssdl.utils.DBC.nonnegative;
import il.ac.technion.cs.ssdl.stereotypes.Immutable;
import il.ac.technion.cs.ssdl.stereotypes.Instantiable;
import il.ac.technion.cs.ssdl.utils.DBC.Checkable;

import java.io.Serializable;

/**
 * An immutable class to model a position in a text file, including a column and
 * line number.
 * 
 * Author: Yossi Gil @since 13/06/2007
 */
@Immutable @Instantiable public final class Position implements Comparable<Position>, Serializable, Checkable {
    /**
     * The line of this position. First line is 0.
     */
    public final int line;
    /**
     * The column of this position. First column is 0.
     */
    public final int column;
    
    @Override public void invariant() {
        nonnegative(line);
        nonnegative(column);
    }
    
    @Override public String toString() {
        return "(" + line + ":" + column + ")";
    }
    
    /**
     * Create a new instance
     * 
     * line a non-negative integer specifying the line of this position
     * column non-negative integer specifying the column of this position
     */
    public Position(final int line, final int column) {
        this.line = line;
        this.column = column;
    }
    
    @Override public boolean equals(final Object o) {
        if (this == o)
            return true;
        if (o == null || getClass() != o.getClass())
            return false;
        return equals((Position) o);
    }
    
    /**
     * Determine whether two positions are the same
     * 
     * p a position to compare with
     * Return: true iff both positions are the same
     */
    public boolean equals(final Position p) {
        if (p == null)
            return false;
        return column == p.column && line == p.line;
    }
    
    @Override public int hashCode() {
        return line ^ column >>> 1;
    }
    
    @Override public int compareTo(final Position p) {
        return line != p.line ? line - p.line : column - p.column;
    }
    
    /**
     * Total Inspector: Determine whether one position occurs before another.
     * 
     * p a position to compare with
     * Return: true iff this position occurs prior to
     *         p
     */
    public boolean before(final Position p) {
        return compareTo(p) < 0;
    }
    
    /**
     * Compute the next position
     * 
     * Return: a new Position object, representing the next character
     *         position.
     */
    public Position nextColumn() {
        return new Position(line, column + 1);
    }
    
    /**
     * Compute the position of the next line
     * 
     * Return: a new Position object, representing the first character
     *         in the next line.
     */
    public Position nextLine() {
        return new Position(line + 1, 0);
    }
    
    private static final long serialVersionUID = -9094620074260625651L;
}