-
Notifications
You must be signed in to change notification settings - Fork 0
Description
Description
TraceabilityLink is the only core domain entity without any JML contracts. Both Requirement and RequirementRelation have JML class invariants and method contracts, but TraceabilityLink has none.
This is inconsistent with the project's formal methods strategy (ADR-012, CODING_STANDARDS.md) which calls for JML contracts on state transitions and data integrity boundaries. TraceabilityLink handles external artifact references where silent corruption (wrong artifact type, null identifiers) would be difficult to diagnose.
Recommendation: Add JML class invariants for required field non-nullity and method contracts on the constructor and any future domain methods.
Location: TraceabilityLink.java
Traced Requirements
- GC-E001: Universal Artifact Linking
- GC-E002: Typed Link Semantics
Impact
Formal methods consistency — gap in contract coverage on a core entity.