Validation
The compiler validates .ddd files before generating code. All checks operate on the AST — they are platform-independent and apply regardless of the code generation target. If the compiler accepts a .ddd file, the stated properties hold and the generated code is structurally sound.
Unknown = error. The compiler never silently succeeds when it cannot verify.
Check Summary
| Check | Page |
|---|---|
| Exhaustiveness | Completeness |
| Evolve totality | Completeness |
| Terminal state enforcement | Completeness |
| Guard consistency | Guards |
require false deprecation | Guards |
| Postcondition derivability | Guards |
| Initial state completeness | Structural |
| Dead code detection | Structural |
Terminal states (marked terminal(State) = true) are excluded from both exhaustiveness and evolve totality checks — they are absorbing states that reject all commands and have no outgoing transitions.
Error Format
All validation errors include:
- Source position (
file:line:column) - Human-readable error message
- Actionable fix suggestion
Unresolved References
Validation checks skip AST nodes with unresolved cross-references. Langium’s linking phase independently reports reference errors — validation defers structural checks until all references are resolved. This prevents duplicate diagnostics and crashes on partial ASTs during error recovery.
Architecture Decisions
- ADR-004: Two-level verification architecture
- ADR-006: Guard analysis via Galois connection
- ADR-007: Validation error accumulation via applicative functor
- ADR-010: Unknown equals error — strict verification
- ADR-012: Skip semantic validation on unresolved references
- ADR-015: Abstract interpretation for guard satisfiability
- ADR-016: Rejection category keywords