Allium

Allium は、ソフトウェアの動作をドメインレベルで捉えるための形式言語です。非形式的な機能説明と実装の間に位置し、ソフトウェアが何をするのかを正確に指定する方法を提供します。実装方法については指示しません。

この名前は、タマネギとシャロットを含む植物科に由来しており、Cucumber と Gherkin が確立した動作指定ツール業界の伝統を引き継いでいます。

主要な原則：

• 観察可能な動作を説明し、実装ではなく
• 動作レベルで重要なドメインロジックをキャプチャ
• 統合テストとエンドツーエンドテストを生成（ユニットテストではない）
• 実装前に曖昧性を明確にする
• 実装非依存：同じ仕様をどの言語でも実装できる

Allium は、プログラミング言語またはフレームワークの選択、データベーススキーマまたはストレージメカニズム、API設計またはUIレイアウト、内部アルゴリズム（ドメインレベルの関心事でない限り）を指定しません。

ルーティングテーブル

タスク	ツール	使用時
.allium ファイルの作成または読み込み	このスキル	言語構文と構造が必要
会話を通じた仕様構築	elicit スキル	ユーザーが構築したい機能または動作を説明
既存コードからの仕様抽出	distill スキル	ユーザーが実装コードを持ち、そこから仕様を抽出したい
既存仕様の修正	tend スキル	ユーザーが .allium ファイルへの対象変更を希望
仕様とコード間の一貫性確認	weed スキル	ユーザーが仕様と実装の乖離を見つけるまたは修正したい
仕様からのテスト生成	propagate スキル	ユーザーが仕様からテスト、PBT プロパティ、または状態機械テストを生成したい

クイック構文サマリー

エンティティ

entity Candidacy {
    -- Fields
    candidate: Candidate
    role: Role
    status: pending | active | completed | cancelled   -- インラインEnum
    retry_count: Integer

    -- Relationships
    invitation: Invitation with candidacy = this         -- 一対一
    slots: InterviewSlot with candidacy = this           -- 一対多

    -- Projections
    confirmed_slots: slots where status = confirmed
    pending_slots: slots where status = pending

    -- Derived
    is_ready: confirmed_slots.count >= 3
    has_expired: invitation.expires_at <= now
}

外部エンティティ

external entity Role { title: String, required_skills: Set<Skill>, location: Location }

値型

value TimeRange { start: Timestamp, end: Timestamp, duration: end - start }

Sum型

基本エンティティは判別子フィールドを宣言し、その大文字化された値がバリアント名になります。バリアントは variant キーワードを使用します。

entity Node {
    path: Path
    kind: Branch | Leaf              -- 判別子フィールド
}

variant Branch : Node {
    children: List<Node?>
}

variant Leaf : Node {
    data: List<Integer>
    log: List<Integer>
}

小文字のパイプ値は Enum リテラル（status: pending | active）です。大文字化された値はバリアント参照（kind: Branch | Leaf）です。型ガード（requires: または if ブランチ）がバリアントを絞り込み、そのフィールドをアンロックします。

モジュール given

モジュールのルールが動作するエンティティインスタンスを宣言します。すべてのルールはこれらのバインディングを継承します。すべてのモジュールに必要ではありません：ドメインエンティティでトリガーされたスコープのルールは、トリガーからエンティティを取得します。given は、ルールがモジュールスコープごとに 1 回存在する共有インスタンスで動作する仕様用です。

given {
    pipeline: HiringPipeline
    calendar: InterviewCalendar
}

インポートされたモジュールインスタンスは、限定名（scheduling/calendar）でアクセスでき、ローカル given ブロックには表示されません。サーフェス context とは異なり、これはパラメトリックスコープのバインディングです。

ルール

rule InvitationExpires {
    when: invitation: Invitation.expires_at <= now
    requires: invitation.status = pending
    let remaining = invitation.proposed_slots where status != cancelled
    ensures: invitation.status = expired
    ensures:
        for s in remaining:
            s.status = cancelled
    @guidance
        -- 非規範的な実装アドバイス。
}

トリガータイプ

• 外部刺激: when: CandidateSelectsSlot(invitation, slot) — システム外部からのアクション
• 状態遷移: when: interview: Interview.status transitions_to scheduled — エンティティが状態を変更（遷移のみ、作成ではない）
• 状態の成立: when: interview: Interview.status becomes scheduled — エンティティがこの値を持つ（作成または遷移による）
• 時間ベース: when: invitation: Invitation.expires_at <= now — 時間ベースの条件（再発動を防ぐため常に requires ガードを追加）
• 派生条件: when: interview: Interview.all_feedback_in — 派生値が true になる
• エンティティ作成: when: batch: DigestBatch.created — 新しいエンティティが作成されたときに発火
• チェーン: when: AllConfirmationsResolved(candidacy) — 別のルールの ensures 句からのトリガー発行をサブスクライブ

すべてのエンティティスコープトリガーは明示的な var: Type バインディングを使用します。名前が不要な場合は _ をディスカードバインディングとして使用します：when: _: Invitation.expires_at <= now、when: SomeEvent(_, slot)。

ルールレベルの反復

for 句は、コレクション内の各要素に対してルール本体を 1 回適用します：

rule ProcessDigests {
    when: schedule: DigestSchedule.next_run_at <= now
    for user in Users where notification_setting.digest_enabled:
        let settings = user.notification_setting
        ensures: DigestBatch.created(user: user, ...)
}

Ensures パターン

Ensures 句には 4 つの結果形式があります：

• 状態変更: entity.field = value
• エンティティ作成: Entity.created(...) — 単一の正規作成動詞
• トリガー発行: TriggerName(params) — 他のルールがチェーンできるようにイベントを発行
• エンティティ削除: not exists entity — エンティティが存在しなくなったことを宣言

これらの形式は、for 反復（for x in collection: ...）、if/else 条件付き、let バインディングと組み合わせられます。

エンティティ作成は .created() を排他的に使用します。ドメイン意味はエンティティ名とルール名に存在し、作成動詞には存在しません。

状態変更の割り当てでは、右辺の式はルール前のフィールド値を参照します。ensures ブロック内の条件（if ガード、作成パラメータ、トリガー発行パラメータ）は、結果の状態を参照します。

サーフェス

surface InterviewerDashboard {
    facing viewer: Interviewer

    context assignment: SlotConfirmation where interviewer = viewer

    exposes:
        assignment.slot.time
        assignment.status

    provides:
        InterviewerConfirmsSlot(viewer, assignment.slot)
            when assignment.status = pending

    related:
        InterviewDetail(assignment.slot.interview)
            when assignment.slot.interview != null
}

サーフェスは境界でのコントラクトを定義します。facing 句は外部パーティを名付け、context はエンティティをスコープしています。残りの句は、境界がユーザー向けであるか、コード間であるかに関わらず、単一の語彙を使用します：exposes（表示可能なデータ、コレクションに対する for 反復をサポート）、provides（オプションの when ガード付きで利用可能な操作）、contracts:（demands/fulfils 方向マーカー付きのモジュールレベル contract 宣言を参照）、@guarantee（境界に関する名前付きプローズ宣言）、@guidance（非規範的なアドバイス）、related（この境界から到達可能な関連サーフェス）、timeout（サーフェスのコンテキスト内で適用される時間ルールへの参照）。

facing 句は、アクタータイプ（対応する actor 宣言と identified_by マッピング付き）またはエンティティタイプを直接受け入れます。境界が特定の ID 要件を持つ場合はアクター宣言を使用します；任意のインスタンスが相互作用できる場合はエンティティタイプを使用します（例：facing visitor: User）。外部パーティがコードである統合サーフェスの場合、最小限の identified_by 式を持つアクタータイプを宣言します。identified_by 式で within を参照するアクターは、期待されるコンテキストタイプを宣言する必要があります：within: Workspace。

サーフェスから実装へのコントラクト

