Contract Coverage

Contract coverage measures how much of a declared contract is actually tested. Unlike code coverage, which measures lines executed, contract coverage measures clauses exercised — the invariants, required semantics, and forbidden behaviors that have corresponding tests.

Coverage ensures contracts are not merely documentation but are enforced.

How It Works

Each contract clause can declare expected test tags via the test_tags field:

[[invariants]]
id = "inv-001"
description = "A key set with a value must return that value on get"
severity = "required"

[[required_semantics]]
id = "req-001"
description = "get(key) returns None for missing keys"
test_tags = ["conformance.value_retrieval"]

[[required_semantics]]
id = "req-002"
description = "delete is idempotent for missing keys"
test_tags = ["conformance.delete_behavior"]

Lexicon scans your test files for tags, matches them against the declared test_tags, and computes:

• clauses tested — contract elements with at least one matching test tag
• clauses missing tests — contract elements with tags but no matching tests
• coverage percentage — covered clauses / total clauses with tags

Clauses that do not declare any test_tags are excluded from the denominator. This means coverage percentage reflects how well you have tested the clauses you intended to test, not every clause in the contract.

Supported Tag Formats

Lexicon recognizes three ways to tag tests:

Attribute tag

#[lexicon_tag("conformance.value_retrieval")]
#[test]
fn test_get_returns_value() {
    // ...
}

Function call tag

#[test]
fn test_delete_behavior() {
    lexicon::tags("conformance.delete_behavior", "edge-case");
    // ...
}

Comment tag

conformance.value_retrieval

#[test]
fn test_retrieval() {
    // ...
}

All three formats are detected by the coverage scanner when it walks .rs files in the project. You can mix formats freely — a single test file can use attributes, function calls, and comments.

Coverage Report

A typical coverage report looks like:

Contract Coverage Report

Contract: key-value-store

Clauses: 12
Covered: 9
Missing coverage: 3

Missing clauses:

- concurrent_write_behavior
- serialization_roundtrip
- large_key_handling

This report is integrated into the verification pipeline and surfaces in lexicon verify. Use the COVERAGE_REPORT action in lexicon chat for a detailed interactive view.

Scoring Integration

Contract coverage influences the scoring model. The conformance-coverage dimension measures how thoroughly your tests exercise your contracts.

Full coverage earns full points. Gaps reduce the score proportionally. This makes coverage a concrete, measurable dimension of system health rather than an aspirational goal.

Why Contract Coverage Matters

Code coverage tells you what lines ran. Contract coverage tells you what behaviors are proven. A system can have 100% code coverage but 30% contract coverage if the tests exercise code paths without actually verifying the declared invariants.

Contract coverage closes this gap. It connects the behavioral specification (what the system must do) to the test suite (what the tests actually check).