Property-Based Testing Catalog

This document lists the algorithmic invariants (hypotheses) verified by Yog's property-based testing suite. We use StreamData to generate thousands of random graph structures to ensure these properties hold across all possible edge cases, including sparse, dense, disconnected, and cyclic graphs.

Location: All property-based tests are in test/yog/pbt/.

Connectivity and Components

File: test/yog/pbt/component_test.exs

• SCC Partitioning: Strongly Connected Components must partition the set of all nodes exactly. Every node belongs to one and only one SCC.
• MST Algorithm Agreement: Kruskal and Prim algorithms must produce the same total weight for connected undirected graphs.

File: test/yog/pbt/k_core_test.exs

• k-core Degree: Every node in a $k$-core must have degree at least $k$ within that subgraph.
• Core Number Consistency: A node with core number $k$ must exist in the $k$-core but not in the $(k+1)$-core.
• Complete Graph Core: A complete graph $K_n$ has a $(n-1)$-core containing all nodes.

File: test/yog/pbt/bipartite_test.exs

• Bipartite Verification: Graphs identified as bipartite must be 2-colorable with no monochromatic edges.
• Matching Bound: Maximum matching size cannot exceed the minimum partition size.

File: test/yog/pbt/clique_test.exs

• Disjoint Cliques: Generated disjoint cliques produce the expected number of maximal cliques.

Pathfinding and Flow

File: test/yog/pbt/pathfinding_test.exs

• Dijkstra-BFS Agreement: Dijkstra agrees with BFS on the shortest path distance for unweighted graphs.
• Algorithm Consistency: Dijkstra, Bellman-Ford, and A* (with zero heuristic) must agree on shortest path weights for non-negative weights.
• Negative Cycle Detection: Bellman-Ford correctly identifies graphs containing reachable negative cycles.
• Bidirectional Correctness: Bidirectional Dijkstra yields the same path distance as standard Dijkstra.
• Floyd-Warshall Agreement: Floyd-Warshall agrees with repeated Dijkstra runs for all-pairs shortest paths.
• All-Pairs Unweighted Self-Distances: Self-distances are always zero.
• All-Pairs Unweighted Symmetry: Distances are symmetric in undirected graphs.
• All-Pairs Unweighted Triangle Inequality: $d(a,c) \leq d(a,b) + d(b,c)$ for all reachable triples.
• All-Pairs Unweighted BFS Consistency: All-pairs results match single-source BFS distances.
• All-Pairs Unweighted Floyd-Warshall Consistency: All-pairs results match Floyd-Warshall on unit weights.
• All-Pairs Reachability Transitivity: If $a$ reaches $b$ and $b$ reaches $c$, then $a$ reaches $c$.

File: test/yog/pbt/flow_test.exs

• Max-Flow Min-Cut Theorem: The maximum flow value equals the minimum cut capacity.
• Flow Conservation: At every node except source and sink, total in-flow equals total out-flow.
• Integrality: Integer capacities yield integer max flow.
• Residual Graph Termination: After max flow, no augmenting path exists in the residual graph.
• Zero Flow on Disconnected: Max flow is zero between disconnected components.

Centrality Measures

File: test/yog/pbt/centrality_test.exs

• Star Graph Centrality: In a star graph, the center node has strictly higher centrality (Degree, Closeness, Betweenness, PageRank, Eigenvector) than any leaf node.
• PageRank Unity: The sum of PageRank scores across all nodes equals exactly 1.0.

Graph Operations

File: test/yog/pbt/operation_test.exs

• Union: Union contains all nodes and edges from both graphs.
• Intersection Idempotence: Intersection of a graph with itself equals the graph.
• Difference Annihilation: Difference of a graph with itself is empty.
• Disjoint Union Re-indexing: Disjoint union correctly re-indexes to avoid collisions.
• Isomorphism Reflexivity: A graph is isomorphic to itself.
• Power Identity: Power of a graph to 1 equals the graph.
• Cartesian Product Order: Node count equals product of operand node counts.
• Subgraph Reflexivity: Subgraph relation is reflexive.
• Symmetric Difference Commutativity: Symmetric difference is commutative.
• Symmetric Difference Exclusivity: Resulting edges are in exactly one input graph.
• Line Graph Node Count: Equals edge count of original graph.
• Line Graph Edge Count: Matches theoretical formula for undirected and directed graphs.

File: test/yog/pbt/transform_test.exs

• Transpose Involutivity: transpose(transpose(G)) == G.
• Map-Nodes Identity: map_nodes(G, id) == G.
• Map-Nodes Composition: map(f) . map(g) == map(g . f).
• Map-Nodes Topology Preservation: Node and edge counts are preserved.
• Map-Edges Identity: map_edges(G, id) == G.
• Filter-Nodes Consistency: Filtering removes associated edges and preserves remaining structure.
• Merge Idempotence: merge(G, G) == G.
• Subgraph Invariants: All edges connect nodes within the subset.
• Filter-Edges Consistency: Node count preserved, edge count non-increasing.
• Complement Invariants: Same nodes, complement of complement (minus self-loops) equals original.
• To-Directed/Undirected Invariants: Type conversion preserves node counts.
• Contract Node Reduction: Contracting two distinct nodes reduces count by 1.
• Transitive Closure/Reduction Round-trip: reduction(closure(G)) == G for transitively reduced DAGs.
• Transitive Closure Idempotence: closure(reduction(G)) == closure(G).
• Transitive Reduction Idempotence: reduction(closure(G)) == reduction(G).

Traversal

File: test/yog/pbt/traversal_test.exs

• BFS Uniqueness: BFS visits each reachable node exactly once.
• DFS-BFS Node Agreement: DFS and BFS visit the same set of reachable nodes.
• Find-Path Connectivity: Found paths are valid (connected edges) when target is reachable.
• Implicit-Explicit DFS Agreement: Implicit and explicit DFS visit the same nodes.
• Topological Order: For any edge $(u,v)$ in a DAG, $u$ appears before $v$ in topological sort.
• Cyclicity Consistency: A graph is either cyclic or acyclic (exclusive or).

Minimum Spanning Tree

File: test/yog/pbt/mst_test.exs

• Kruskal-Prim Agreement: Both algorithms produce the same total weight.
• MST Edge Count: Equals $V - c$ where $c$ is the number of connected components.
• MST Cycle-Free: No duplicate undirected edges in the result.
• MST Non-Negative: Total weight is non-negative for non-negative input weights.
• MST of Tree: The MST of a tree is the tree itself.

Structural Properties

File: test/yog/pbt/structural_test.exs

• Transpose Involutivity: transpose(transpose(G)) == G.
• Undirected Symmetry: All edges have reverse counterparts.
• Edge Count Consistency: Yog.edge_count/1 matches length(Yog.all_edges/1).
• To-Undirected Symmetry: Creates symmetric edge structure.

File: test/yog/pbt/structure_test.exs

• Tree Characterization: Generated trees are connected, acyclic, and have exactly $V-1$ edges.
• Arborescence Validity: Directed trees have a unique root with in-degree 0, others in-degree 1.
• Complete Graph: $K_n$ is complete and $(n-1)$-regular.

File: test/yog/pbt/cyclicity_test.exs

• DAG Generation: Numeric-order edge generation produces acyclic graphs.

Eulerian Paths

File: test/yog/pbt/eulerian_test.exs

• Circuit Consistency: has_eulerian_circuit? agrees with eulerian_circuit result.
• Circuit Closure: Eulerian circuits start and end at the same node.
• Path Consistency: has_eulerian_path? agrees with eulerian_path result.

Community Detection

File: test/yog/pbt/community_test.exs

• Partitioning Coverage: All nodes are assigned to exactly one community.
• Community ID Consistency: Number of communities matches unique assignment IDs.
• Disjoint Component Separation: Communities from different disconnected components are not merged.
• Local Community Contains Seed: Local community detection always includes the seed node.

Data Structures

File: test/yog/pbt/disjoint_set_test.exs

• Reflexivity: Every element is connected to itself.
• Symmetry: Connectedness is bidirectional.
• Transitivity: If $x$ is connected to $y$ and $y$ to $z$, then $x$ is connected to $z$.
• Union Set Count: Union reduces set count by 1 for distinct sets, 0 for same set.
• Partitioning Coverage: to_lists produces disjoint sets covering all elements.

File: test/yog/pbt/priority_queue_test.exs

• Heap Ordering: Popping all elements returns a sorted list.
• Custom Comparison: Works with custom comparators (max-heap).
• Peek-Pop Agreement: peek returns the same as first pop.
• Size Invariant: Push/pop accurately track element count.
• Merge Order: Merging preserves overall sorted order.

Graph Generators

File: test/yog/pbt/generator_test.exs

Classic Generators

• Complete Graph: complete(n) has $n$ nodes, $n(n-1)/2$ edges, degree $n-1$.
• Cycle Graph: cycle(n) has $n$ nodes, $n$ edges, degree 2.
• Path Graph: path(n) has $n$ nodes, $\max(0, n-1)$ edges.
• Star Graph: star(n) has $n$ nodes, $n-1$ edges, center degree $n-1$.
• Wheel Graph: wheel(n) has $n$ nodes, $2(n-1)$ edges.
• Binary Tree: binary_tree(d) has $2^{d+1}-1$ nodes, $2^{d+1}-2$ edges.
• Petersen Graph: Has exactly 10 nodes, 15 edges, degree 3.
• Empty Graph: empty(n) has $n$ nodes, 0 edges.
• Grid 2D: grid_2d(r,c) has $r \times c$ nodes, $(r-1)c + r(c-1)$ edges.
• Complete Bipartite: complete_bipartite(m,n) has $m+n$ nodes, $m \times n$ edges.
• Hypercube: hypercube(n) has $2^n$ nodes, $n \cdot 2^{n-1}$ edges, degree $n$.
• Ladder Graph: ladder(n) has $2n$ nodes, $3n-2$ edges.

Random Generators

• Erdős-Rényi GNP: erdos_renyi_gnp(n,p) has exactly $n$ nodes.
• Erdős-Rényi GNM: erdos_renyi_gnm(n,m) has exactly $n$ nodes, at most $m$ edges.
• Random Tree: random_tree(n) has $n$ nodes, $n-1$ edges.
• Random Regular: random_regular(n,d) has $n$ nodes, $nd/2$ edges, degree $d$.
• Seed Reproducibility: Same seed produces identical graphs.
• SBM Node Count: Stochastic Block Model has exactly $n$ nodes.
• SBM Community Validity: Community assignments are in valid range $[0, k)$.

Graph Health Metrics

File: test/yog/pbt/health_test.exs

Distance Metrics

• Path Diameter: Diameter of $P_n$ is $n-1$.
• Path Radius: Radius of $P_n$ is $\lfloor n/2 \rfloor$.
• Cycle Diameter: Diameter of $C_n$ is $\lfloor n/2 \rfloor$.
• Complete Graph Diameter: Diameter and radius of $K_n$ are both 1.
• Complete Graph Eccentricity: All nodes have eccentricity 1 in $K_n$.

Assortativity

• Regular Graph Assortativity: Regular graphs have assortativity 0.0.
• Star Graph Assortativity: Star graphs have negative assortativity.

Average Path Length

• Complete Graph APL: Average path length of $K_n$ is 1.0.
• Star Graph APL: Average path length of $S_n$ is $2 - 2/n$.
• Disconnected APL: Disconnected graphs have nil APL.

I/O Roundtrip

File: test/yog/pbt/io_test.exs

• TGF Roundtrip: Serialize then parse preserves node and edge counts.
• JSON Roundtrip: Serialize then parse preserves graph structure.
• Pajek Roundtrip: Serialize then parse preserves node and edge counts.

Test Summary

• Total PBT Files: 21
• Total Properties: 145+
• Test Location: test/yog/pbt/

File Listing