Breadth-first search on a small directed graph represented as an adjacency
Map<String, List>. Demonstrates: a queue (List) of frontier nodes, a visited Map used as a set, level-order distance tracking, and shortest unweighted path length between two nodes.
A Soma program from the algorithms part of the verified corpus: 69 lines, cells BFS, BFSTests. It passes soma check with soma 3.2.4.
How it is built
The cell BFS declares 3 signals in its face: adj() -> Map, reachable(src: String, dst: String) -> Bool and hops(src: String, dst: String) -> Int. Handlers: adj (line 16), hops (line 28) and reachable (line 53).
The file also holds 1 test cell (BFSTests) with 7 assertions, run by soma test.
The source
bfs.cell
// Breadth-first search on a small directed graph represented as an adjacency
// Map<String, List>. Demonstrates: a queue (List) of frontier nodes, a
// visited Map used as a set, level-order distance tracking, and shortest
// unweighted path length between two nodes.
//
// soma run examples/corpus/algorithms/bfs.cell hops A F
// soma test examples/corpus/algorithms/bfs.cell
cell BFS {
face {
signal adj() -> Map
signal reachable(src: String, dst: String) -> Bool
signal hops(src: String, dst: String) -> Int
}
on adj() {
return map(
"A", list("B", "C"),
"B", list("D"),
"C", list("D", "E"),
"D", list("F"),
"E", list("F"),
"F", list()
)
}
// shortest number of edges from src to dst, or -1 if unreachable
on hops(src: String, dst: String) {
let g = adj()
let dist = map()
dist[src] = 0
let queue = list(src)
let answer = -1
while len(queue) > 0 {
let node = queue[0]
let rest = list()
for i in range(1, len(queue)) { rest = push(rest, queue[i]) }
queue = rest
if node == dst {
answer = dist[node]
break
}
for nb in g[node] {
if (dist[nb] ?? -1) == -1 {
dist[nb] = dist[node] + 1
queue = push(queue, nb)
}
}
}
return answer
}
on reachable(src: String, dst: String) {
return hops(src, dst) >= 0
}
}
cell test BFSTests {
rules {
assert hops("A", "A") == 0
assert hops("A", "D") == 2
assert hops("A", "F") == 3
assert hops("C", "F") == 2
assert reachable("A", "F")
assert !reachable("F", "A")
assert hops("F", "A") == -1
}
}What the toolchain says
$ soma check bfs.cell
✓ All checks passed.$ soma test bfs.cell
test BFSTests ...
✓ assert hops("A", "A") == 0
✓ assert hops("A", "D") == 2
✓ assert hops("A", "F") == 3
✓ assert hops("C", "F") == 2
✓ assert reachable("A", "F")
✓ assert !reachable("F", "A")
✓ assert hops("F", "A") == -1
7 tests: 7 passed, 0 failed$ soma verify bfs.cell
Verifying bfs.cell...
BFS/termination:
⚠ handler `hops`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
⚠ `reachable` calls `BFS.hops`, which may not terminate
0 passed, 2 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK$ soma run bfs.cell hops A F
3