Repository navigation
fix(check): warn on a feature value whose type is unrelated to the feature's own type - #1621
Merged
Merged
Conversation
…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>
Contributor
Author
|
I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".
|
… and compliance map Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…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>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What and why
A feature value implies a binding of the feature to the value's result, and KerML's
validateBindingConnectorTypeConformanceasks 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 withattribute def R :> Real;the valueattribute a : R = 5;read as "Integer conforms to Real" and stayed silent, while the pilot warns at the feature: Integer does not specializeRandRdoes 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-typeswarning (Bound features should have conforming types) at the feature, where the pilot reports it. Of the reproducer this came from:attribute a1 : R = 5;andpart p : P { attribute :>> x = 5; }(the featurex : Rinherited through the redefinition) now warn, at the usage and at the redefining member.R = 5.0stays silent: aLiteralRationalspecializesPerformances::literalRationalEvaluations(KerML 1.1 §8.3.4.8.13checkLiteralRationalSpecialization), whoseLiteralRationalEvaluationdeclaresreturn : Real[1], andRspecializesReal. 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 6stay silent: anOperatorExpressioninstantiates the Kernel Function Library function its operator names, inBaseFunctions,DataFunctions,ControlFunctionsorder (§8.3.4.8.17instantiatedType), so-5isDataFunctions::'-''sDataValueresult,5 [m]BaseFunctions::'[''sAnything, 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 refusedattribute t : DurationUnit = s * s / s;where the pilot does not.R default 5stays silent: aFeatureValuewithisDefault = trueimplies no binding connector (§8.3.4.9checkFeatureValueBindingConnector, "If a FeatureValue has isDefault = true, then no BindingConnector is required"); an initial value (:=) implies one and is judged.Integer = 5.5andString = 5stay the type checker'sbinding-connector-type-conformanceerror alone: a value the checker already rejects is not warned on a second time.R = a11(anR),R = a13(aReal),Real = 5,Pct = 0.5,Boolean = 5 > 3,N = 5forN :> Naturalstay silent — one side specializes the other.The same judgment covers a metadata body declaration restating a feature (
@M { x = 5; }overx : R) and the constraint anassume/requiremember owns (require constraint c = n;), which the pilot warns on at the declaration. Unknown types, collection values, features typed by aCollectionorElement, subjects (judged byW9CBoundFeatureTypesPassalready) and assignments are not judged.Four existing test fixtures declared untyped
attributes orparts valued by anItemconstructor, an expression body or anIntegercalculation (attribute q = new Telemetry(…),attribute v = { … },part n = Count(…)); the pinned pilot warns on each of those bindings too (an attribute is implicitly aDataValue, a part aPart), 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;overenum def Grade :> Realmoved 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 itsMust reference an actionerror, as in the pilot.Specification basis
KerML 1.1 §8.3.4.5.2
validateBindingConnectorTypeConformance, applied to the binding §8.3.4.9checkFeatureValueBindingConnectorimplies; result typing by §8.3.4.8.13 and §8.3.4.8.17. ThevalidateBindingConnectorTypeConformancerow ofdocs/project/validation-constraints.md(viaconstraint-manifest.json) and a new feature-value row ofdocs/project/spec-compliance.mdrecord 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
TestW9CFeatureValueBindingConformancepins the reproducer line for line at the pilot's line:column plus the pilot-verified extra shapes above;TestW9CFeatureValueBindingOfBodyAndOwnedDeclarationsthe metadata-body and owned-constraint forms. The census probevalidateBindingConnectorTypeConformance.value.sysmlholds 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 -validateoverexamples/(own models, training, the three pilot corpora, spec examples) andtests/testdataon 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 -checkreproduces 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 testandmake lintpass locallychanges/unreleased/<slug>.<section>.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (compliance rows need nothing: the census is counted at docs build)F4,K5) in the body, docs, or changelogLink 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