counterexample-explainer

Counterexample Explainer

Overview

Analyze counterexamples that violate specifications and produce clear, structured explanations showing step-by-step how and why the violation occurs, with root cause analysis and impact assessment.

Workflow

1. Understand the Specification

Identify what property is being checked.

Questions to ask:

• What is the specification or requirement?
• Is it formal (invariant, temporal logic) or informal (requirement doc)?
• What should happen vs what actually happened?
• Is this from a test failure, model checker, or runtime error?

See specification-types.md for comprehensive specification catalog.

Common specification types:

Formal specifications:

• Invariants: balance >= 0
• Temporal logic: G(request → F grant)
• Pre/postconditions: @requires(x > 0), @ensures(result >= 0)
• State machines: Valid state transitions
• Concurrency: Atomicity, deadlock freedom

Informal requirements:

• User stories with acceptance criteria
• Functional requirements
• API contracts
• Expected behavior descriptions

Test specifications:

• Assertions: assert result == expected
• Property-based tests
• Integration test expectations

2. Collect Counterexample Information

Gather all relevant data about the violation.

From test failures:

# Run test to get failure details
pytest test_file.py::test_name -v

# Get stack trace
pytest test_file.py::test_name -v --tb=long

# Get variable values at failure
pytest test_file.py::test_name -v -l

Information to extract:

• Input values that triggered failure
• Expected output/behavior
• Actual output/behavior
• Intermediate state changes
• Stack trace or execution path
• Error messages

From runtime violations:

# Assertion failure
AssertionError: balance must be non-negative
  File "account.py", line 45
  assert self.balance >= 0

# Extract:
# - Variable: self.balance
# - Expected: >= 0
# - Actual: (check value)