A MoonBit pathfinding and graph algorithms library with executable documentation, runtime-checked proof predicates, and multi-backend verification gates. Built for OSC 2026.
严谨工程化的 MoonBit 路径规划库 — 15+ 图算法 · WASM 原生 · 三后端一致 · 可执行文档。本文件既是项目 README,也是一份可执行测试脚本: 每段 ```mbt check 代码块都会被 moon test README.mbt.md 编译 + 运行 + 快照校验。文档永不过时,过时即构建失败。
关于代码围栏: 本文件的可执行代码块均以 ```mbt check 开头,这是 MoonBit toolchain 识别可运行代码块的标记; 块首的 ///| 是 MoonBit 的 top-level marker,用于声明该段为一个 独立条目。如需在 README 里展示不被执行的片段,把围栏改为 ```moonbit skip (本文件 示例 5 中展示)。
///|
test "README · BFS finds 4-node path on linear adjacency array" {
// 节点 0..3 串成一条链; successors 直接在邻接数组上查询。
let adj : Array[Array[Int]] = [[1], [2], [3], []]
let path = @uw.bfs(0, fn(n) { adj[n] }, fn(n) { n == 3 })
// path[0] == start, goal(path[-1]), 相邻节点均在 successors 中 (R13.2)
match path {
Some(p) => {
assert_true(p.length() == 4)
assert_true(p[0] == 0 && p[1] == 1 && p[2] == 2 && p[3] == 3)
}
None => assert_true(false)
}
}0 ─(1)─▶ 1 0 ─(4)─▶ 2
1 ─(2)─▶ 2 1 ─(5)─▶ 3
2 ─(1)─▶ 3///|
test "README · Dijkstra picks cheapest of three candidate paths" {
// 每个元素是 (邻居索引, 边权)
let adj : Array[Array[(Int, Int)]] = [
[(1, 1), (2, 4)], // 0: 0->1(1), 0->2(4)
[(2, 2), (3, 5)], // 1: 1->2(2), 1->3(5)
[(3, 1)], // 2: 2->3(1)
[], // 3: 目标,无出边
]
let result = @dir.dijkstra(0, fn(n) { adj[n] }, fn(n) { n == 3 })
match result {
Some((path, cost)) => {
inspect(cost, content="4")
@debug.debug_inspect(path, content="[0, 1, 2, 3]")
}
None => inspect("unreachable", content="should have found a path")
}
}///|
test "README · A-star on 3x3 grid with manhattan heuristic" {
// 4-方向移动, 每步代价 1
let successors = fn(pos : (Int, Int)) -> Array[((Int, Int), Int)] {
let (x, y) = pos
let neighbors = [(x + 1, y), (x - 1, y), (x, y + 1), (x, y - 1)]
let filtered : Array[((Int, Int), Int)] = []
for p in neighbors {
let (nx, ny) = p
if nx >= 0 && nx < 3 && ny >= 0 && ny < 3 {
filtered.push((p, 1))
}
}
filtered
}
// Admissible heuristic: 到 (2,2) 的曼哈顿距离
let heuristic = fn(pos : (Int, Int)) -> Int {
let (x, y) = pos
(2 - x).abs() + (2 - y).abs()
}
let result = @dir.astar((0, 0), successors, heuristic, fn(p) { p == (2, 2) })
match result {
Some((_path, cost)) => inspect(cost, content="4")
None => inspect("unreachable", content="goal should be reachable")
}
}0 ─(1)─ 1
│ │
(4) (2)
│ │
3 ─(3)─ 2///|
test "README · Kruskal MST picks 3 edges with total weight 6" {
let nodes = [0, 1, 2, 3]
// 边列表: (u, v, w), 无向图按无序对解读
let edges : Array[(Int, Int, Int)] = [
(0, 1, 1),
(1, 2, 2),
(2, 3, 3),
(3, 0, 4),
]
let mst = @und.kruskal_mst(nodes, edges)
// MST 应恰好有 |V| - 1 = 3 条边 (R13.4)
inspect(mst.length(), content="3")
// 总权重: 1 + 2 + 3 = 6
let total = mst.fold(init=0, fn(acc, e) {
let (_, _, w) = e
acc + w
})
inspect(total, content="6")
}状态: runtime-checked today; static moon prove discharge remains toolchain-dependent.src/proofs/*_proof.mbt already encodes the proof vocabulary as ordinary MoonBit predicates and runtime tests. The same predicates are intended to be referenced by future stable moon prove annotations.
///|
test "README · BFS proof predicate accepts shortest witness" {
let adj : Array[Array[Int]] = [[1], [2], [3], []]
let result : Array[Int]? = Some([0, 1, 2, 3])
inspect(
@proofs.bfs_post(result, 0, fn(n) { adj[n] }, fn(n) { n == 3 }, [0, 1, 2, 3]),
content="true",
)
}///|
/// Dijkstra shortest paths on non-negative weighted graphs.
///
/// # Invariants (R8-AC4)
/// - For every v with dist[v] < infinity, dist[v] is the cost of some valid
/// path from start to v.
/// - For every v popped from pq (and not dropped as a stale entry), dist[v]
/// is already the final shortest distance.
/// - All edge weights are non-negative => dist[v] >= Weight::zero() for
/// every reachable v.
pub fn[N : Eq + Hash, W : Weight] dijkstra(
start : N,
successors : (N) -> Array[(N, W)],
goal : (N) -> Bool,
) -> (Array[N], W)? {
let pq = PQueue::new()
let dist : Map[N, W] = Map::new()
let parents : Map[N, N] = Map::new()
dist[start] = Weight::zero()
pq.push(Weight::zero(), start)
/// invariant: forall v popped from pq (non-stale), dist[v] is final
/// invariant: forall v with dist[v] < infinity, exists valid path start->v
/// invariant: all edge weights >= zero => dist[v] >= Weight::zero()
while pq.pop() is Some((d, u)) {
if goal(u) {
return Some((reconstruct(parents, u), d))
}
// ... 松弛 successors(u) ...
}
None
}#requires(/* successors is total */)
#ensures(forall v : N. reachable(v) -> dist[v] >= Weight::zero())
#decreases(nodes.length() - visited.length())
pub fn[N : Eq + Hash, W : Weight] dijkstra(...) -> ... { ... }💡 只有 ```mbt check 围栏的代码块会参与测试; ```moonbit skip 仍用于展示 尚未稳定的未来 moon prove 语法。
///|
test "README · docgen 复杂度表覆盖 33 种算法且可重复生成" {
// 元数据数组恰好 33 条:30 种经典算法 + CH / JPS / ALT(R19.2)。
let metas = @docgen.algorithm_metadata()
inspect(metas.length(), content="33")
inspect(@docgen.algorithm_count, content="33")
// R19.3:同一元数据重复生成 → 复杂度表逐字段完全相等(确定性、可重复)。
let r1 = @docgen.complexity_table(metas)
let r2 = @docgen.complexity_table(@docgen.algorithm_metadata())
assert_true(r1 == r2)
// 从元数据 O(n) 线性生成 Markdown 复杂度表(R19.1)。
match r1 {
Ok(table) => {
// 表格 = 表头行 + 对齐分隔行 + 33 条数据行;每行以换行结尾,故共 35 个 '\n'。
let mut newlines = 0
for ch in table.iter().to_array() {
if ch == '\n' {
newlines = newlines + 1
}
}
inspect(newlines, content="35")
// 数据行数 = 总行数 - 表头 2 行 = 33(R19.2:唯一对应、无重复无遗漏)。
inspect(newlines - 2, content="33")
// 五列表头与 GFM 对齐分隔行齐备(R19.1)。
assert_true(
table.contains(
"| 算法 | 最坏时间复杂度 | 平均时间复杂度 | 空间复杂度 | 适用条件 |",
),
)
assert_true(table.contains("| --- | --- | --- | --- | --- |"))
// 经典算法首行五字段非空(R19.1)。
assert_true(table.contains("| BFS | O(V + E) | O(V + E) | O(V) |"))
// 三种旗舰高级算法各占唯一一行(R19.2)。
assert_true(table.contains("| Contraction Hierarchies |"))
assert_true(table.contains("| Jump Point Search |"))
assert_true(table.contains("| ALT |"))
}
Err(_) => assert_true(false)
}
}对应需求 R21 (Cookbook 与公开 API 文档完整性) — R21.1 (≥20 用例,覆盖 网格寻路 / 网络路由 / 任务调度 / 最大流 / 匹配五类,每类 ≥1)、R21.2 (每个用例在 wasm-gc / js / native 三后端均成功)、R21.5 (每个用例提供可执行命令与预期输出)。
moon test README.mbt.md///|
test "Cookbook 网格寻路 1 · BFS 在 5x5 空网格最短步数" {
let w = 5
let h = 5
let succ = fn(pos : (Int, Int)) -> Array[(Int, Int)] {
let (x, y) = pos
let cand = [(x + 1, y), (x - 1, y), (x, y + 1), (x, y - 1)]
let out : Array[(Int, Int)] = []
for p in cand {
let (nx, ny) = p
if nx >= 0 && nx < w && ny >= 0 && ny < h {
out.push(p)
}
}
out
}
let path = @uw.bfs((0, 0), succ, fn(p) { p == (4, 4) })
match path {
// 路径含 9 个格子 (8 步 + 起点)。
Some(p) => inspect(p.length(), content="9")
None => assert_true(false)
}
}///|
test "Cookbook 网格寻路 2 · BFS 绕过障碍墙" {
let w = 3
let h = 3
let blocked = fn(p : (Int, Int)) -> Bool { p == (1, 0) || p == (1, 1) }
let succ = fn(pos : (Int, Int)) -> Array[(Int, Int)] {
let (x, y) = pos
let cand = [(x + 1, y), (x - 1, y), (x, y + 1), (x, y - 1)]
let out : Array[(Int, Int)] = []
for p in cand {
let (nx, ny) = p
if nx >= 0 && nx < w && ny >= 0 && ny < h && !blocked(p) {
out.push(p)
}
}
out
}
let path = @uw.bfs((0, 0), succ, fn(p) { p == (2, 0) })
match path {
// 绕墙后最短路径含 7 个格子。
Some(p) => inspect(p.length(), content="7")
None => assert_true(false)
}
}///|
test "Cookbook 网格寻路 3 · A-star 曼哈顿启发式" {
let w = 5
let h = 5
let succ = fn(pos : (Int, Int)) -> Array[((Int, Int), Int)] {
let (x, y) = pos
let cand = [(x + 1, y), (x - 1, y), (x, y + 1), (x, y - 1)]
let out : Array[((Int, Int), Int)] = []
for p in cand {
let (nx, ny) = p
if nx >= 0 && nx < w && ny >= 0 && ny < h {
out.push((p, 1))
}
}
out
}
let heuristic = fn(pos : (Int, Int)) -> Int {
let (x, y) = pos
(4 - x).abs() + (4 - y).abs()
}
let result = @dir.astar((0, 0), succ, heuristic, fn(p) { p == (4, 4) })
match result {
Some((_path, cost)) => inspect(cost, content="8")
None => assert_true(false)
}
}///|
test "Cookbook 网格寻路 4 · A-star 绕障碍最优代价" {
let w = 3
let h = 3
let blocked = fn(p : (Int, Int)) -> Bool { p == (1, 0) || p == (1, 1) }
let succ = fn(pos : (Int, Int)) -> Array[((Int, Int), Int)] {
let (x, y) = pos
let cand = [(x + 1, y), (x - 1, y), (x, y + 1), (x, y - 1)]
let out : Array[((Int, Int), Int)] = []
for p in cand {
let (nx, ny) = p
if nx >= 0 && nx < w && ny >= 0 && ny < h && !blocked(p) {
out.push((p, 1))
}
}
out
}
let heuristic = fn(pos : (Int, Int)) -> Int {
let (x, y) = pos
(2 - x).abs() + (0 - y).abs()
}
let result = @dir.astar((0, 0), succ, heuristic, fn(p) { p == (2, 0) })
match result {
Some((_path, cost)) => inspect(cost, content="6")
None => assert_true(false)
}
}///|
test "Cookbook 网格寻路 5 · JPS 对角线跳点搜索" {
let blocked : Array[Bool] = Array::make(25, false)
let grid = @advanced.JPSGrid::new(5, 5, blocked).unwrap()
let result = @advanced.jps(grid, (0, 0), (4, 4))
match result {
Some((path, cost)) => {
// 4 步对角线,每步 √2 ≈ 1.4142135。
assert_true((cost - 4.0 * 1.4142135).abs() < 1.0e-6)
// 路径首尾分别为起点与终点。
assert_true(path[0] == (0, 0))
assert_true(path[path.length() - 1] == (4, 4))
}
None => assert_true(false)
}
}///|
test "Cookbook 网络路由 1 · Dijkstra 最便宜路由" {
let adj : Array[Array[(Int, Int)]] = [
[(1, 2), (2, 5)],
[(2, 1), (3, 7)],
[(3, 3), (4, 8)],
[(4, 2)],
[],
]
let result = @dir.dijkstra(0, fn(n) { adj[n] }, fn(n) { n == 4 })
match result {
Some((path, cost)) => {
inspect(cost, content="8")
@debug.debug_inspect(path, content="[0, 1, 2, 3, 4]")
}
None => assert_true(false)
}
}///|
test "Cookbook 网络路由 2 · Dijkstra 多跳优于直连" {
let adj : Array[Array[(Int, Int)]] = [
[(1, 1), (3, 10)],
[(2, 1)],
[(3, 1)],
[],
]
let result = @dir.dijkstra(0, fn(n) { adj[n] }, fn(n) { n == 3 })
match result {
Some((path, cost)) => {
inspect(cost, content="3")
@debug.debug_inspect(path, content="[0, 1, 2, 3]")
}
None => assert_true(false)
}
}///|
test "Cookbook 网络路由 3 · Bellman-Ford 负权边距离" {
let nodes = [0, 1, 2, 3]
let edges : Array[(Int, Int, Int)] = [
(0, 1, 4),
(0, 2, 5),
(1, 2, -3),
(2, 3, 2),
]
let result = @dir.bellman_ford(nodes, edges, 0)
match result {
Ok(dist) => {
@debug.debug_inspect(dist.get(2), content="Some(1)")
@debug.debug_inspect(dist.get(3), content="Some(3)")
}
Err(_) => assert_true(false)
}
}///|
test "Cookbook 网络路由 4 · Bellman-Ford 检测负环" {
let nodes = [0, 1, 2]
let edges : Array[(Int, Int, Int)] = [(0, 1, 1), (1, 2, -3), (2, 1, 1)]
let result = @dir.bellman_ford(nodes, edges, 0)
// 存在可达负环 → 返回结构化错误。
inspect(result is Err(_), content="true")
}///|
test "Cookbook 网络路由 5 · Dijkstra 单源最短路树" {
let adj : Array[Array[(Int, Int)]] = [
[(1, 2), (2, 5)],
[(2, 1), (3, 7)],
[(3, 3), (4, 8)],
[(4, 2)],
[],
]
let tree = @dir.dijkstra_all(0, fn(n) { adj[n] })
@debug.debug_inspect(tree.distance_to(4), content="Some(8)")
@debug.debug_inspect(tree.path_to(4), content="Some([0, 1, 2, 3, 4])")
}///|
test "Cookbook 任务调度 1 · 拓扑排序合法执行顺序" {
let adj : Array[Array[Int]] = [[1, 2], [3], [3], [4], []]
let result = @dir.topological_sort([0, 1, 2, 3, 4], fn(n) { adj[n] })
match result {
Ok(order) => {
inspect(order.length(), content="5")
// 校验拓扑性:每条依赖边 u→v 满足 pos[u] < pos[v]。
let pos : Map[Int, Int] = Map([])
for i, n in order {
pos[n] = i
}
let edges = [(0, 1), (0, 2), (1, 3), (2, 3), (3, 4)]
let mut valid = true
for e in edges {
let (u, v) = e
if pos.get(u).unwrap() >= pos.get(v).unwrap() {
valid = false
}
}
inspect(valid, content="true")
}
Err(_) => assert_true(false)
}
}///|
test "Cookbook 任务调度 2 · 拓扑排序检测循环依赖" {
let adj : Array[Array[Int]] = [[1], [2], [0]]
let result = @dir.topological_sort([0, 1, 2], fn(n) { adj[n] })
// 存在环 → 返回结构化错误。
inspect(result is Err(_), content="true")
}///|
test "Cookbook 任务调度 3 · DAG 最短完工路径" {
let adj : Array[Array[(Int, Int)]] = [
[(1, 3), (2, 2)],
[(3, 4)],
[(3, 5)],
[],
]
let result = @dir.dag_shortest_path([0, 1, 2, 3], 0, fn(n) { adj[n] }, fn(n) {
n == 3
})
match result {
Ok(Some((path, cost))) => {
inspect(cost, content="7")
inspect(path.length(), content="3")
}
Ok(None) => assert_true(false)
Err(_) => assert_true(false)
}
}///|
test "Cookbook 任务调度 4 · DAG 唯一关键路径" {
let adj : Array[Array[(Int, Int)]] = [
[(1, 1), (2, 4)],
[(2, 1), (3, 5)],
[(3, 1)],
[(4, 2)],
[],
]
let result = @dir.dag_shortest_path([0, 1, 2, 3, 4], 0, fn(n) { adj[n] }, fn(
n,
) {
n == 4
})
match result {
Ok(Some((path, cost))) => {
inspect(cost, content="5")
@debug.debug_inspect(path, content="[0, 1, 2, 3, 4]")
}
Ok(None) => assert_true(false)
Err(_) => assert_true(false)
}
}///|
test "Cookbook 最大流 1 · Edmonds-Karp 经典网络" {
let nodes = [0, 1, 2, 3, 4, 5]
let cap : Map[(Int, Int), Int] = Map([])
cap[(0, 1)] = 16
cap[(0, 2)] = 13
cap[(1, 2)] = 10
cap[(2, 1)] = 4
cap[(1, 3)] = 12
cap[(3, 2)] = 9
cap[(2, 4)] = 14
cap[(4, 3)] = 7
cap[(3, 5)] = 20
cap[(4, 5)] = 4
let flow = @dir.edmonds_karp(nodes, cap, 0, 5)
inspect(flow, content="23")
}///|
test "Cookbook 最大流 2 · Dinic 与 Edmonds-Karp 一致" {
let nodes = [0, 1, 2, 3, 4, 5]
let cap : Map[(Int, Int), Int] = Map([])
cap[(0, 1)] = 16
cap[(0, 2)] = 13
cap[(1, 2)] = 10
cap[(2, 1)] = 4
cap[(1, 3)] = 12
cap[(3, 2)] = 9
cap[(2, 4)] = 14
cap[(4, 3)] = 7
cap[(3, 5)] = 20
cap[(4, 5)] = 4
let flow = @dir.dinic(nodes, cap, 0, 5)
inspect(flow, content="23")
}///|
test "Cookbook 最大流 3 · 最小割等于最大流" {
let nodes = [0, 1, 2, 3, 4, 5]
let cap : Map[(Int, Int), Int] = Map([])
cap[(0, 1)] = 16
cap[(0, 2)] = 13
cap[(1, 2)] = 10
cap[(2, 1)] = 4
cap[(1, 3)] = 12
cap[(3, 2)] = 9
cap[(2, 4)] = 14
cap[(4, 3)] = 7
cap[(3, 5)] = 20
cap[(4, 5)] = 4
let (cut, _edges, _side) = @dir.min_cut(nodes, cap, 0, 5)
inspect(cut, content="23")
}///|
test "Cookbook 最大流 4 · 最小费用最大流" {
let nodes = [0, 1, 2, 3]
// (u, v, capacity, unit_cost)
let edges : Array[(Int, Int, Int, Int)] = [
(0, 1, 2, 1),
(0, 2, 2, 2),
(1, 3, 2, 1),
(2, 3, 2, 1),
]
let (flow, cost) = @dir.min_cost_max_flow(nodes, edges, 0, 3)
inspect(flow, content="4")
inspect(cost, content="10")
}///|
test "Cookbook 匹配 1 · Hopcroft-Karp 完美匹配" {
let left = [0, 1, 2]
let right = [10, 11, 12]
let adj = fn(l : Int) -> Array[Int] {
if l == 0 {
[10, 11]
} else if l == 1 {
[10]
} else {
[11, 12]
}
}
let matching = @und.hopcroft_karp(left, right, adj)
// 三条边全部匹配成功。
inspect(matching.length(), content="3")
}///|
test "Cookbook 匹配 2 · Hopcroft-Karp 非完美匹配" {
let left = [0, 1, 2]
let right = [10, 11]
let adj = fn(l : Int) -> Array[Int] {
if l == 0 {
[10]
} else if l == 1 {
[10]
} else {
[11]
}
}
let matching = @und.hopcroft_karp(left, right, adj)
// 受右侧容量限制,最大匹配规模为 2。
inspect(matching.length(), content="2")
}///|
test "Cookbook 匹配 3 · Kuhn-Munkres 最小代价指派 3x3" {
let cost : Array[Array[Double]] = [
[4.0, 1.0, 3.0],
[2.0, 0.0, 5.0],
[3.0, 2.0, 2.0],
]
match @und.kuhn_munkres(cost) {
Ok((assign, total)) => {
// assign[i] = 分配给工人 i 的工作编号。
@debug.debug_inspect(assign, content="[1, 0, 2]")
assert_true((total - 5.0).abs() < 1.0e-9)
}
Err(_) => assert_true(false)
}
}///|
test "Cookbook 匹配 4 · Kuhn-Munkres 最小代价指派 2x2" {
let cost : Array[Array[Double]] = [[3.0, 1.0], [2.0, 4.0]]
match @und.kuhn_munkres(cost) {
Ok((assign, total)) => {
@debug.debug_inspect(assign, content="[1, 0]")
assert_true((total - 3.0).abs() < 1.0e-9)
}
Err(_) => assert_true(false)
}
}# 编码修正 + 在项目根目录执行
chcp 65001
moon test README.mbt.mdTotal tests: 28, passed: 28, failed: 0.A MoonBit pathfinding and graph algorithms library with executable documentation, runtime-checked proof predicates, and multi-backend verification gates. Built for OSC 2026.