// This program demonstrates an algorithm designed from its key loop // invariants. The algorithm finds the shortest route from a starting point // to all other points on a map (technically, it is Dijkstra's algorithm for // finding shortest paths in a graph). // History: // // February 2007 -- Created by Doug Baldwin as a prototype solution to a // CSci 240 exercise. public class LoopInvariants { // The algorithm for finding the shortest distances from a starting point // to all other points in a map. The map consists of points (e.g., street // intersections) and the distances between those points that are directly // connected (e.g., intersections with a segment of street between them). // This information is represented by a 2-dimensional array, A, of numbers, // where A[i][j] is the distance from point i to point j. If there is no // direct connection between points i and j, A[i][j] should be the constant // INFINITY. Note that this representation of maps assumes that points in the // map are identified by the integers 0, 1, 2, etc. It also implies that A is // square. The other parameter to this method is such an integer, indicating // the point at which the shortest distance computation is to start. The // method returns an array of distances from that starting point to all // points in the map. // // This algorithm classifies map points (aka "nodes") into 2 sets: those // nodes to which the shortest distance from the start node is known, and // those to which only a bound (possibly infinite) is known. The former nodes // are said to be "finalized," and their distances are said to be "final." // Distances to both kinds of nodes (minimal distances for finalized nodes, and // bounds on minimal distance for unfinalized ones) are recorded in a "distances" // array. The algorithm reduces the set of unfinalized nodes one by one, // maintaining the loop invariant that the entry in the distances array for // unfinalized node i is the minimal distance from the start node to node i *if // one visits only finalized nodes* between the start node and i (exclusive // of the start node and i). public static final double INFINITY = 1.0e100; static double[] findDistances( double[][] map, int start ) { final int n = map.length; // The number of nodes in the system double[] distances = new double[ n ]; boolean[] finalized = new boolean[ n ]; // finalized[i] = true iff distances[i] is final // Initialize the distances and finalized arrays. Initially no nodes are finalized, // and all distances are bounded by infinity, except for the distance from the start // node to itself, which is 0. for ( int i = 0; i < n; i++ ) { distances[i] = INFINITY; finalized[i] = false; } distances[start] = 0.0; // Now shrink the bounds in the distances array until all become final. To do this, // note that the loop invariant implies that at the start of each iteration of the // loop, the smallest supposedly unfinalized distance is actually final. This is // because any distance from the start node to the node with that smallest distance // (node m) would have to be from the start node via some (possibly 0) finalized nodes, // and then via at least one unfinalized one (otherwise the distance is along a path // that only goes via finalized nodes, and so is the distance already recorded in the // distances array, by the loop invariant). But getting from the start node to the first // unfinalized node on this hypothetical path involves a distance greater than the // distance from the start node to node m using only finalized nodes. Given this fact, // the node with the minimal distance can be moved to finalized node set. Then, in order // to maintain the loop invariant, distances to other unfinalized nodes have to be checked // and possibly updated, since the new finalized node may provide a shorter route to them // than was possible without that node. Since each iteration of this loop reduces the // number of unfinalized nodes by 1, and initially all nodes were unfinalized, the loop // has to repeat n times. for ( int i = 0; i < n; i++ ) { // Find the first unfinalized node. This loop has the invariant that at the start of // each iteration, nodes 0 through j-1 are known to be finalized. int j = 0; while ( j < n && finalized[j] ) { j = j + 1; } // Find the unfinalized node with minimal distance from the start. This loop is based // on the invariant that m is the index of the unfinalized node with the // the least distance in nodes 0 through j-1 at the start of each iteration of the loop. int m = j; j = j + 1; while ( j < n ) { if ( ! finalized[j] && distances[j] < distances[m] ) { m = j; } j = j + 1; } // Make the minimal-distance unfinalized node (node m) final. finalized[m] = true; // Update distance bounds for the remaining unfinalized nodes. This loop is based on // the invariant that at the beginning of each iteration, nodes 0 through k-1 have // distances conforming to the main loop invariant, given the new final node m. for ( int k = 0; k < n; k++ ) { if ( distances[m] + map[m][k] < distances[k] ) { distances[k] = distances[m] + map[m][k]; } } } // There are no unfinalized nodes left, so the distances array must contain only // final (i.e., shortest) distances. Return it. return distances; } // The main method simply demonstrates the others. public static void main (String args[]) { // Demonstrate shortest paths in a map. // An artificial "map" in which intersections form a single "street," with // intersections 1 unit apart: double[][] testMap = { { 0.0, 1.0, INFINITY, INFINITY, INFINITY }, { 1.0, 0.0, 1.0, INFINITY, INFINITY }, { INFINITY, 1.0, 0.0, 1.0, INFINITY }, { INFINITY, INFINITY, 1.0, 0.0, 1.0 }, { INFINITY, INFINITY, INFINITY, 1.0, 0.0 } }; // A map of part of the north edge of the Geneseo campus, based on MapQuest with // distances in feet, estimated by eyeball. Intersections are... // 0: The corner of Main St. and University Dr. // 1: The intersection of University Dr. and Wadsworth St. // 2: The intersection of University Dr. and Franklin St. // 3: The intersection of University Dr. and Court St. // 4: The intersection of Court St. and Franklin St. // 5: The intersection of Court St. and Wadsworth St. // 6: The intersection of Court St. and Main St. double[][] geneseoMap = { { 0.0, 450.0, INFINITY, INFINITY, INFINITY, INFINITY, 600.0 }, { 450.0, 0.0, 400.0, INFINITY, INFINITY, 800.0, INFINITY }, { INFINITY, 400.0, 0.0, 800.0, 700.0, INFINITY, INFINITY }, { INFINITY, INFINITY, 800.0, 0.0, 200.0, INFINITY, INFINITY }, { INFINITY, INFINITY, 700.0, 200.0, 0.0, 300.0, INFINITY }, { INFINITY, 800.0, INFINITY, INFINITY, 300.0, 0.0, 500.0 }, { 600.0, INFINITY, INFINITY, INFINITY, INFINITY, 500.0, 0.0 } }; double[] distances = findDistances( geneseoMap, 0 ); System.out.println( "Distances from point 0:" ); for ( int i = 0; i < distances.length; i++ ) { System.out.println( "\tto point " + i + ": " + distances[i] ); } } }