Comprehensive collection of algorithms and data structures with well-documented loop invariants for correctness reasoning

algorithms

data-structures

loop-invariants

competitive-programming

moon add bobzhang/loop_invariants@0.8.0

Download zip

Author

bobzhang

Version

0.8.0

License

Apache-2.0

Repository

github.com/moonbit-community/loop_invariants

Last updated

3 months ago

Downloads

README

#Loop Invariants in MoonBit

This repository is a learning library for algorithms. Each package explains one topic in clear, beginner-friendly language and shows why it works using loop invariants.

The repository is organized as a MoonBit workspace. The root module keeps the introductory examples and command-line sandbox, while algorithm packages live in domain modules under modules/.

If you are new to algorithms, you can read these packages like a book. Each README is designed to be understandable without heavy math.

#Workspace Modules

modules/graph: graph, tree, shortest path, flow, matching, and connectivity algorithms
modules/data_structures: Fenwick trees, segment trees, sparse tables, treaps, tries, and related structures
modules/string: string matching, hashing, suffix structures, and automata
modules/math: number theory, algebra, transforms, recurrence, and linear algebra routines
modules/geometry: computational geometry algorithms
modules/dp: dynamic programming examples and optimizations
modules/techniques: general competitive-programming techniques and search/window patterns
modules/persistent: persistent data structure examples
modules/verified: small verified examples with proof-oriented loop invariants

#What You Will Learn

How to translate a problem into a step-by-step algorithm
How to reason about correctness with loop invariants
How to write clean, testable MoonBit implementations

#How the Tutorials Are Written

Each package README follows this structure:

Problem statement in simple terms
Core idea (the intuition)
Step-by-step algorithm
Multiple examples
Complexity and pitfalls

Think of the README as a Wikipedia article: definition, motivation, examples, then implementation notes.

#How Examples Are Tested

README.mbt.md files include code blocks tagged mbt check. These blocks are compiled and run by moon test, so documentation stays correct.

If you want a snippet that should not run, use mbt nocheck instead.

///|
test "doc example runs" {
  debug_inspect(1 + 1, content="2")
}

#What Is a Loop Invariant?

A loop invariant is a sentence that stays true every time the loop repeats. It connects code to reasoning.

A good invariant explains:

what has been computed so far
what remains to be processed
why the algorithm will be correct at the end

#Example 1: Sum of an Array

We want the sum of all elements. The invariant is:

"After processing the first i elements, sum equals their total."

///|
test "invariant sum example" {
  let xs : Array[Int] = [1, 2, 3, 4]
  let n = xs.length()
  let total = for i = 0, sum = 0; i < n; {
    continue i + 1, sum + xs[i]
  }  {
    sum
  }  {
    proof_invariant: 0 <= i && i <= n,
    proof_reasoning: "sum equals the total of xs[0..i).",
  }
  debug_inspect(total, content="10")
}

#Example 2: Maximum Value

We keep a running maximum. The invariant is:

"best is the maximum of elements seen so far."

///|
test "invariant max example" {
  let xs : Array[Int] = [2, 7, 1, 5]
  let n = xs.length()
  let best = for i = 0, best = xs[0]; i < n; {
    let v = xs[i]
    continue i + 1, if v > best { v } else { best }
  }  {
    best
  }  {
    proof_invariant: 0 <= i && i <= n,
    proof_reasoning: "best is max of xs[0..i).",
  }
  debug_inspect(best, content="7")
}

#Example 3: Simple Loop Without Invariants

For very simple loops, a for .. in loop is clearer and needs no invariant.

///|
test "simple loop example" {
  let xs : Array[Int] = [1, 2, 3]
  let sum = for v in xs; sum = 0 {
    continue sum + v
  }  {
    sum
  }
  debug_inspect(sum, content="6")
}

#How to Read a Package

Each algorithm package lives in modules/<domain>/<name>/ and has:

README.mbt.md (the tutorial)
.mbt source files (the implementation)
tests (often inside the README itself)

Each domain module also has a README.md that explains the package family.

If a README feels too advanced, pick an easier package first and return later.

#Suggested Learning Path

Start small and build up:

Basics: modules/data_structures/union_find, modules/data_structures/fenwick, modules/data_structures/segment_tree
Dynamic Programming: modules/dp/dp, modules/math/linear_recurrence
Strings: modules/string/kmp, modules/string/aho_corasick, modules/string/suffix_array
Graphs: modules/graph/dijkstra, modules/graph/bellman_ford, modules/graph/mst
Advanced: modules/graph/centroid, modules/data_structures/linkcut, modules/data_structures/segment_tree_beats

#Running the Code

Run these from the workspace root:

moon check
moon test
moon info
moon fmt
moon run cmd/main

#Contributing

When improving a tutorial:

Keep it beginner-friendly
Add multiple examples
Explain why the algorithm works
Mention complexity and pitfalls

#License

See LICENSE.

Source Files

Site source Report issue Packages Build queue Skills Statistics