Fix typos.

Author: waywardmonkeys

src/kodkod/ast/Decl.java

@@ -80,7 +80,7 @@ public final class Decl extends Decls {
 
     /**
      * Returns the expression in this declaration.
-     * @return this.exresssion
+     * @return this.expresssion
      */
     public Expression expression() { return expression;  }
 

src/kodkod/ast/LeafExpression.java

@@ -24,7 +24,7 @@
 /** 
  * An expression with no children.  
  * {@link kodkod.ast.Relation Relation} and {@link kodkod.ast.Variable Variable} 
- * are examples of leaf exressions.  Two leaf expressions are equal 
+ * are examples of leaf expressions.  Two leaf expressions are equal
  * if and only if they refer to the same object.  That is, 
  * leaf1.eauls(leaf2) <=> leaf1 == leaf2.  A leaf has a name, which is 
  * basically a comment for the purpose of printing, viewing, etc.  The name 

src/kodkod/engine/Evaluator.java

@@ -43,7 +43,7 @@
  * that an Instance i is a solution to a formula f found using options o.
  * If you create an evaluator e such that e.instance = i, but e.options
  * is an Options object with different integer settings than o, 
- * e.evalate(f) may return false. </p>
+ * e.evaluate(f) may return false. </p>
  * 
  * @specfield options: Options
  * @specfield instance: Instance
@@ -103,7 +103,7 @@ public boolean evaluate(Formula formula){
 	}
 
 	/**
-	 * Evaluates the specified expession with respect to the relation-tuple mappings 
+	 * Evaluates the specified expression with respect to the relation-tuple mappings
 	 * given by this.instance and using this.options.
 	 * @return  {@link kodkod.instance.TupleSet set} of tuples to which the expression evaluates given the
 	 * mappings in this.instance and the options in this.options.
@@ -118,7 +118,7 @@ public TupleSet evaluate(Expression expression){
 	}
 
 	/**
-	 * Evaluates the specified int expession with respect to the relation-tuple mappings 
+	 * Evaluates the specified int expression with respect to the relation-tuple mappings
 	 * given by this.instance and using this.options.
 	 * @return  the integer to which the expression evaluates given the
 	 * mappings in this.instance and the options in this.options.

src/kodkod/engine/fol2sat/FOL2BoolTranslator.java

@@ -136,8 +136,8 @@ BooleanValue cache(Formula formula, BooleanValue translation) {
 	/**
 	 * Translates the given annotated expression into a boolean
 	 * matrix that is a least sound upper bound on the expression's
-	 * value, given the leaf and variable bindings in the 
-	 * the provided interpreter and environment.
+	 * value, given the leaf and variable bindings in the
+	 * provided interpreter and environment.
 	 * @requires interpreter.relations = AnnotatedNode.relations(annotated)
 	 * @return a boolean matrix that is a least sound upper bound on the expression's value
 	 * @throws HigherOrderDeclException  annotated.node contains a higher order declaration
@@ -419,7 +419,7 @@ public final BooleanMatrix visit(UnaryExpression unaryExpr) {
 	 * @param decls the declarations comprehension
 	 * @param param formula the body of the comprehension
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE initially
 	 * @param partialIndex partial index into the provided matrix; should be 0 initially
 	 * @param matrix boolean matrix that will retain the final results; should be an empty matrix of dimensions universe.size^decls.length initially
 	 * @ensures the given matrix contains the translation of the comprehension "{ decls | formula }"
@@ -520,7 +520,7 @@ public final BooleanValue visit(ConstantFormula constant) {
 	 * @param decls formula declarations
 	 * @param formula the formula body
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.FALSE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.FALSE initially
 	 * @param acc the accumulator that contains the top level conjunction; should be an empty AND accumulator initially
 	 * @ensures the given accumulator contains the translation of the formula "all decls | formula"
 	 */
@@ -556,7 +556,7 @@ private void all(Decls decls, Formula formula, int currentDecl, BooleanValue dec
 	 * @param decls formula declarations
 	 * @param formula the formula body
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE initially
 	 * @param acc the accumulator that contains the top level conjunction; should be an empty OR accumulator initially
 	 * @ensures the given accumulator contains the translation of the formula "some decls | formula"
 	 */
@@ -953,7 +953,7 @@ public final Int visit(UnaryIntExpression intExpr) {
 	 * @param decls intexpr declarations
 	 * @param formula the formula body
 	 * @param currentDecl currently processed declaration; should be 0 initially
-	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
+	 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE initially
 	 * @param values integer values computed so far
 	 */
 	private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,

src/kodkod/engine/fol2sat/Skolemizer.java

@@ -78,7 +78,7 @@ abstract class Skolemizer extends AbstractReplacer {
 	 * Skolemizes the given annotated formula using the given bounds and options.  If 
 	 * Options.trackFormulas is set and the formula is skolemizable, the resulting annotated
 	 * formula will contain transitive source information for each of its subformulas. 
-	 * Specifically, let f be the returned annotated formula, t be a descendeant of f.node, and
+	 * Specifically, let f be the returned annotated formula, t be a descendant of f.node, and
 	 * s a descendant of annotated.node from which t was derived.  Then, 
 	 * f.source[t] = annotated.source[s].  If options.trackFormulas is false, no source 
 	 * information will be recorded (i.e. f.source[t] = t for all descendants t of f).
@@ -157,7 +157,7 @@ private Skolemizer(AnnotatedNode<Formula> annotated, Bounds bounds, Options opti
 		super(annotated.sharedNodes());
 
 		// only cache intermediate computations for expressions with no free variables
-		// and formulas with no free variables and no quantified descendents
+		// and formulas with no free variables and no quantified descendants
 
 		for(Node n: annotated.sharedNodes()) {
 			final AbstractDetector fvdetect = annotated.freeVariableDetector();
@@ -274,7 +274,7 @@ public final  Decls visit(Decls decls) {
 	/** 
 	 * Returns the binding for the given variable in the current replacement environment.
 	 * @return the binding for the given variable in the current replacement environment.
-	 * @throws UnboundLeafException  variable not bound in teh replacement environment.
+	 * @throws UnboundLeafException  variable not bound in the replacement environment.
 	 */
 	@Override
 	public final Expression visit(Variable variable) { 

src/kodkod/engine/fol2sat/SymmetryBreaker.java

@@ -259,7 +259,7 @@ private static final BooleanValue leq(BooleanFactory f, List<BooleanValue> l0, L
 	/**
 	 * Let t be the tuple represent by the given arity and tupleIndex.
 	 * This method returns the tuple index of the tuple t' such t'
-	 * is equal to t with each occurence of atomIndex0
+	 * is equal to t with each occurrence of atomIndex0
 	 * replaced by atomIndex1 and vice versa.
 	 * @return the index of the tuple to which the given symmetry
 	 * maps the tuple specified by arith and tupleIndex
@@ -318,7 +318,7 @@ public int compare(RelationPredicate o1, RelationPredicate o2) {
 	 * this.bounds.upperBound[acyclic.relation] is the cross product of some partition in this.symmetries with
 	 * itself. Assuming that this is the case, we then break symmetry on acyclic.relation using one of the methods
 	 * described in {@linkplain #breakMatrixSymmetries(Map, boolean)}; the method used depends
-	 * on the value of the "agressive" flag.
+	 * on the value of the "aggressive" flag.
 	 * The partition that formed the upper bound of acylic.relation is removed from this.symmetries.</p>
 	 * 
 	 * @return null if symmetry cannot be broken on acyclic; otherwise returns a formula
@@ -370,13 +370,13 @@ private final Formula breakAcyclic(RelationPredicate.Acyclic acyclic, boolean ag
 	 * cross-multiplied with itself gives the upper bound of total.relation. Assuming that this is the case, 
 	 * we then break symmetry on total.relation, total.first, total.last, and total.ordered using one of the methods
 	 * described in {@linkplain #breakMatrixSymmetries(Map, boolean)}; the method used depends
-	 * on the value of the "agressive" flag.
+	 * on the value of the "aggressive" flag.
 	 * The partition that formed the upper bound of total.ordered is removed from this.symmetries.</p>
 	 * 
 	 * @return null if symmetry cannot be broken on total; otherwise returns a formula
 	 * f such that the meaning of total with respect to this.bounds is equivalent to the
 	 * meaning of f with respect to this.bounds' 
-	 * @ensures this.symmetries and this.bounds are modified as desribed in {@linkplain #breakMatrixSymmetries(Map, boolean)} 
+	 * @ensures this.symmetries and this.bounds are modified as described in {@linkplain #breakMatrixSymmetries(Map, boolean)}
 	 * iff total.first, total.last, and total.ordered have the same upper bound, which, when 
 	 * cross-multiplied with itself gives the upper bound of total.relation
 	 * 

src/kodkod/engine/fol2sat/SymmetryDetector.java

@@ -247,7 +247,7 @@ private void refinePartitions(IntSet set) {
 	 * Returns an IntSet that can store elements
 	 * in the range [0..size), and that holds
 	 * the given number.
-	 * @requries 0 <= num < size
+	 * @requires 0 <= num < size
 	 * @return {s: IntSet | s.ints = num } 
 	 */
 	private static final IntSet oneOf(int size, int num) {

src/kodkod/engine/fol2sat/Translator.java

@@ -104,7 +104,7 @@ public static BooleanMatrix evaluate(Expression expression,Instance instance, Op
 	}
 
 	/**
-	 * Evalutes the given intexpression to an {@link kodkod.engine.bool.Int} using the provided instance and options. 
+	 * Evaluates the given intexpression to an {@link kodkod.engine.bool.Int} using the provided instance and options.
 	 * @return an {@link kodkod.engine.bool.Int} representing the value of the intExpr with respect
 	 * to the specified instance and options.
 	 * @throws NullPointerException  formula = null || instance = null || options = null
@@ -215,7 +215,7 @@ private static Translation.Incremental translateIncrementalTrivial(Formula formu
 
 		// add new relation bindings to the translation bounds.  since the given bounds induce
 		// a coarser set of symmetries on the universe than transl.symmetries, adding their (disjoint) bindings to tBounds 
-		// will not change the symmetries of tBounds.  note that the ymmetries of tBounds refine transl.symmetries, and they 
+		// will not change the symmetries of tBounds.  note that the symmetries of tBounds refine transl.symmetries, and they
 		// may be strictly finer if some of the symmetries in transl.symmetries were broken via SymmetryBreaker.breakMatrixSymmetries(...) 
 		// during the generation of transl.  in particular, any symmetries absent from tBounds are precisely those that were broken based
 		// on the total ordering and acyclic predicates in transl.originalFormula.
@@ -481,7 +481,7 @@ public Formula visit(RelationPredicate pred) {
 	 * information for each of the subformulas of f.node.  Specifically, let t be a subformula of f.node, and
 	 * s be a descdendent of annotated.node from which t was derived.  Then, f.source[t] = annotated.source[s]. </p>
 	 * @requires simplified.keySet() in annotated.predicates()[RelationPredicate.NAME]
-	 * @requires no disj p, p': simplified.keySet() | simplified.get(p) = simplifed.get(p') // this must hold in order
+	 * @requires no disj p, p': simplified.keySet() | simplified.get(p) = simplified.get(p') // this must hold in order
 	 * to maintain the invariant that each subformula of the returned formula has exactly one source
 	 * @requires for each p in simplified.keySet(), the formulas "p and [[this.bounds]]" and
 	 * "simplified.get(p) and [[this.bounds]]" are equisatisfiable

src/kodkod/util/collections/Containers.java

@@ -56,7 +56,7 @@ public static final <T, E extends T> Iterator<T> iterate(final E... items) {
 	 * The iterator is backed by the given array.  The contents
 	 * of the array are not modified by the iterator.
 	 * The returned iterator enumerates the items located between
-	 * indeces start, inclusive, and end, exclusive.  If start < end,
+	 * indices start, inclusive, and end, exclusive.  If start < end,
 	 * the elements are returned in the ascending order; otherwise,
 	 * they are returned in the descending order.
 	 * @throws NullPointerException  items = null
@@ -189,7 +189,7 @@ public static final <T> T[] hashSort(T[] array) {
 	 * and reference equality. 
 	 * The array must be sorted into ascending order according to the identity hashcodes of its elements 
 	 * (as by {@link #identitySort(Object[])}) prior to making this call. If it is not sorted, 
-	 * the results are undefined.  If the array contains multiple occurences of the specified object, 
+	 * the results are undefined.  If the array contains multiple occurrences of the specified object,
 	 * there is no guarantee which one will be found.
 	 * @requires all i, j: [0..array.length) | i < j => array[i].hashCode() <= array[j].hashCode())
 	 * @return index of the search key, if it is contained in the array; otherwise, (-(insertion point) - 1). 
@@ -231,7 +231,7 @@ else if (midIndex > index)
 	 * and object equality. 
 	 * The array must be sorted into ascending order according to the hashcodes of its elements 
 	 * (as by {@link #hashSort(Object[])}) prior to making this call. If it is not sorted, 
-	 * the results are undefined.  If the array contains multiple occurences of the specified object, 
+	 * the results are undefined.  If the array contains multiple occurrences of the specified object,
 	 * there is no guarantee which one will be found.
 	 * @requires all i, j: [0..array.length) | i < j => System.identityHashCode(array[i]) <= System.identityHashCode(array[j])
 	 * @return index of the search key, if it is contained in the array; otherwise, (-(insertion point) - 1). 
@@ -334,7 +334,7 @@ private static abstract class ArrayIterator<T> implements Iterator<T> {
 		 * The iterator is backed by the given array.  The contents
 		 * of the array are not modified by the iterator.  The 
 		 * constructed iterator returns the items located between the 
-		 * indeces start, inclusive, and end, exclusive.
+		 * indices start, inclusive, and end, exclusive.
 		 * @requires items != null && 
 		 *           start < end => end in [0..items.length] && start in [0..end], 
 		 *                          start in [0..items.length) && end in [-1..start]

src/kodkod/util/nodes/AnnotatedNode.java

@@ -141,7 +141,7 @@ public final N node() {
 	}
 
 	/**
-	 * Returns the source of the the given descendant of this.node.
+	 * Returns the source of the given descendant of this.node.
 	 * @requires n in this.node.*components
 	 * @return this.source[n]
 	 */
@@ -215,10 +215,10 @@ public final Map<RelationPredicate.Name, Set<RelationPredicate>> predicates() {
 	}
 
 	/**
-	 * Returns a Detector that will return TRUE when applied to a descendent
-	 * of this.node iff the descendent contains a quantified formula.
-	 * @return a Detector that will return TRUE when applied to a descendent
-	 * of this.node iff the descendent contains a quantified formula.
+	 * Returns a Detector that will return TRUE when applied to a descendant
+	 * of this.node iff the descendant contains a quantified formula.
+	 * @return a Detector that will return TRUE when applied to a descendant
+	 * of this.node iff the descendant contains a quantified formula.
 	 */
 	public final AbstractDetector quantifiedFormulaDetector() {
 		return new AbstractDetector(sharedNodes) {
@@ -229,10 +229,10 @@ public Boolean visit(QuantifiedFormula quantFormula) {
 	}
 
 	/**
-	 * Returns a Detector that will return TRUE when applied to a descendent
-	 * of this.node iff the descendent contains a free variable.
-	 * @return a Detector that will return TRUE when applied to a descendent
-	 * of this.node iff the descendent contains a free variable.
+	 * Returns a Detector that will return TRUE when applied to a descendant
+	 * of this.node iff the descendant contains a free variable.
+	 * @return a Detector that will return TRUE when applied to a descendant
+	 * of this.node iff the descendant contains a free variable.
 	 */
 	public final AbstractDetector freeVariableDetector() {
 		return new FreeVariableDetector(sharedNodes);
@@ -254,7 +254,7 @@ public String toString() {
 	}
 
 	/**
-	 * Detects shared non-leaf descendents of a given node.
+	 * Detects shared non-leaf descendants of a given node.
 	 * 
 	 * @specfield node: Node // node to which the analyzer is applied
 	 */
@@ -383,7 +383,7 @@ private static final class PredicateCollector extends AbstractVoidVisitor {
 		 * if it is mapped to TRUE, it has been visited with negated=TRUE,
 		 * if it is mapped to null, it has been visited with both values of negated. */
 		private final Map<Node,Boolean> visited;	
-		/* holds the top level predicates at the the end of the visit*/
+		/* holds the top level predicates at the end of the visit*/
 		final EnumMap<RelationPredicate.Name, Set<RelationPredicate>> preds;
 		/**
 		 * Constructs a new collector.