Skip to content

fix(check): warn on a feature value whose type is unrelated to the feature's own type - #1621

Merged
HuiJun merged 6 commits into
developfrom
fix/feature-value-binding-conformance
Oct 28, 2026
Merged

HuiJun merged 6 commits into
developfrom
fix/feature-value-binding-conformance

Conversation

@devin-ai-integration

@devin-ai-integration devin-ai-integration Bot commented Oct 28, 2026 •

Copy link
Copy Markdown
Contributor

What and why

A feature value implies a binding of the feature to the value's result, and KerML's validateBindingConnectorTypeConformance asks the two bound features to have conforming types: one side's type must specialize the other's. The type checker judged a scalar value against the scalar ancestor of the feature's declared type, so with attribute def R :> Real; the value attribute a : R = 5; read as "Integer conforms to Real" and stayed silent, while the pilot warns at the feature: Integer does not specialize R and R does not specialize Integer.

The value's declared result type is now judged against the feature's own types, symmetrically, and reported as the existing bound-feature-types warning (Bound features should have conforming types) at the feature, where the pilot reports it. Of the reproducer this came from:

  • attribute a1 : R = 5; and part p : P { attribute :>> x = 5; } (the feature x : R inherited through the redefinition) now warn, at the usage and at the redefining member.
  • R = 5.0 stays silent: a LiteralRational specializes Performances::literalRationalEvaluations (KerML 1.1 §8.3.4.8.13 checkLiteralRationalSpecialization), whose LiteralRationalEvaluation declares return : Real[1], and R specializes Real. The pilot types the literal the same way (ImplicitGeneralizationMap: LiteralRationalImpl → Performances::literalRationalEvaluations), so there is no spec/pilot deviation to record.
  • R = -5, R = 2 + 3, R = b + 1, LengthValue = 5 [m], R = if … ? 5 else 6 stay silent: an OperatorExpression instantiates the Kernel Function Library function its operator names, in BaseFunctions, DataFunctions, ControlFunctions order (§8.3.4.8.17 instantiatedType), so -5 is DataFunctions::'-''s DataValue result, 5 [m] BaseFunctions::'[''s Anything, which every attribute type specializes. The judgment reads those declared results (and a behavior invocation's declared result parameter) rather than the checker's refined static types, which would have refused attribute t : DurationUnit = s * s / s; where the pilot does not.
  • R default 5 stays silent: a FeatureValue with isDefault = true implies no binding connector (§8.3.4.9 checkFeatureValueBindingConnector, "If a FeatureValue has isDefault = true, then no BindingConnector is required"); an initial value (:=) implies one and is judged.
  • Integer = 5.5 and String = 5 stay the type checker's binding-connector-type-conformance error alone: a value the checker already rejects is not warned on a second time.
  • R = a11 (an R), R = a13 (a Real), Real = 5, Pct = 0.5, Boolean = 5 > 3, N = 5 for N :> Natural stay silent — one side specializes the other.

The same judgment covers a metadata body declaration restating a feature (@M { x = 5; } over x : R) and the constraint an assume/require member owns (require constraint c = n;), which the pilot warns on at the declaration. Unknown types, collection values, features typed by a Collection or Element, subjects (judged by W9CBoundFeatureTypesPass already) and assignments are not judged.

Four existing test fixtures declared untyped attributes or parts valued by an Item constructor, an expression body or an Integer calculation (attribute q = new Telemetry(…), attribute v = { … }, part n = Count(…)); the pinned pilot warns on each of those bindings too (an attribute is implicitly a DataValue, a part a Part), so the incidental declarations were changed to the kind the value has (item, calc, attribute) and their assertions are unchanged. attribute g : L::Grade = 4; over enum def Grade :> Real moved from "silent" to "warns": the constant 4 still equals the enumerated 4.0, but Integer and Grade are unrelated types, and the pilot warns on it; action call = tag(3) naming a calculation now carries the binding warning beside its Must reference an action error, as in the pilot.

Specification basis

KerML 1.1 §8.3.4.5.2 validateBindingConnectorTypeConformance, applied to the binding §8.3.4.9 checkFeatureValueBindingConnector implies; result typing by §8.3.4.8.13 and §8.3.4.8.17. The validateBindingConnectorTypeConformance row of docs/project/validation-constraints.md (via constraint-manifest.json) and a new feature-value row of docs/project/spec-compliance.md record the rule; the census row stays approximate for its error severity on unrelated primitive kinds, so no gap-register entry is needed.

How it was verified

  • TestW9CFeatureValueBindingConformance pins the reproducer line for line at the pilot's line:column plus the pilot-verified extra shapes above; TestW9CFeatureValueBindingOfBodyAndOwnedDeclarations the metadata-body and owned-constraint forms. The census probe validateBindingConnectorTypeConformance.value.sysml holds the plain and redefinition forms; the pinned pilot (release 2026-09, 0.63.0 — and 2026-08 before it) reports both at the same positions.
  • ./bin/sysml -validate over examples/ (own models, training, the three pilot corpora, spec examples) and tests/testdata on develop and on this branch: zero diagnostics moved on any root (training 305, pilot KerML 16, pilot SysML 413, pilot validation 67, spec examples 1094, tests/testdata 92, own examples 11), so the training corpus stays clean and the pilot differential records no row movement (pilot-diff -check reproduces the committed baseline: 921 files, 518 fully agreeing).
  • gofmt -l . empty, go vet ./..., make lint, go test -race ./... -timeout 40m, go test -C tools ./... -timeout 40m, the three corpus gates with their require variables, pilot-diff -check, pilot-reject -check (349 cases, 339 both reject, 10 only ours, unchanged), pilot-xpect -check (1299 agree / 30 disagree, unchanged), validation-census -check, make docs-counts, python3 scripts/changelog.py check.

Checklist

  • make test and make lint pass locally
  • Tests added or updated for the change
  • Documentation extended where it already covers the surface (see CONTRIBUTING.md)
  • Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
  • baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
  • No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/628e8312906c45b39833f621fdee4eb3
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/628e8312906c45b39833f621fdee4eb3?variant=devin
Requested by: @HuiJun

…ature's own type

A feature value implies a binding of the feature to the value's result
(KerML 1.1 §8.3.4.5.2 validateBindingConnectorTypeConformance). The type
checker judged a scalar value against the scalar ancestor of the feature's
declared type, so an Integer literal bound to a user `attribute def R :> Real`
read as conforming to Real and stayed silent where the pilot warns: Integer
and R specialize neither the other. The value's declared result type is now
judged against the feature's own types, symmetrically, and reported as the
`bound-feature-types` warning at the feature; a value the lattice already
rejects, a `default`, a collection value or a Collection/Element-typed
feature stay as they were.

Co-Authored-By: jason.han <hanhuijun@gmail.com>
@devin-ai-integration

Copy link
Copy Markdown
Contributor Author

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

  • Disable automatic comment, CI, and merge conflict monitoring

devin-ai-integration Bot and others added 2 commits October 28, 2026 03:29
… and compliance map

Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
devin-ai-integration[bot]

This comment was marked as resolved.

…d an owned constraint

A metadata body declaration restating a feature (`@M { x = 5; }`) and the
constraint an `assume`/`require` member owns bind their values as any feature
value does, and the pilot warns on each at the declaration; both took paths
the new judgment did not reach.

Co-Authored-By: jason.han <hanhuijun@gmail.com>
devin-ai-integration[bot]

This comment was marked as resolved.

Co-Authored-By: jason.han <hanhuijun@gmail.com>
@devin-ai-integration
devin-ai-integration Bot marked this pull request as ready for review October 28, 2026 07:00
devin-ai-integration[bot]

This comment was marked as resolved.

Co-Authored-By: jason.han <hanhuijun@gmail.com>
@HuiJun
HuiJun merged commit 532f3c3 into develop Oct 28, 2026
30 checks passed
@HuiJun
HuiJun deleted the fix/feature-value-binding-conformance branch October 28, 2026 13:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant