VColumn: A Single Column of the V-Matrix

サブシステム識別子、VColumn 構造体、レイヤフィルタ、 および Complete 述語を定義する。

structure VerifiedMBSE.Matrix.VColumn : Type

VColumn: 1 サブシステムに対応する V 行列の列。 subsystem はドメイン固有の enum 化を避けるため String で持つ。

• subsystem : String
• records : List VV.VVRecord

def VerifiedMBSE.Matrix.VColumn.atLayer (col : VColumn) (l : VV.Layer) : List VV.VVRecord

特定レイヤの VVRecord を取得する。

Equations

• col.atLayer l = List.filter (fun (r : VerifiedMBSE.VV.VVRecord) => r.layer == l) col.records

def VerifiedMBSE.Matrix.VColumn.hasLayer (col : VColumn) (l : VV.Layer) : Bool

列が特定レイヤに VVRecord を持つか。

Equations

• col.hasLayer l = !(col.atLayer l).isEmpty

def VerifiedMBSE.Matrix.VColumn.allLayersCovered (col : VColumn) : Bool

全レイヤ（system/subsystem/component）を埋めているか。

Equations

• col.allLayersCovered = (col.hasLayer VerifiedMBSE.VV.Layer.system && col.hasLayer VerifiedMBSE.VV.Layer.subsystem && col.hasLayer VerifiedMBSE.VV.Layer.component)

def VerifiedMBSE.Matrix.VColumn.Complete (col : VColumn) : Prop

列の完全性: 各レイヤに少なくとも 1 件の VVRecord が存在する。

Equations

• col.Complete = ((col.atLayer VerifiedMBSE.VV.Layer.system).length > 0 ∧ (col.atLayer VerifiedMBSE.VV.Layer.subsystem).length > 0 ∧ (col.atLayer VerifiedMBSE.VV.Layer.component).length > 0)

def VerifiedMBSE.Matrix.VColumn.fullyTrusted (col : VColumn) : Bool

列のすべてのレコードが .trusted であるか（構造子判別）。

旧実装は currentLevel == 1.0 の Float 等号に依存していたが、IEEE 754 の 等号比較は推奨されないため、ValidationTrace.isTrusted の inductive 判別に 置き換えた（F2）。.trusted 以外の混在があれば false を返す。

Equations

• col.fullyTrusted = col.records.all fun (r : VerifiedMBSE.VV.VVRecord) => r.validation.isTrusted

def VerifiedMBSE.Matrix.VColumn.merge (c1 c2 : VColumn) : c1.subsystem = c2.subsystem → VColumn

VColumn の合成: 同一サブシステムの列をマージする。

Equations

• c1.merge c2 x✝ = { subsystem := c1.subsystem, records := c1.records ++ c2.records }