KerML Core Layer: Dependent Type Semantics

Defines the KerML core layer structures (Element, Type, Feature, Direction) and direction conjugation as an involution.

References

• OMG KerML Specification v2.0 Beta (formal/2023-06-03), Part III
• Almeida et al., "An Analysis of the Semantic Foundation of KerML and SysML v2" (ER 2024)

structure VerifiedMBSE.Core.Element : Type

KerML Element: root of all model elements.

• name : Option String

def VerifiedMBSE.Core.instReprElement.repr : Element → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprElement : Repr Element

Equations

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

def VerifiedMBSE.Core.instBEqElement.beq : Element → Element → Bool

Equations

• VerifiedMBSE.Core.instBEqElement.beq { name := a } { name := b } = (a == b)
• VerifiedMBSE.Core.instBEqElement.beq x✝¹ x✝ = false

@[implicit_reducible]

instance VerifiedMBSE.Core.instBEqElement : BEq Element

Equations

• VerifiedMBSE.Core.instBEqElement = { beq := VerifiedMBSE.Core.instBEqElement.beq }

structure VerifiedMBSE.Core.KerMLTypeextends VerifiedMBSE.Core.Element : Type

KerML Type: classifier that may own features. Semantically represents a set of instances (extent).

• name : Option String
• isAbstract : Bool

  Whether it is abstract (cannot be directly instantiated)

def VerifiedMBSE.Core.instReprKerMLType.repr : KerMLType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprKerMLType : Repr KerMLType

Equations

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

structure VerifiedMBSE.Core.Featureextends VerifiedMBSE.Core.Element : Type

Feature: characteristic of a type (named, multiplicity-bearing slot). In dependent type theory, corresponds to a projection of Σ(x:A).B(x).

• name : Option String
• lower : ℕ

  Multiplicity lower bound

• upper : ℕ

  Multiplicity upper bound (0 = unbounded)

def VerifiedMBSE.Core.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprFeature : Repr Feature

Equations

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

inductive VerifiedMBSE.Core.Direction : Type

Feature Direction (KerML spec §8.4.4). Corresponds to polarity in linear logic: in = negative, out = positive.

• in_ : Direction
• out : Direction
• inout : Direction

def VerifiedMBSE.Core.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprDirection : Repr Direction

Equations

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

def VerifiedMBSE.Core.instBEqDirection.beq : Direction → Direction → Bool

Equations

• VerifiedMBSE.Core.instBEqDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.Core.instBEqDirection : BEq Direction

Equations

• VerifiedMBSE.Core.instBEqDirection = { beq := VerifiedMBSE.Core.instBEqDirection.beq }

def VerifiedMBSE.Core.Direction.conj : Direction → Direction

Direction inversion via conjugation. Corresponds to negation A⊥ in linear logic.

Equations

• VerifiedMBSE.Core.Direction.in_.conj = VerifiedMBSE.Core.Direction.out
• VerifiedMBSE.Core.Direction.out.conj = VerifiedMBSE.Core.Direction.in_
• VerifiedMBSE.Core.Direction.inout.conj = VerifiedMBSE.Core.Direction.inout

theorem VerifiedMBSE.Core.Direction.conj_involution (d : Direction) : d.conj.conj = d

Direction conjugation is an involution: conj(conj(d)) = d

structure VerifiedMBSE.Core.DirectedFeatureextends VerifiedMBSE.Core.Feature : Type

Directed feature: the basic unit of port definitions.

• name : Option String
• lower : ℕ
• upper : ℕ
• direction : Direction

def VerifiedMBSE.Core.instReprDirectedFeature.repr : DirectedFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprDirectedFeature : Repr DirectedFeature

Equations

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

def VerifiedMBSE.Core.DirectedFeature.conj (f : DirectedFeature) : DirectedFeature

DirectedFeature conjugation: inverts only the direction, preserving the body.

Equations

• f.conj = { toFeature := f.toFeature, direction := f.direction.conj }

theorem VerifiedMBSE.Core.DirectedFeature.conj_involution (f : DirectedFeature) : f.conj.conj = f

DirectedFeature conjugation is also an involution.