The Constrained Shortest Path Problem: A Case Study in Using ASMs

Karl Stroetmann

(Siemens AG, 81730 Munich, Germany Karl.Stroetmann@mchp.siemens.de)

Abstract: This paper addresses the correctness problem of an algorithm solving the constrained shortest path problem. We define an abstract, nondeterministic form of the algorithm and prove its correctness from a few simple axioms. We then define a sequence of natural refinements which can be proved to be correct and lead from the abstract algorithm to an efficient implementation due to Ulrich Lauther [Lauther 1996] and based on [Desrosiers et al. 1995]. Along the way, we also show that the abstract algorithm can be regarded as a natural extension of Moore’s algorithm [Moore 1957] for solving the shortest path problem. Key Words: abstract state machine, software verification, shortest path problem, constrained shortest path problem Category: D.2.4, F.3.1, G.2.2

1 Introduction

The subject of this case study is an algorithm to solve the constrained shortest path problem. This problem is specified in Section 2. We develop an abstract generic algorithm for solving shortest path problems in Section 3, and prove its correctness from a few simple axioms in Section 4. This abstract algorithm is non–deterministic. This non-determinism is eliminated in Section 5, yielding a generic deterministic algorithm. In Section 6, this generic algorithm is instantiated in order to solve the constrained shortest path problem. To this end, we provide an implementation of certain operations on step functions. The resulting algorithm can readily be translated into an efficient C++ program.

The algorithms are presented as abstract state machines (ASM), a notion introduced by Gurevich under the name of evolving algebras [Gurevich 1993]. ASMs can be regarded as pseudo code. However, in contrast to pseudo code, ASMs have a rigorous semantics, formally defined in Gurevich [Gurevich 1995]. The notation used to present an ASM is mostly self explanatory. For the reader not familiar with [Gurevich 1995] we explain this notation and its semantics on an informal level.

The basic notion of an ASM is the notion of an update. It takes the form

f(t_{1}, ⋯, t_{n}) := s

where f is a function symbol and s, t_{1}, ⋯, t_{n} are expressions that can be evaluated. If the evaluation of these expressions produces the values v_{0}, v_{1}, ⋯, v_{n}, respectively, then the value of f(v_{1}, ⋯, v_{n}) is changed to v_{0}, as the effect of this update.

Updates may be combined into blocks of updates. A block of n updates takes the form

f(t_{1}) := s_{1}
⋮
f(t_{n}) := s_{n}

where t_{1}, ⋯, t_{n} denote tuples of expressions. To execute a block of n updates, all of its updates are executed simultaneously.

The qualified choose construct can be used to describe non-determinism. Its form is

choose x in S satisfying p(x)

B(x)

where x is a variable, S is a sort, p(x) is a Boolean expression containing the variable x, while B(x) is a block of updates that contains expressions mentioning the variable x. To execute this choose construct we non-deterministically choose a value v with sort S such that p(v) is satisfied. This value is then substituted for x in B(x) and the resulting block B(v) is executed. If there is no value v in S such that p(v) is satisfied, then the computation terminates.

The guarded block has the form

if G then

B

where G is a Boolean expression referred to as the guard of the block B. This block is executed only if the guard G evaluates to true.

It should be noted that the choose construct and the guarded block can be mixed freely. All further notations used like, e.g. the initialization, are self explanatory. The above explanation of abstract state machines should be sufficient for the rest of this paper. The methodology applied in this paper has been suggested by Börger, cf. [Börger 1995].

2 Preliminaries

The constrained shortest path problem is a generalization of the shortest path problem. For didactic purposes, we define this simpler and well known problem first. To this end, we introduce the notion of a weighted graph, i.e. a graph where a weight is associated with every edge.

Definition 1 (weighted graph) A weighted graph is a triple ⟨𝕍, 𝔼, ∥·∥⟩ such that the pair ⟨𝕍, 𝔼⟩ is a directed graph and ∥ · ∥ : 𝔼 → ℕ is a function assigning a natural number to every edge. If ∥e∥ = l, then l is the weight of e. ∥e∥ is also called the length of e. For any edge e = ⟨v, w⟩ we use the notation head(e) = w and tail(e) = v, i.e. an edge is regarded as an arrow pointing from tail(e) to head(e). □

The definition of a weighted graph given above is actually the definition of a directed weighted graph. However, there is no loss in generality since an undirected weighted graph can be seen as a special case of a weighted graph where the set 𝔼 and the function ∥ · ∥ are symmetric.

Paths are defined as usual. The set of all paths will be denoted as ℙ. The function ∥ · ∥ is extended to ℙ by collecting all the weights along the path, i.e.

∥e_{1}e_{2} ⋯ e_{n}∥ := ∑_{i=1}^{n} ∥e_{i}∥.

If p = e_{1}e_{2} ⋯ e_{n} is a path in G, then we say that p connects the node tail(e_{1}) with the node head(e_{n}). Furthermore, the empty path ε connects every node to itself. The set of all paths connecting node v with node w will be denoted as ℙ(v, w).

In the rest of this paper we will assume that every graph is finite.

Definition 2 (shortest path problem) Given a distinguished node source, the single source shortest path problem consists in computing the function

sp : 𝕍 → ℕ

sp(v) := min{∥p∥ : p ∈ ℙ(source, v)}. □

For the constrained shortest path problem we redefine the notion of a weighted graph by letting the function ∥·∥ assign a pair of natural numbers to every edge, i.e. we have ∥ · ∥ : 𝔼 → ℕ × ℕ. Again, ∥e∥ is called the weight of e. If ∥e∥ = ⟨l, c⟩, then l is called the length of e and c is called the cost of e. Therefore, we introduce two functions length and cost satisfying ∥e∥ = ⟨length(e), cost(e)⟩. These functions are extended from 𝔼 to ℙ:

length(e_{1} ⋯ e_{n}) := ∑_{i=1}^{n} length(e_{i}), cost(e_{1} ⋯ e_{n}) := ∑_{i=1}^{n} cost(e_{i}).

Definition 3 (SF) A function f : ℕ → ℕ ∪ {∞} is a monotonically decreasing step function iff

l_{1} ≤ l_{2} ⇒ f(l_{2}) ≤ f(l_{1}).

The set of all monotonically decreasing step functions is denoted by SF. □

Definition 4 (constrained shortest path problem) Given a distinguished node source, the constrained shortest path problem consists in computing the following function:

csp : 𝕍 → SF

csp(v)(l) := min{cost(p) : p ∈ ℙ(source, v) ∧ length(p) ≤ l}. □

In the form given above, it is not easy to see that the constrained shortest path problem and the shortest path problem are instances of the same problem. In order to emphasize the similarity between these problems we reformulate the constrained shortest path problem. To this end, we interpret the weight ∥e∥ of an edge e as the following step function:

∥e∥ : ℕ → ℕ ∪ {∞}

∥e∥(l) := \{ \begin{matrix}∞ & if l < length(e); \\ cost(e) & if l ≥ length(e). \end{matrix}

Next, we introduce a notion of addition for step functions.

Definition 5 (+) For f, g ∈ SF the function f + g is defined as follows: (f + g)(l) = min{f(l_{1}) + g(l_{2}) : l_{1} + l_{2} ≤ l} □

Now the function ∥ · ∥ is extended from 𝔼 to ℙ as follows:

∥e_{1} ⋯ e_{n}∥ := ∑_{i=1}^{n} ∥e_{i}∥.

Then the following is immediate:

Lemma 6 If p ∈ ℙ and l ∈ ℕ, then:

∥p∥(l) := \{ \begin{matrix}∞ & if l < length(p); \\ cost(p) & if l ≥ length(p). \end{matrix} □

Proof: This is an easy induction on the number of edges of p.

The previous lemma enables us to give a different formulation of the constrained shortest path problem that resembles the formulation of the shortest path problem more closely. However, there is one important difference: In contrast to the set ℕ of natural numbers, the function space SF is not linearly ordered. Therefore, in general the minimum of two functions f_{1}, f_{2} ∈ SF does not exist. Instead, the greatest lower bound (glb) has to be used. It is defined as the pointwise minimum of f_{1} and f_{2}, i.e. glb(f_{1}, f_{2})(l) = min(f_{1}(l), f_{2}(l)). Then the constrained shortest path problem can be reformulated as shown by the following theorem.

Theorem 7 csp(v) = glb{∥p∥ : p ∈ ℙ(source, v)}.

Proof: For all l ∈ ℕ we have the following chain of equations:

csp(v)(l) = min{cost(p) : p ∈ ℙ(source, v) ∧ length(p) ≤ l}

= min{∥p∥(l) : p ∈ ℙ(source, v) ∧ length(p) ≤ l}

(by Lemma 6) = min{∥p∥(l) : p ∈ ℙ(source, v)}

(since ∥p∥(l) = ∞ if l < length(p)) = glb{∥p∥ : p ∈ ℙ(source, v)}(l)

(since glb is defined pointwise) □

3 A Generic Algorithm for Solving Shortest Path Problems

In this section we present an algorithm that is able to solve generalized shortest path problems. The algorithm is generic. This is achieved by working with an abstract data type. The benefit of this approach is twofold. Firstly, it is quite universal. The algorithm presented in this section can be used to solve the classical shortest path problem as well as the constrained shortest path problem. Secondly, this approach simplifies the development of the algorithm: By separating the implementation of the abstract data type from the implementation of the generic algorithm to solve the shortest path problem we have effectively split our original problem into smaller problems that are easier to solve.

Proceeding in this spirit, we generalize the notion of a weighted graph given in the last section by working with an abstract version of the function ∥·∥, i.e. we do no longer assume that the result of ∥ · ∥ is a pair of positive natural numbers. Rather, the signature of ∥ · ∥ is now given as

∥ · ∥ : 𝔼 → 𝕎,

where the set 𝕎 is a set of abstractly given weights. This set comes together with a relation ≺⊆ 𝕎 × 𝕎, elements 0, ∞ ∈ 𝕎, a function glb : 𝕎 × 𝕎 → 𝕎, and a function + : 𝕎 × 𝕎 → 𝕎 satisfying the following axioms:

1. (𝕎, ≺) is a partial order.

2. ≺ is well–founded.

3. 0 is the smallest element w.r.t. ≺, i.e. 0 ⪯ w for all w ∈ 𝕎.

4. ∞ is the largest element w.r.t. ≺, i.e. w ⪯ ∞ for all w ∈ 𝕎.

5. glb(m_{1}, m_{2}) is the greatest lower bound of m_{1} and m_{2}, i. e.

(a) glb(m_{1}, m_{2}) ⪯ m_{1} ∧ glb(m_{1}, m_{2}) ⪯ m_{2},

(b) m_{3} ⪯ m_{1} ∧ m_{3} ⪯ m_{2} ⇒ m_{3} ⪯ glb(m_{1}, m_{2}).

6. glb is left distributive w.r.t. +, i.e.

glb(m_{1} + w, m_{2} + w) = glb(m_{1}, m_{2}) + w.

It is easy to see that + is left monotone in its second argument, i.e.

m_{1} ⪯ m_{2} ⇒ m_{1} + w ⪯ m_{2} + w.

Proof: m_{1} ⪯ m_{2} is equivalent to glb(m_{1}, m_{2}) = m_{1}. Therefore,

glb(m_{1}, m_{2}) + w = m_{1} + w.

Now the distributivity of glb w.r.t. + shows

glb(m_{1} + w, m_{2} + w) = m_{1} + w.

This is equivalent to m_{1} + w ⪯ m_{2} + w. □ Since ≺ is well–founded, the function glb can be extended to countable sets.

Theorem 8 If M = {m_{i} : i ∈ ℕ} ⊆ 𝕎 is a countable set, then the greatest lower bound of M exists.

Proof: We define a sequence (g_{i})_{i∈ℕ} by induction.

1. g_{0} := ∞.

2. g_{i+1} := glb(g_{i}, m_{i}).

We have g_{i+1} ⪯ g_{i} for all i ∈ ℕ. Since ≺ is well–founded, there exists a k ∈ ℕ such that g_{i} = g_{k} for all i ≥ k. It is straightforward to see that g_{k} is the greatest lower bound of M. □ Remark: Using transfinite induction, we can extend the last theorem to sets of arbitrary cardinality. This shows that the structure (𝕄, ≺, 0, ∞, glb) is a complete lattice. The least upper bound of a set S is defined as

lub(s) := glb{y : ∀x ∈ S : x ⪯ y}.

3.1 The Algorithm

We extend the function ∥ · ∥ from 𝔼 to ℙ by defining

∥e_{1} ⋯ e_{n}∥ := ∥e_{1}∥ + ⋯ + ∥e_{n}∥.

We assume to be given a distinguished node source. Our goal is to compute the function min weight : 𝕍 → 𝕎 defined as

min weight(v) := glb{∥p∥ : p ∈ ℙ(source, v)}.

Since the set of all paths from source to v is at most countable, Theorem 8 shows that the above greatest lower bound exists. (Theorem 8 is needed because,

although there are only finitely many nodes, the set ℙ(source, v) need not be finite. After all, there may exist paths containing cycles!)

In order to compute the function min weight the idea is to define a function

        label : 𝕍 → 𝕎

assigning a label to every node such that this label is an approximation from above of min weight(v), i.e. we always have min weight(v) ⪯ label(v). This function is successively improved until no further improvement is possible. Therefore, the algorithm proceeds as follows:

1. Initially, the only node v that is known to be connected to the source is the source itself. Therefore we label source with 0 and all nodes different from source are labeled with ∞.

2. Then, the following step is repeated as long as possible: We look for an edge e = ⟨v, w⟩ such that label(w) ⪯̸ label(v) + ∥e∥. If we are able to find an edge e with this property, then we relabel w with the new label glb(label(w), label(v) + ∥e∥). Otherwise, the algorithm terminates.

Note that in the second step the label of a node can only be decreased since we always have

        glb(label(w), label(v) + ∥e∥) ⪯ label(w).

The above inequality is strict iff label(w) ⪯̸ label(v) + ∥e∥.

        asm shortest path1( label : 𝕍 → 𝕎; source : 𝕍 )

initialization ∀x ∈ 𝕍\{source} : label(x) := ∞

                    label(source) := 0

transition relabeling

choose e = ⟨v, w⟩ in 𝔼

satisfying label(w) ⪯̸ label(v) + ∥e∥

                    label(w) := glb( label(w), label(v) + ∥e∥)
                    Figure 1: The ASM shortest path1.

A formalization is given by the ASM shortest path1 in Figure 1. The computation of this ASM stops as soon as we have label(w) ⪯ label(v) + ∥e∥ for every edge e = ⟨v, w⟩.

4 Correctness of shortest path1

Lemma 9 For any node v and any moment in the computation of the ASM shortest path1 the following invariant holds:

        min weight(v) ⪯ label(v).

Proof: The proof is done by induction on the computation of the ASM. In order to show the claim to be true after the initialization, we have to deal with two cases.

1. v = source. We have ε ∈ ℙ(source, v) and ∥ε∥ = 0, showing us that min weight(v) = 0. Since 0 ⪯ m for all m ∈ 𝕎 this proves the claim.

2. v ≠ source. Then we have label(v) = ∞ and since m ⪯ ∞ for all m ∈ 𝕎 the claim is obvious.

For the induction step assume the edge e = ⟨v, w⟩ to be chosen. Then label(w) is updated to the value

glb( label(w), label(v) + ∥e∥ ).

Therefore we have to show that

        min weight(w) ⪯ glb( label(w), label(v) + ∥e∥ )

holds. This is equivalent to the conjunction of (1) and (2) below:

        min weight(w) ⪯ label(w)  (1)

min weight(w) ⪯ label(v) + ∥e∥. (2)

(1) is true by the induction hypothesis stated for w and (2) follows from

        min weight(w) ⪯ min weight(v) + ∥e∥  (3)

and the induction hypothesis for v. In order to prove (3), we note that

{∥p e∥ : p ∈ ℙ(source, v)} ⊆ {∥q∥ : q ∈ ℙ(source, w)}

holds, since p ∈ ℙ(source, v) implies p e ∈ ℙ(source, w). Therefore,

glb{∥q∥ : q ∈ ℙ(source, w)} ⪯ glb{∥p e∥ : p ∈ ℙ(source, v)}.

Since ∥p e∥ = ∥p∥ + ∥e∥ and glb is distributive with respect to +, (3) follows from the definition of min weight. □

While the last lemma showed that label(v) is never too small, the next lemma shows that, once the algorithm has terminated, label(x) is not too big either.

Lemma 10 If the algorithm has terminated, then label(w) ⪯ ∥q∥ holds for any node w and any path q ∈ ℙ(source, w).

Proof: The proof is by induction on the number n of edges of q.

Base Case: n = 0 and therefore q = ε is the empty path. Then w = source and the claim is trivial since, initially, label(source) = 0 and subsequent relabeling can only decrease the value of the function label.

Step Case: The path has the form q = p e. If e = ⟨v, w⟩, then p is a path connecting source to v, i.e. p ∈ ℙ(source, v). By induction hypothesis label(v) ⪯ ∥p∥. Using the monotonicity of + this gives

label(v) + ∥e∥ ⪯ ∥p∥ + ∥e∥. (1)

If the algorithm has terminated, then

label(w) ⪯ label(v) + ∥e∥, (2)

since otherwise the choose construct would be able to choose the edge e and the algorithm would not have been terminated. Together (1) and (2) yield

label(w) ⪯ ∥p∥ + ∥e∥ = ∥p e∥ = ∥q∥. □

Theorem 11 (partial correctness) When the algorithm terminates, then we have label(v) = min weight(v) for any node v.

Proof: This is an immediate consequence of Lemma 9 and Lemma 10. □

Theorem 12 Every computation of the ASM shortest path1 terminates.

Proof: Every time the relabeling rule is applied, the label for one node w strictly decreases and the other labels remain unchanged. Since there are only finitely many nodes and the relation ≺ is well–founded, this rule can be applied only a finite number of times. □

5 Refining the ASM shortest path1

We refine the ASM shortest path1 to shortest path2 by eliminating the nondeterministic choice of edges. The method that we use is known in the literature as the labeling and scanning method, cf. [Tarjan 1983]. It is essentially a bookkeeping method that works by maintaining a set S of nodes that still need to be scanned, where scanning a node v is carried out in three steps:

1. The set E of all edges originating in v is computed. For this purpose, we use

the function adjacent defined as

adjacent(v) = {e ∈ 𝔼 : tail(e) = v}.

2. For every edge e = ⟨v, w⟩ in E such that

label(w) ⪯̸ label(v) + ∥e∥

we relabel w with glb(label(w), label(v) + ∥e∥). Then w is added to the set S of nodes that still need to be scanned, since it might then be possible to lower the labeling of nodes reachable via edges originating in w.

3. We delete v from the set S.

This is formalized by the ASM shortest path2 given in Figure 2. Note that the computation of this ASM terminates iff in the scanning rule the set S becomes empty, since then the choose construct is unable to produce a node v ∈ S.

5.1 Correctness of the Refinement

Theorem 13 The ASM shortest path2 computes the same value for the func-

tion label as the ASM shortest path1.

Proof: We show that every computation of shortest path2 can be regarded as a computation of shortest path1. Indeed, if we abstract from the variables S, E, and mode, then

– the initialization of shortest path2 is the same as that of shortest path1,

– the transition rules “scanning” and “back to scanning” have no effect, and – the transition rule “relabeling” has the same effect on the function label for

both ASMs.

     asm shortest path2( label : 𝕍 → 𝕎; source : 𝕍 )

initialization ∀x ∈ 𝕍\{source} : label(x) := ∞

                 label(source) := 0
                 S := {source}
                 mode := scan

transition scanning

          if  mode = scan

then choose v in 𝕍 satisfying v ∈ S

                 E := adjacent(v)

S := S − {v}

                 mode := relabel

transition relabeling

          if  mode = relabel

& E ≠ ∅ then choose e = ⟨v, w⟩ in 𝔼 satisfying e ∈ E

E := E − {e}

if label(w) ⪯̸ label(v) + ∥e∥

                 then label(w) := glb( label(w), label(v) + ∥e∥)

S := S ∪ {w}

transition back to scanning

          if  mode = relabel

& E = ∅

          then mode := scan.

                    Figure 2: The ASM shortest path2.

We have seen already that the relabeling rule can decrease the value of the function label only a finite number of times, but the ASM shortest path2 can execute this rule without changing the value of the function label. Therefore we have to exclude the possibility of infinite computations of shortest path2. To this end, assume that (s_{n})_{n} is a sequence of states resulting from a computation of shortest path2. Then there must be a time t such that for all n ≥ t the value of the function label remains unchanged in the transition from s_{n} to s_{n+1}. But from that time on the set S can never be increased, since S is only increased when the function label is decreased. The computations of shortest path2 consist of cycles described by the following regular expression:

“scanning” “relabeling”^{∗} “back to scanning”.

Every relabeling step decreases the size of E, therefore after a finite number of relabeling steps, E will be empty and the transition back to scanning is executed. This is followed by a scanning step that decreases the size of S. Therefore, termination of shortest path2 is guaranteed.

Furthermore, we have to exclude the possibility that the computation of the ASM shortest path2 terminates prematurely. This could happen if S = ∅ in the scanning step although there is an edge e = ⟨v, w⟩ such that

label(w) ⪯̸ label(v) + ∥e∥. (∗)

Define t_{0} as the earliest time such that the above inequality holds from t_{0} on up to the termination of the ASM. We first show that then v ∈ S must hold at time t_{0}. To prove this claim, we need a case distinction:

1. Case: t_{0} = 0. Since at t_{0} the only node satisfying label(v) ≠ ∞ is v = source, we have v = source and therefore v ∈ S at t_{0}.

2. Case: t_{0} > 0. Then the relabeling rule must have decreased the value of

label(v) at time t_{0} − 1. (After all, the only way for the inequality label(w) ⪯ label(v) + ∥e∥ to become false is when label(v) is decreased. A decrease of label(w) would surely leave this inequality valid.) But if label(v) has been

decreased at time t_{0} − 1, then v must have been added to S at t_{0} − 1 and we have v ∈ S at t_{0}.

Since v ∈ S at t_{0} and the ASM terminates only when S is empty, there must be a time t_{1} > t_{0} such that v is selected in the scanning step. Because in the following sequence of relabeling steps all edges leaving v are eventually dealt with, there is a time t_{2} > t_{1} such that the edge e = ⟨v, w⟩ is selected at this time by the relabeling rule. Since then the update

        label(w) := glb( label(w), label(v) + ∥e∥)

is executed, we have label(w) = glb( label(w), label(v) + ∥e∥) at time t_{2} + 1, contradicting (∗). □

5.2 Moore’s Algorithm

The algorithm presented in subsection 5.1 above still contains non-determinism since it makes use of the choose construct. We eliminate this non-determinism in this subsection. In order to do this we have to decide how the sets S and E should be represented. We implement S as a queue, while E is implemented as a stack. Then, we arrive at the following implementation shown in Figure 3, where we make use of some functions working on queues and stacks that are specified below:

 – Queue : T → Queue(T)

This function is a constructor of the polymorphic data type Queue. If v is a node, then Queue(v) is a queue containing precisely the node v.

 – empty : Queue(T) → bool

The call empty(Q) evaluates to true iff the queue Q is empty.

 – head : Queue(T) → T

If Q is not empty, then head(Q) returns the first element of Q.

 – pop : Queue(T) → Queue(T)

If Q is not empty, then pop(Q) pops the first element of Q.

 – ∈: T × Queue(T) → bool

The call t ∈ Q yields true iff t is an element of the queue Q.

 – append : Queue(T) × T → Queue(T)

The call append(Q, t) appends the element t at the end of the queue Q.

Furthermore, we use a bit of Prolog notation in Figure 3: [] denotes the empty stack, while [X|Xs] denotes a non-empty stack with top element X and tail Xs, i.e. we have that Xs is the result of removing X from the stack [X|Xs].

It should be noted that the choose construct used with shortest path2 is replaced by appropriately strengthening the guards of the corresponding transition rules in shortest path3. Note further that the ASM shortest path3 terminates when the queue S is empty and mode = scan since then no rule is applicable.

     asm shortest path3( label : 𝕍 → 𝕎; source : 𝕍 )

initialization ∀x ∈ 𝕍\{source} : label(x) := ∞,

                 label(source) := 0,
                 S := Queue(source),
                 mode := scan.

transition scanning

          if  mode = scan
             & ¬ empty(S)
          then E := adjacent(head(S))
                 S := pop(S)
                 mode := relabel

transition relabeling

          if  mode = relabel

& E = [ ⟨v, w⟩ | E′] then E := E′

if label(w) ⪯̸ label(v) + ∥e∥

                 then label(w) := glb( label(w), label(v) + ∥e∥)

if w ∉ S

then S := append(S, w)

transition back to scanning

          if  mode = relabel

& E = []

          then mode := scan.

                    Figure 3: The ASM shortest path3.

When comparing the ASMs shortest path2 and shortest path3, there is a subtle difference to note: The update S := append(S, w) in the ASM shortest path3 is guarded by the condition w ∉ S, while the corresponding update S := S ∪ {w} in shortest path2 is not subject to a similar condition. This guard takes care of maintaining the invariant that the queue S contains every element at most once. This invariant is necessary since, without this precaution, a queue represents a multiset rather than a set. We skip the (standard) proof that this queue implementation is correct. (The sceptical reader may look at the more elaborate proof given for the implementation of the slightly more complex queue concept in the Transputer using ASMs in [Börger and Durdanovic 1996].)

6 Instantiation of the ASM shortest path3

Up to now the ASMs we have presented are generic since they all contain the abstract data type 𝕎. In this section we instantiate 𝕎 with concrete data types and thereby solve both the shortest path problem and the constrained shortest path problem.

6.1 Solving the Shortest Path Problem

To solve the shortest path problem, we instantiate 𝕎 with the set ℕ∪{∞}. Then the interpretation of ≺ is the obvious extension of the usual ordering < on natural numbers to ℕ ∪ {∞} and glb(x, y) is interpreted as the minimum min(x, y). Finally, x + y is interpreted as the sum of x and y if x is a natural number and as ∞ if x equals ∞. It is trivial to verify that the conditions postulated in Section 3 are satisfied by this instantiation. Using this instantiation we obviously have

        min weight(v) = sp(v),

showing that the ASM shortest path3 solves the shortest path problem.

6.2 Solving the Constrained Shortest Path Problem

To solve the constrained shortest path problem, we instantiate 𝕎 with the function space SF. The ordering ≺ is defined pointwise, i.e.

f ⪯ g ⟺^{def} ∀t ∈ ℕ : f(t) ≤ g(t)

and f ≺ g ⟺^{def} f ⪯ g ∧ f ≠ g. The greatest lower bound and the addition have already been defined in Section 2. Using these definitions it is straightforward to verify that the specification of the abstract data type 𝕎 given in Section 3 is satisfied. The only requirement that is not trivial to check is the well–foundedness of ≺.

Lemma 14 The ordering ≺ on SF is well–founded.

Proof: For every f ∈ SF we define

x_{min}(f) := min{x ∈ ℕ : f(x) < ∞}.

If f, g ∈ SF and f ⪯ g, then x_{min}(f) ≤ x_{min}(g), since the assumption x_{min}(f) > x_{min}(g) yields f(x_{min}(g)) = ∞ > g(x_{min}(g)) in contradiction to f ⪯ g. In a similar way, we define for every f ∈ SF

y_{min}(f) := min{f(x) : x ∈ ℕ}.

It is trivial to check that f ⪯ g implies y_{min}(f) ≤ y_{min}(g). Furthermore, for every f ∈ SF we define

x_{max}(f) := min{x ∈ ℕ : f(x) = y_{min}(f)}

If f ⪯ g and y_{min}(f) = y_{min}(g), then x_{max}(f) ⪯ x_{max}(g). To see this, assume x_{max}(f) > x_{max}(g). This would produce the contradiction

f(x_{max}(g)) > f(x_{max}(f)) = y_{min}(f) = y_{min}(g) = g(x_{max}(g).

Next, we define for every f ∈ SF the integral

I(f) := ∫_{xmin(f)}^{xmax(f)}f(t)dt.

If we have f ≺ g, x_{min}(f) = x_{min}(g), and y_{min}(f) = y_{min}(g), then we have seen above that x_{max}(f) ≤ x_{max}(g) holds. Therefore, in this case we have the following chain of inequations:

I(f) := ∫_{xmin(f)}^{xmax(f)}f(t)dt ≤ ∫_{xmin(g)}^{xmax(g)}f(t)dt < ∫_{xmin(g)}^{xmax(g)}g(t)dt = I(g).

In this chain the strict inequation is valid since for all t ∉ [x_{min}(g), x_{max}(g)] the values of f and g coincide. Since f ≺ g, there must be a t ∈ [x_{min}(g), x_{max}(g)] such that f(t) ≺ g(t).

Finally, let us assign the ordinal

o(f) := ω ∗ (x_{min}(f) + y_{min}(f)) + I(f)

to every f ∈ SF. Then we can show that f ≺ g yields o(f) ≺ o(g). Indeed, f ≺ g yields x_{min}(f) ≤ x_{min}(g) and y_{min}(f) ≤ y_{min}(g). If either of these inequations is strict, then the claim is obvious. Otherwise, i.e. if we have x_{min}(f) = x_{min}(g) and y_{min}(f) = y_{min}(g), then we have just shown that I(f) < I(g). □

It is easy to see that, with the instantiations given above, we have

        min weight(v) = glb{∥p∥ : p ∈ ℙ(source, v)}.

Therefore, Theorem 7 shows that the ASM shortest path3 solves the constrained shortest path problem.

6.3 Representation of SF

In order to make the instantiation 𝕎 ↦ SF work, we have to implement the operations ≺, glb, and + for functions from SF. To this end, we have to choose a representation for the set SF.

Definition 15 (SF′) The set of representations SF′ is defined as the set of all lists of pairs of natural numbers of the form

[ ⟨x_{1}, y_{1}⟩, ⋯, ⟨x_{n}, y_{n}⟩ ]

satisfying the following representation invariant:

1. x_{i}, y_{i} ∈ ℕ for all i = 1, ⋯, n,

2. x_{i} < x_{i+1} for all i = 1, ⋯, n − 1,

3. y_{i} > y_{i+1} for all i = 1, ⋯, n − 1.

Definition 16 ([[f]]) If f = [ ⟨x_{1}, y_{1}⟩, ⋯, ⟨x_{n}, y_{n}⟩ ] ∈ SF′, then the function [[f]] ∈ SF represented by f is defined as follows:

[[f]](t) := { ∞ if t < x_{1}; y_{1} if x_{1} ≤ t < x_{2}; ⋮ y_{n−1} if x_{n−1} ≤ t < x_{n}; y_{n} if x_{n} ≤ t. □

Equivalently, [[f]] could be defined via:

[[f]](t) = min({y_{i} : x_{i} ≤ t, i = 1, ⋯, n}).

We have [[[]]] = ∞ and [[[⟨0, 0⟩]]] = 0.

We need to define an auxiliary function merge in order to compute the greatest lower bound of two functions from SF.

Definition 17 For f_{1}, f_{2} ∈ SF′, merge(f_{1}, f_{2}) is defined recursively:

1. merge([], f) = f.

2. merge(f, []) = f.

3. If x_{1} ≤ x_{2}, then merge([ ⟨x_{1}, y_{1}⟩ | f_{1} ], [ ⟨x_{2}, y_{2}⟩ | f_{2} ]) equals [ ⟨x_{1}, y_{1}⟩ | merge(f_{1}, [ ⟨x_{2}, y_{2}⟩ | f_{2} ]) ]

4. If x_{1} > x_{2}, then merge([ ⟨x_{1}, y_{1}⟩ | f_{1} ], [ ⟨x_{2}, y_{2}⟩ | f_{2} ]) equals = [ ⟨x_{2}, y_{2}⟩ | merge([ ⟨x_{1}, y_{1}⟩ | f_{1} ], f_{2}) ] □

Note that merge(f_{1}, f_{2}) is, in general, not an element of SF′ since the representation invariant is not maintained. For example, we have

merge([⟨1, 1⟩], [⟨2, 2⟩]) = [⟨1, 1⟩, ⟨2, 2⟩]

We need a function contract that reestablishes the representation invariant.

Definition 18 (contract) The value contract(f) is defined by induction on the length of the list f:

1. contract([]) = [].

2. contract([⟨x, y⟩]) = [⟨x, y⟩].

3. If x_{1} = x_{2}, then contract([ ⟨x_{1}, y_{1}⟩, ⟨x_{2}, y_{2}⟩ | f ]) = contract([ ⟨x_{1}, min(y_{1}, y_{2})⟩ | f ]).

4. If x_{1} ≠ x_{2} and y_{1} > y_{2}, then contract([ ⟨x_{1}, y_{1}⟩, ⟨x_{2}, y_{2}⟩ | f ]) = [ ⟨x_{1}, y_{1}⟩ | contract([ ⟨x_{2}, y_{2}⟩ | f ]) ].

5. If x_{1} ≠ x_{2} and y_{1} ≤ y_{2}, then contract([ ⟨x_{1}, y_{1}⟩, ⟨x_{2}, y_{2}⟩ | f ]) = contract([ ⟨x_{1}, y_{1}⟩ | f ]). □

Definition 19 (glb′) For f_{1}, f_{2} ∈ SF′ we define glb′(f_{1}, f_{2}) = contract(merge(f_{1}, f_{2})) □

The next lemma shows that the above definition of glb′ computes the greatest lower bound of the set SF.

Lemma 20 If f_{1}, f_{2} ∈ SF′, then glb′(f_{1}, f_{2}) ∈ SF′. Furthermore, [[glb′(f_{1}, f_{2})]] = glb([[f_{1}]], [[f_{2}]]). □

Proof: This lemma can be shown by a simple expansion of the definitions. □ Implementing the relation ≺ is now straightforward:

Definition 21 (≺) f_{1} ≺ f_{2} ⟺^{def} glb′(f_{1}, f_{2}) = f_{1}. □

We proceed to define addition for SF′. However, to simplify matters we note that we only need to define the addition of f + g where g is the weight of an edge. Since then the representation of g has the form [⟨x, y⟩], we get by with the following definition:

Definition 22 (+′) [ ⟨x_{1}, y_{1}⟩, ⋯, ⟨x_{n}, y_{n}⟩ ] +′ [⟨x, y⟩] := [⟨x_{1} + x, y_{1} + y⟩, ⋯, ⟨x_{n} + x, y_{n} + y⟩ ].

Lemma 23 If f ∈ SF′ and ⟨x, y⟩ ∈ ℕ×ℕ, then f +′[⟨x, y⟩] ∈ SF′. Furthermore, [[f +′ [⟨x, y⟩]]] = [[f]] + [[[⟨x, y⟩]]].

Proof: This lemma can be shown by a simple expansion of the definitions. □

Concluding Remark: At this point the implementation of SF is complete and we have developed an algorithm to solve the constrained shortest path problem. Based on the precise semantical ASM description given in [Wallace 1995] for the semantics of C++ we can transform the ASM obtained here to a C++-program and further optimize this program in the spirit of [Lauther 1996]. In this way we can prove the correctness of a highly sophisticated program that solves a non-trivial graph theoretical problem.

Acknowledgment: First of all, I would like to thank Egon Börger both for introducing me to his method of proving the correctness of software using abstract state machines and, furthermore, for various discussions during the case study presented here. Without these discussions, this case study would not have been completed in a satisfactory way. After having read an earlier draft of this paper, Peter Päppinghaus and Egon Börger both suggested numerous improvements.

Furthermore, I would like to thank Ulrich Lauther for introducing me to the constrained shortest path problem and for explaining his program solving this problem. Finally, I thank Bertil A. Brandin, Michael Hofmeister, Martin Müller, and Doris Tesch for helpful discussions.

This project has been sponsored from the German BMBF via the research grant no. 01 IS 519 A 9.

References

[Börger 1995] Börger, E.: “Why Use Evolving Algebras for Hardware and Software Engineering”. In Miroslav Bartosek, Jan Staudek, and Jiri Wiedermann, editors, SOFSEM ‘95, 22nd Seminar on Current Trends in Theory and Practice of Informatics, volume 1012 of Lecture Notes in Computer Science, pages 236–271, Springer, 1995.

[Börger and Durdanovic 1996] Börger, E. and Durdanovic, I.: “Correctness of Compiling Occam to Transputer Code”. In The Computer Journal, volume 39, no. 1, pages 52–92, 1996.

[Desrosiers et al. 1995] Desrosiers, J., Dumas Y., Solomon M., and Soumis, F.: “Time Constrained Routing and Scheduling”. In M. O. Ball, T. L. Magnanti, C. L. Monma, and G. L. Nemhauser, editors, Network Routing, volume 8 of Handbooks in Operations Research and Management Science, chapter 4, pages 35– 140. North-Holland, 1995.

[Gurevich 1993] Gurevich, Y.: “Evolving Algebras: An Attempt to Discover Semantics”. In G. Rozenberg and A. Salomaa, editors, Current Trends in Theoretical Computer Science, pages 266–292. World Scientific, 1993.

[Gurevich 1995] Gurevich, Y.: “Evolving Algebras 1993: Lipari Guide”. In Egon Börger, editor, Specification and Validation Methods, pages 3–36. Oxford University Press, 1995.

[Lauther 1996] Lauther, U.: “C++ Implementation of Constrained Shortest Path Cal-

culations”. Personal communication, 1996.

[Moore 1959] Moore, E. F.: “The Shortest Path Through a Maze”. In Proc. International Symposium on the Theory of Switching, Part II, volume 30 of The Annals of the Computation Laboratory of Harvard University, Cambridge, MA, 1959. Harvard University Press.

[Tarjan 1983] Tarjan, R. E.: “Data Structures and Network Algorithms.” volume 44 of CBMS-NSF Regional Conference Series in Applied Mathematics. SIAM, Philadelphia, PA, 1983.

[Wallace 1995] Wallace, C.: “The Semantics of the C++ Programming Language”. In Egon Börger, editor, Specification and Validation Methods, pages 131–164. Oxford University Press, 1995.