exposes ブロックはフィールドレベルのコントラクトです：実装は正確にこれらのフィールドを返し、コンシューマーはこれらのフィールドを正確に使用します。リストされていないフィールドを追加しないでください。リストされているフィールドを省略しないでください。

コントラクト

contract Codec {
    serialize: (value: Any) -> ByteArray
    deserialize: (bytes: ByteArray) -> Any

    @invariant Roundtrip
        -- deserialize(serialize(value)) produces a value
        -- equivalent to the original for all supported types.
}

コントラクトはモジュールレベルの宣言で、サーフェス contracts: 句で名前で参照されます（demands Codec、fulfils EventSubmitter）。宣言構文と参照ルールについては Contracts を参照してください。

式

ナビゲーション：interview.candidacy.candidate.email、reply_to?.author（オプション）、timezone ?? "UTC"（null 結合）。コレクション：slots.count、slot in invitation.slots、interviewers.any(i => i.can_solo)、for item in collection: item.status = cancelled、permissions + inherited（セット和）、old - new（セット差）。比較：status = pending、count >= 2、status in {confirmed, declined}、provider not in providers。ブール論理：a and b、a or b、not a、a implies b。

モジュール仕様

use "github.com/allium-specs/google-oauth/abc123def" as oauth

限定名は仕様全体でエンティティを参照します：oauth/Session。座標は不変です（git SHA またはコンテンツハッシュ）。ローカル仕様は相対パスを使用します：use "./candidacy.allium" as candidacy。

コンフィグ

config {
    invitation_expiry: Duration = 7.days
    max_login_attempts: Integer = 5
    extended_expiry: Duration = invitation_expiry * 2              -- 式形式のデフォルト
    sync_timeout: Duration = core/config.default_timeout           -- コンフィグパラメータ参照
}

ルールは config.invitation_expiry としてコンフィグ値を参照します。デフォルトエンティティインスタンスの場合、default を使用します。

デフォルト

default Role viewer = { name: "viewer", permissions: { "documents.read" } }

インバリアント

invariant NonNegativeBalance {
    for account in Accounts:
        account.balance >= 0
}

式を含むインバリアント（invariant Name { expression }）はエンティティ状態に対するプロパティを宣言します。これらは論理的なアサーションであり、ランタイムチェックではありません。コントラクト内のプローズ注釈（@ 記号でマークされ、チェッカーが評価しない内容）とは異なります。Invariants を参照してください。

遷移グラフ（v3）

entity Order {
    status: pending | confirmed | shipped | delivered | cancelled

    transitions status {
        pending -> confirmed
        confirmed -> shipped
        shipped -> delivered
        pending -> cancelled
        confirmed -> cancelled
        terminal: delivered, cancelled
    }
}

状態依存フィールド存在（v3）

entity Order {
    status: pending | confirmed | shipped | delivered | cancelled
    customer: Customer
    total: Money
    tracking_number: String when status = shipped | delivered
    shipped_at: Timestamp when status = shipped | delivered

    transitions status {
        pending -> confirmed
        confirmed -> shipped
        shipped -> delivered
        pending -> cancelled
        confirmed -> cancelled
        terminal: delivered, cancelled
    }
}

遅延仕様

deferred InterviewerMatching.suggest    -- see: detailed/interviewer-matching.allium

未解決の質問

open question "Admin ownership - should admins be assigned to specific roles?"

検証

allium CLI がインストールされている場合、書き込みまたは編集後に .allium ファイルが自動的に検証されます。報告されたすべての問題を修正してから、結果を提示してください。CLI が利用できない場合は、言語リファレンスに対して検証してください。

リファレンス

• 言語リファレンス — エンティティ、ルール、式、サーフェス、コントラクト、インバリアント、検証の完全な構文
• テスト生成 — 仕様からテストを生成
• パターン — 9 つの解説されたパターン：認証、RBAC、招待、ソフト削除、通知、使用制限、コメント、ライブラリ仕様統合、フレームワーク統合コントラクト