Specialization, Feature Typing, Redefinition, and Interpretation

Defines Specialization (preorder), FeatureTyping (substitution lemma), Redefinition (type refinement), Interpretation (model-theoretic semantics), and the soundness theorem.

structure VerifiedMBSE.Core.Specialization : Type

A specializes B iff every instance of A is also an instance of B.

Specialization is a syntactic pair structure carrying only specific and general; chain evidence is kept in the propositional form specializes, not in the structure itself. If a future extension embeds a chain witness into the structure, this note should be updated.

• specific : KerMLType
• general : KerMLType

def VerifiedMBSE.Core.instReprSpecialization.repr : Specialization → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprSpecialization : Repr Specialization

Equations

• VerifiedMBSE.Core.instReprSpecialization = { reprPrec := VerifiedMBSE.Core.instReprSpecialization.repr }

def VerifiedMBSE.Core.Specialization.refl (t : KerMLType) : Specialization

Specialization is reflexive.

Equations

• VerifiedMBSE.Core.Specialization.refl t = { specific := t, general := t }

def VerifiedMBSE.Core.specializes (a b : KerMLType) : Prop

Propositional form of specialization.

Equations

• VerifiedMBSE.Core.specializes a b = ∃ (s : VerifiedMBSE.Core.Specialization), s.specific = a ∧ s.general = b

theorem VerifiedMBSE.Core.specializes_refl (a : KerMLType) : specializes a a

specializes is reflexive.

theorem VerifiedMBSE.Core.specializes_trans {a b c : KerMLType} (_hab : specializes a b) (_hbc : specializes b c) : specializes a c

specializes is transitive.

Because Specialization is a shallow pair carrying no chain witness, the evidence a ≤ c is constructed directly as ⟨⟨a, c⟩, rfl, rfl⟩. The hypotheses hab and hbc are accepted at the API level but not needed in the body; they preserve the signature so a future extension that embeds a chain witness into Specialization can make use of them without changing call sites.

@[implicit_reducible]

instance VerifiedMBSE.Core.instPreorderKerMLType : Preorder KerMLType

Preorder instance.

Equations

• One or more equations did not get rendered due to their size.

structure VerifiedMBSE.Core.FeatureTyping : Type

FeatureTyping assigns a type to a feature, corresponding to the typing judgement f : A.

• feature : Feature

  The feature being typed.

• featureType : KerMLType

  The assigned type.

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprFeatureTyping : Repr FeatureTyping

Equations

• VerifiedMBSE.Core.instReprFeatureTyping = { reprPrec := VerifiedMBSE.Core.instReprFeatureTyping.repr }

def VerifiedMBSE.Core.instReprFeatureTyping.repr : FeatureTyping → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure VerifiedMBSE.Core.TypedFeature : Type

TypedFeature bundles a Feature with a FeatureTyping, together with a consistency proof that the typing refers to the same feature.

• feature : Feature
• typing : FeatureTyping
• wf : self.typing.feature = self.feature

  Consistency: typing refers to the same feature.

def VerifiedMBSE.Core.FeatureTyping.widen (ft : FeatureTyping) (b : KerMLType) : ft.featureType ≤ b → FeatureTyping

Type widening via the substitution lemma (subsumption): A ≤ B, f : A ⊢ f : B.

Equations

• ft.widen b x✝ = { feature := ft.feature, featureType := b }

theorem VerifiedMBSE.Core.FeatureTyping.widen_feature (ft : FeatureTyping) (b : KerMLType) (h : ft.featureType ≤ b) : (ft.widen b h).feature = ft.feature

Widening does not change the feature itself.

theorem VerifiedMBSE.Core.FeatureTyping.widen_type (ft : FeatureTyping) (b : KerMLType) (h : ft.featureType ≤ b) : (ft.widen b h).featureType = b

After widening, the type is the specified b.

theorem VerifiedMBSE.Core.FeatureTyping.widen_trans (ft : FeatureTyping) (b c : KerMLType) (hab : ft.featureType ≤ b) (hbc : b ≤ c) : (ft.widen c ⋯).feature = ((ft.widen b hab).widen c hbc).feature

Widening composes transitively (coherence).

structure VerifiedMBSE.Core.Redefinition : Type

Redefinition of a feature in a subtype context. Requires the refinement condition redefining.featureType ≤ redefined.featureType.

• redefining : FeatureTyping

  Redefining feature (subtype side).

• redefined : FeatureTyping

  Redefined feature (supertype side).

• typeRefinement : self.redefining.featureType ≤ self.redefined.featureType

  Type refinement condition.

def VerifiedMBSE.Core.Redefinition.toWidened (r : Redefinition) : FeatureTyping

Recover a FeatureTyping from a Redefinition via widening.

Equations

• r.toWidened = r.redefining.widen r.redefined.featureType ⋯

theorem VerifiedMBSE.Core.Redefinition.toWidened_type (r : Redefinition) : r.toWidened.featureType = r.redefined.featureType

After widening, the type coincides with redefined's type.

theorem VerifiedMBSE.Core.Redefinition.toWidened_feature (r : Redefinition) : r.toWidened.feature = r.redefining.feature

The feature itself stays as redefining after widening.

def VerifiedMBSE.Core.Redefinition.trans (r₁ r₂ : Redefinition) (h : r₁.redefined.featureType = r₂.redefining.featureType) : Redefinition

Transitivity of Redefinition.

Equations

• r₁.trans r₂ h = { redefining := r₁.redefining, redefined := r₂.redefined, typeRefinement := ⋯ }

def VerifiedMBSE.Core.Interpretation : Type 1

Semantic interpretation: a function assigning a carrier type to each KerMLType. Denotationally, ⟦T⟧_I := I T.

Equations

• VerifiedMBSE.Core.Interpretation = (VerifiedMBSE.Core.KerMLType → Type)

def VerifiedMBSE.Core.extent (I : Interpretation) (T : KerMLType) : Type

Extent of T under the interpretation I.

Equations

• VerifiedMBSE.Core.extent I T = I T

def VerifiedMBSE.Core.semanticSpecializes (I : Interpretation) (a b : KerMLType) : Prop

Semantic specialization: under I, A ≤_sem B iff an injection I A → I B exists.

Equations

• VerifiedMBSE.Core.semanticSpecializes I a b = ∃ (f : I a → I b), Function.Injective f

theorem VerifiedMBSE.Core.semanticSpecializes_refl (I : Interpretation) (a : KerMLType) : semanticSpecializes I a a

Semantic specialization is reflexive.

theorem VerifiedMBSE.Core.semanticSpecializes_trans (I : Interpretation) {a b c : KerMLType} (hab : semanticSpecializes I a b) (hbc : semanticSpecializes I b c) : semanticSpecializes I a c

Semantic specialization is transitive.

theorem VerifiedMBSE.Core.semanticSpecializes_preorder (I : Interpretation) (a b c : KerMLType) : semanticSpecializes I a b → semanticSpecializes I b c → semanticSpecializes I a c

Semantic specialization forms a preorder.

def VerifiedMBSE.Core.trivialInterpretation : Interpretation

Single-point interpretation (trivial model).

Equations

• VerifiedMBSE.Core.trivialInterpretation x✝ = Unit

def VerifiedMBSE.Core.stringInterpretation : Interpretation

String interpretation (for debugging).

Equations

• VerifiedMBSE.Core.stringInterpretation x✝ = String

theorem VerifiedMBSE.Core.trivial_semanticSpecializes_all (a b : KerMLType) : semanticSpecializes trivialInterpretation a b

Under the trivial model, specialization always holds.

def VerifiedMBSE.Core.InterpretationRespects (I : Interpretation) : Prop

I satisfies the model condition: every Specialization is respected semantically.

Equations

• VerifiedMBSE.Core.InterpretationRespects I = ∀ (s : VerifiedMBSE.Core.Specialization), VerifiedMBSE.Core.semanticSpecializes I s.specific s.general

theorem VerifiedMBSE.Core.soundness (I : Interpretation) (hI : InterpretationRespects I) {a b : KerMLType} (hab : specializes a b) : semanticSpecializes I a b

Soundness: syntactic specialization implies semantic specialization.

theorem VerifiedMBSE.Core.trivial_respects : InterpretationRespects trivialInterpretation

The trivial interpretation satisfies the model condition.

theorem VerifiedMBSE.Core.soundness_trivial {a b : KerMLType} (hab : specializes a b) : semanticSpecializes trivialInterpretation a b

Corollary: under the trivial model, syntactic specialization implies semantic specialization.