Skip to content

Instantly share code, notes, and snippets.

@FliegendeWurst

FliegendeWurst/ShortestPath.java Secret

Last active September 5, 2023 09:16
Show Gist options
  • Save FliegendeWurst/9be15e20e3bfd0722fcdd7f5c4afebcd to your computer and use it in GitHub Desktop.
Save FliegendeWurst/9be15e20e3bfd0722fcdd7f5c4afebcd to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ShortestPath.java
class ShortestPath {
//@ ghost \seq s;
/// ensures (l > 1) ==> \result == ph(p, p[i], l-1);
/*@ public normal_behaviour
@ requires l >= 1;
@ requires 0 <= i;
@ requires i < p.length;
@ requires (l > 1) ==> (0 <= p[i] & p[i] < p.length);
@ ensures (l == 1) ==> \result == p[i];
@
@ measured_by l;
@ strictly_pure
@*/
static int ph(long[] p, long i, long l) {
return l == 1 ? p[i] : ph(p, p[i], l-1);
}
/*@ public normal_behaviour
@ requires (\forall int i; 0 <= i & i < n.length; n[i].length == n.length);
@ requires (\forall int i; 0 <= i & i < n.length; (\forall int j; 0 <= j & j < n.length; -1 <= n[i][j]));
@ requires start >= 0 & start < n.length;
@ requires end >= 0 & end < n.length;
@ requires n.length >= 2;
@ requires start != end;
@ requires (\forall int i; 0 <= i & i < n.length; (\forall int j; 0 <= j & j < n.length; n[i][j] == 0 <==> i == j));
@ requires (\exists \seq p; 2 <= \dl_seqLen(p) & \dl_seqLen(p) <= n.length & (\forall int i; 0 <= i & i < \dl_seqLen(p);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(p, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(p) ==> n[(\dl_seqGet__int(p, i-1))][(\dl_seqGet__int(p, i))] != -1)
& (i == \dl_seqLen(p) - 1 ==> (\dl_seqGet__int(p, i)) == end))));
@ ensures \result.length >= 2;
@ ensures \result[0] == start;
@ ensures \result[\result.length - 1] == end;
@ ensures (\forall int i; 1 <= i & i < \result.length; n[\result[i-1]][\result[i]] != -1);
@*/
/*@ spec_bigint_math @*/
int[] bellmanFord(int[][] n, int start, int end) {
long[] d = new long[n.length];
long[] p = new long[n.length];
long[] l = new long[n.length];
//@ assert d != p;
//@ assert d != l;
//@ assert p != l;
/*@ loop_invariant 0 <= idx & idx <= d.length
& (\forall int j; 0 <= j & j < idx; d[j] == -1 & p[j] == -1 & l[j] == -1);
@ assignable d[*], p[*], l[*];
@ decreases d.length - idx;
@*/
for (int idx = 0; idx < d.length; idx++) {
d[idx] = -1;
p[idx] = -1;
l[idx] = -1;
}
d[start] = 0;
l[start] = 0;
p[start] = start;
/* All nodes x with d[x] != -1 have a valid path of length l[x].
* All paths with length <= x are explored (longer paths may also be explored).
* Values in d, p, l are valid.
* If a path exists, it is stored in p.
* Values in p correspond to existing edges.
* Length of path can be up to n-1.
*/
/*@ loop_invariant (\forall int dest; 0 <= dest & dest < n.length; dest != start & d[dest] != -1 ==> (\exists \seq s; 2 <= \dl_seqLen(s) & \dl_seqLen(s) <= n.length & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1 & p[(\dl_seqGet__int(s, i))] == (\dl_seqGet__int(s, i-1)))
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest)))))
& (\forall int dest; 0 <= dest & dest < n.length; (dest != start & (\exists \seq s; \dl_seqLen(s) >= 2 & \dl_seqLen(s) <= x & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1)
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest))))) ==> d[dest] != -1)
& (\forall int a; 0 <= a & a < n.length; l[a] >= -1 & l[a] <= n.length - 1 & -1 <= p[a] & p[a] < n.length & d[a] >= -1)
& (\forall int a; 0 <= a & a < n.length; d[a] != -1 & a != start ==> l[a] > 0 & p[a] >= 0 & p[a] < n.length & d[p[a]] != -1 & ph(p, a, (int) (l[a])) == start)
& (\forall int a; 0 <= a & a < n.length; p[a] >= 0 & p[a] < n.length ==> n[p[a]][a] != -1 & (a != start ==> d[p[a]] < d[a]) & d[a] != -1)
& d[start] == 0 & l[start] == 0 & p[start] == start
& (\forall int y; 0 <= y & y < n.length; (l[y] == 0 | p[y] == y) <==> y == start)
& (\forall int ni; 0 <= ni & ni < n.length; n[ni] != d & n[ni] != p & n[ni] != l)
& 0 <= x & x <= n.length - 1;
@ assignable d[*], p[*], l[*];
@ decreases n.length - x;
@*/
for (int x = 0; x < n.length - 1; x++) {
/* Paths of length x with last node <= i are expanded to length x+1 paths.
*/
/*@ loop_invariant
(\forall int dest2; 0 <= dest2 & dest2 < n.length; dest2 != start & d[dest2] != -1 ==> (\exists \seq s; 2 <= \dl_seqLen(s) & \dl_seqLen(s) <= n.length & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1 & p[(\dl_seqGet__int(s, i))] == (\dl_seqGet__int(s, i-1)))
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest2)))))
& (\forall int dest2; 0 <= dest2 & dest2 < n.length; dest2 != start & (\exists \seq s; 2 <= \dl_seqLen(s) & \dl_seqLen(s) <= n.length & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1 & p[(\dl_seqGet__int(s, i))] == (\dl_seqGet__int(s, i-1)))
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest2)))) ==> d[dest2] != -1)
& (\forall int a; 0 <= a & a < i; (\forall int dest; 0 <= dest & dest < n.length; (dest != start & d[a] != -1 & n[a][dest] != -1 & (\exists \seq s; \dl_seqLen(s) == l[a] + 1 & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1 & p[(\dl_seqGet__int(s, i))] == (\dl_seqGet__int(s, i-1)))
& (i == \dl_seqLen(s) - 2 ==> (\dl_seqGet__int(s, i)) == a)
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest)))) ==> d[dest] != -1 & l[dest] <= l[a] + 1 & p[dest] != -1)))
& (\forall int dest2b; 0 <= dest2b & dest2b < n.length; (dest2b != start & (\exists \seq s; \dl_seqLen(s) >= 2 & \dl_seqLen(s) <= x & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1)
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest2b))))) ==> d[dest2b] != -1)
& (\forall int a2; 0 <= a2 & a2 < n.length; l[a2] >= -1 & l[a2] <= n.length - 1 & -1 <= p[a2] & p[a2] < n.length & d[a2] >= -1)
& (\forall int a; 0 <= a & a < n.length; (d[a] != -1 & a != start) ==> l[a] > 0 & p[a] >= 0 & p[a] < n.length & d[p[a]] != -1)
& (\forall int a; 0 <= a & a < n.length; p[a] >= 0 & p[a] < n.length ==> n[p[a]][a] != -1 & (a != start ==> d[p[a]] < d[a]) & d[a] != -1)
& d[start] == 0 & l[start] == 0 & p[start] == start
& (\forall int y2; 0 <= y2 & y2 < n.length; (l[y2] == 0 | p[y2] == y2) <==> y2 == start)
& (\forall int ni; 0 <= ni & ni < n.length; n[ni] != d & n[ni] != p & n[ni] != l)
& 0 <= x & x < n.length - 1
& 0 <= i & i <= n.length;
@ assignable d[*], p[*], l[*];
@ decreases n.length - i;
@*/
for (int i = 0; i < n.length; i++) {
if (d[i] == -1) {
continue; // proven @ 2023-08-24
}
/* Paths of length x with last node == i are expanded to length x+1 paths to final node j.
*/
/*@ loop_invariant
(\forall int dest3; 0 <= dest3 & dest3 < n.length; dest3 != start & d[dest3] != -1 ==> (\exists \seq s; 2 <= \dl_seqLen(s) & \dl_seqLen(s) <= n.length & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1 & p[(\dl_seqGet__int(s, i))] == (\dl_seqGet__int(s, i-1)))
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest3)))))
& (\forall int dest3; 0 <= dest3 & dest3 < n.length; dest3 != start & (\exists \seq s; 2 <= \dl_seqLen(s) & \dl_seqLen(s) <= n.length & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1 & p[(\dl_seqGet__int(s, i))] == (\dl_seqGet__int(s, i-1)))
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest3)))) ==> d[dest3] != -1)
& (\forall int a; 0 <= a & a < i; (\forall int dest; 0 <= dest & dest < n.length; (dest != start & d[a] != -1 & n[a][dest] != -1 & (\exists \seq s; \dl_seqLen(s) == l[a] + 1 & (\forall int i; 0 <= i & i < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, i) & \dl_seqGet__int(s, i) < n.length
& ((i == 0 ==> (\dl_seqGet__int(s, i)) == start)
& (i == 1 ==> (\dl_seqGet__int(s, i)) != start)
& (i > 0 & i < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, i-1))][(\dl_seqGet__int(s, i))] != -1 & p[(\dl_seqGet__int(s, i))] == (\dl_seqGet__int(s, i-1)))
& (i == \dl_seqLen(s) - 2 ==> (\dl_seqGet__int(s, i)) == a)
& (i == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, i)) == dest)))) ==> d[dest] != -1 & l[dest] <= l[a] + 1 & p[dest] != -1)))
& (\forall int dest; 0 <= dest & dest < j; (dest != start & n[i][dest] != -1 & (\exists \seq s; \dl_seqLen(s) == l[i] + 1 & (\forall int ix; 0 <= ix & ix < \dl_seqLen(s);
0 <= \dl_seqGet__int(s, ix) & \dl_seqGet__int(s, ix) < n.length
& ((ix == 0 ==> (\dl_seqGet__int(s, ix)) == start)
& (ix == 1 ==> (\dl_seqGet__int(s, ix)) != start)
& (ix > 0 & ix < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, ix-1))][(\dl_seqGet__int(s, ix))] != -1 & p[(\dl_seqGet__int(s, ix))] == (\dl_seqGet__int(s, ix-1)))
& (ix == \dl_seqLen(s) - 2 ==> (\dl_seqGet__int(s, ix)) == i)
& (ix == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, ix)) == dest)))) ==> d[dest] != -1 & l[dest] <= l[i] + 1 & p[dest] != -1))
& (\forall int a2; 0 <= a2 & a2 < n.length; l[a2] >= -1 & l[a2] <= n.length - 1 & -1 <= p[a2] & p[a2] < n.length & d[a2] >= -1)
& (\forall int a; 0 <= a & a < n.length; (d[a] != -1 & a != start) ==> l[a] > 0 & p[a] >= 0 & p[a] < n.length & d[p[a]] != -1)
& (\forall int a; 0 <= a & a < n.length; p[a] >= 0 & p[a] < n.length ==> n[p[a]][a] != -1 & (a != start ==> d[p[a]] < d[a]) & d[a] != -1)
& d[start] == 0 & l[start] == 0 & p[start] == start
& (\forall int y3; 0 <= y3 & y3 < n.length; (l[y3] == 0 | p[y3] == y3) <==> y3 == start)
& (\forall int ni; 0 <= ni & ni < n.length; n[ni] != d & n[ni] != p & n[ni] != l)
& d[i] != -1
& 0 <= x & x < n.length - 1
& 0 <= i & i < n.length
& 0 <= j & j <= n.length;
@ assignable d[*], p[*], l[*];
@ decreases n.length - j;
@*/
for (int j = 0; j < n.length; j++) {
// relax edge from i to j
if (i == j || n[i][j] == -1 || j == start) {
continue; // proven @ 2023-08-24
}
//@ assert (\exists \seq s; \dl_seqLen(s) == l[i] + 1 & (\forall int ix; 0 <= ix & ix < \dl_seqLen(s);
//@ \dl_seqGet__int(s, ix) >= 0
//@ & \dl_seqGet__int(s, ix) < n.length
//@ & ((ix == 0 ==> (\dl_seqGet__int(s, ix)) == start)
//@ & (ix == 1 ==> (\dl_seqGet__int(s, ix)) != start)
//@ & (ix > 0 & ix < \dl_seqLen(s) ==> n[(\dl_seqGet__int(s, ix-1))][(\dl_seqGet__int(s, ix))] != -1 & p[(\dl_seqGet__int(s, ix))] == (\dl_seqGet__int(s, ix-1)))
//@ & (ix == \dl_seqLen(s) - 1 ==> (\dl_seqGet__int(s, ix)) == i))));
//@ assert n[i][j] >= 0 & d[i] >= 1 & d[i] < n.length & l[i] > 0;
long nDist = d[i] + n[i][j];
if (nDist < d[j]) {
d[j] = nDist;
p[j] = i;
l[j] = l[i] + 1;
// int_induction:
// nv >= s_0.length | (int)s_0[s_0.length - 1 - nv] != j_0
// provable:
// nv >= s_0.length | (@d[(int)s_0[s_0.length - 1 - nv]]@anon_heap_LOOP_3 < @d[j_0]@anon_heap_LOOP_3 & 0 <= (int)s_0[s_0.length - 1 - nv] & (int)s_0[s_0.length - 1 - nv] < n.length & @p[(int)(s_0[s_0.length - 1 - nv])]@@h3 < n.length & @p[(int)(s_0[s_0.length - 1 - nv])]@@h3 >= 0)
// required to prove, TODO: prove
// nv >= s_0.length | ((\forall int nv1; ((nv1 >= 0 & nv1 < nv) -> @d[(int)s_0[s_0.length - 1 - nv]]@anon_heap_LOOP_3 < @d[(int)s_0[s_0.length - 1 - nv1]]@anon_heap_LOOP_3)) & @d[(int)s_0[s_0.length - 1 - nv]]@anon_heap_LOOP_3 < @d[j_0]@anon_heap_LOOP_3 & 0 <= (int)s_0[s_0.length - 1 - nv] & (int)s_0[s_0.length - 1 - nv] < n.length & @p[(int)(s_0[s_0.length - 1 - nv])]@@h3 < n.length & @p[(int)(s_0[s_0.length - 1 - nv])]@@h3 >= 0)
// nv >= s_1.length | ((\forall int nv1; ((nv1 >= 0 & nv1 < nv) -> @d[(int)s_1[s_1.length - 1 - nv]]@anon_heap_LOOP_3 < @d[(int)s_1[s_1.length - 1 - nv1]]@anon_heap_LOOP_3)) & @d[(int)s_1[s_1.length - 1 - nv]]@anon_heap_LOOP_3 < @d[j_0]@anon_heap_LOOP_3 & 0 <= (int)s_1[s_1.length - 1 - nv] & (int)s_1[s_1.length - 1 - nv] < n.length & @p[(int)(s_1[s_1.length - 1 - nv])]@@h3 < n.length & @p[(int)(s_1[s_1.length - 1 - nv])]@@h3 >= 0)
// untested:
// nv >= s_2.length - 1 | ((int)s_2[s_2.length - 2 - nv] != (int)s_2[s_2.length - 1] & p[(int)s_2[s_2.length - 2 - nv]] >= 0 & p[(int)s_2[s_2.length - 2 - nv]] < n.length)
// nv >= s_2.length - 1 | (int)s_2[s_2.length - 2 - nv] != (int)s_2[s_2.length - 1]
// nv >= s_0.length | (\forall int z; ((s_0.length - 1 - nv < z & z < s_0.length) -> ((int)s_0[z] != (int)s_0[s_0.length - 1 - nv])))
// nv >= s_2.length | (\forall int z; ((s_2.length - 1 - nv < z & z < s_2.length) -> ((int)s_2[z] != (int)s_2[s_2.length - 1 - nv])))
//
// nv >= seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length | ((\forall int nv1; ((nv1 >= 0 & nv1 < nv) -> @d[(int)seqConcat(s_0, seqSub(s_1, i_21, s_1.length))[seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length - 1 - nv]]@anon_heap_LOOP_3 < @d[(int)seqConcat(s_0, seqSub(s_1, i_21, s_1.length))[seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length - 1 - nv1]]@anon_heap_LOOP_3)) & @d[(int)seqConcat(s_0, seqSub(s_1, i_21, s_1.length))[seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length - 1 - nv]]@anon_heap_LOOP_3 < @d[j_0]@anon_heap_LOOP_3 & 0 <= (int)seqConcat(s_0, seqSub(s_1, i_21, s_1.length))[seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length - 1 - nv] & (int)seqConcat(s_0, seqSub(s_1, i_21, s_1.length))[seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length - 1 - nv] < n.length & @p[(int)(seqConcat(s_0, seqSub(s_1, i_21, s_1.length))[seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length - 1 - nv])]@@h3 < n.length & @p[(int)(seqConcat(s_0, seqSub(s_1, i_21, s_1.length))[seqConcat(s_0, seqSub(s_1, i_21, s_1.length)).length - 1 - nv])]@@h3 >= 0)
}
}
}
}
//@ assert false;
if (d[end] == -1) {
return new int[0];
}
/* assert (\exists \seq a; \dl_seqLen(a) == l[end] & (\forall int i; 0 <= i & i < \dl_seqLen(a);
0 <= (\dl_seqGet__int(a, i)) & (\dl_seqGet__int(a, i)) < n.length & ((i == 0 ==> (\dl_seqGet__int(a, i)) == start)
& (i > 0 & i < \dl_seqLen(a) ==> n[(\dl_seqGet__int(a, i-1))][(\dl_seqGet__int(a, i))] != -1 & p[(\dl_seqGet__int(a, i))] == (\dl_seqGet__int(a, i-1)))
& (i == \dl_seqLen(a) - 1 ==> (\dl_seqGet__int(a, i)) == end))));
*/
int[] t = new int[l[end]];
t[t.length-1] = end;
/*@ loop_invariant ti <= l[end] - 1 & ti >= 0
& t[t.length - 1] == end
& (\forall int a; ti <= a & a < t.length; 0 <= t[a] & t[a] < n.length & d[t[a]] != -1)
& (\forall int a; ti <= a & a < t.length - 1; n[t[a]][t[a+1]] != -1)
& (\forall int a; ti <= a & a < t.length - 1; p[t[a+1]] == t[a]);
@ assignable t[*];
@ decreases ti;
@*/
for (int ti = l[end] - 1; ti > 0; ti--) {
t[ti-1] = p[t[ti]];
}
// set this.s = \dl_array2seq(t);
return t;
}
}
// nv >= s_0.length | (int)s_0[s_0.length - nv - 1] = @t[s_0.length - nv - 1]@anon_heap_LOOP_2
// @d[@t[ti_0]@anon_heap_LOOP_2]@anon_heap_LOOP_1 != -1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment