allium

Allium

Allium は、ドメインレベルでソフトウェアの振る舞いを記述するための形式言語です。非形式的な機能の説明と実装の間に位置し、ソフトウェアの構築方法を規定せずに、ソフトウェアが何をするのかを正確に指定できます。

名前は、タマネギやエシャロットを含む植物の属に由来し、Cucumber や Gherkin が築いてきた振る舞い仕様ツールの伝統を受け継いでいます。

主な原則：

• 実装ではなく、観察可能な振る舞いを記述します
• 振る舞いのレベルで重要なドメインロジックを捉えます
• 統合テストとエンドツーエンドテストを生成します（単体テストではありません）
• 実装前に曖昧さを明らかにします
• 実装に依存しません。同じ仕様をどの言語でも実装できます

Allium は、プログラミング言語やフレームワークの選択、データベーススキーマやストレージの仕組み、API の設計や UI のレイアウト、内部アルゴリズム（ドメインレベルの関心事である場合を除く）を規定しません。

ルーティング表

タスク	ツール	利用する場面
.allium ファイルの作成または読み取り	このスキル	言語の構文や構造が必要な場合
会話を通じた仕様の作成	elicit スキル	ユーザーが構築したい機能や振る舞いを説明する場合
既存コードからの仕様の抽出	distill スキル	ユーザーが実装コードを持っており、そこから仕様を作成したい場合
既存の仕様の変更	tend スキル	ユーザーが .allium ファイルに対象を絞った変更を加えたい場合
仕様とコードの整合性の確認	weed スキル	ユーザーが仕様と実装の相違を見つける、または修正したい場合
仕様からのテスト生成	propagate スキル	ユーザーが仕様からテスト、PBT プロパティ、またはステートマシンテストを生成したい場合
ループの収束の証明	witness スキル	ユーザーがグラウンドトゥルースに基づいて実行の収束の主張を独立して確認したい場合 — テストが実際に成功すること、生成されたテストが弱められていないこと、ブロッキングとなる質問がひそかに先送りされていないことを確認します
ループ全体を収束まで実行	このスキル（ループの実行を参照）	ユーザーが機能をエンドツーエンドで構築または調整したい場合 — /allium <goal> が gather→act→verify→repeat のループを自律的に実行し、仕様、テスト、コードが一致するまで続けます

/allium への応答（ループ優先）

/allium はエントリーポイントです。自律的な経路を優先してください。ループ全体を実行する価値こそが、単発でスキルを使うだけでは得られないものです。

• 明確な単一タスク → ルーティング表に従って該当するスキルへ直接案内します。ユーザーにメニューを選ばせないでください。

• 目標や機能（例：「ギフトカードを追加する」「パスワードリセットを使えるようにする」）→ 単一フェーズだけを実行するのではなく、ループ全体をエンドツーエンドで実行します。ループの実行に従ってください。

• 具体性がない、または曖昧 → ループ優先で案内します。まずループ全体の実行を標準の選択肢として提案し、その後、個別スキルを手動操作の手段として、それぞれ一行のヒントとともに列挙します。また、プロジェクトの状態（既存の .allium 仕様があるか、仕様はないがコードがあるか、調整すべき乖離があるか）を踏まえて、具体的な開始点を提案します。例：

  目標を教えていただければ、仕様 → テスト → コードの順に、すべてが一致するまでループ全体を実行します。または、ステップを一つだけ実行することもできます。elicit（意図から仕様を作成）、distill（既存コードから仕様を作成）、propagate（仕様からテストを作成）、tend（仕様を編集）、weed（仕様とコードの乖離を修正）を使えます。コードはありますが、まだ .allium がないので、まずはコードから仕様を抽出するのがおすすめです。目標を教えていただければ、エンドツーエンドで進めることもできます。

ループを先に提示し、手動で制御したいユーザーにも個別スキルをすぐ使えるようにしてください。また、単一のスキルが完了したら、ユーザーに尋ねられるのを待たずに、次のフェーズを積極的に提案してください。

Allium ループ（推奨される実行順序）

スキルは一度限りのコマンドではありません。自律的なループとして組み合わせることができ、コンテキストの収集 → アクションの実行 → 検証 → 繰り返しの流れで、仕様（意図）、テスト（契約）、コード（実装）の3つの成果物を一致させます。/elicit または /distill でコンテキストを収集し（仕様は永続的なコンテキストです）、/propagate を実行してから実装に移ります。仕様先行の作業では、まず新しいテストが失敗することを確認してください。実装前からテストが成功している場合は、すでにカバーされているか、実質的に意味のないテストです。テストを実行して検証し、次に /weed、その後に CLI の構造チェックを行います。収束するまで繰り返してください。最も重要なのは検証フェーズです。仕様・テスト・weed のシグナルがそろうことで、このループの信頼性が確保されます。スキルを実行した後は、次のステップを尋ねられるのを待たずに積極的に提案してください。ループ全体を一度に収束させるには、/allium に目標を伝えるだけです。ループの進め方に従って、ループを自動で進めます。

2つの開始点から、同じ収束ループに進みます。

• 仕様先行（前向き、意図から開始）： /elicit → /propagate → 実装 → /weed。要件が変わったら /tend を実行し、続けて /propagate を再実行します。
• コード先行（後ろ向き、既存コードから開始）： /distill → 意図された動作と偶発的な動作を確認 → /propagate → コードに対してテストを実行 → /weed で整合 → 領域ごとに繰り返します。

テストが成功し、/weed が乖離なしと報告し、未解決の疑問が残っておらず（さらにコード先行の場合は、新たに /distill を実行しても何も見つからず）、独立した /witness の実行でその主張が実際の状態に照らして証明されたとき、作業は「完了」です。ループ中は、常に次の2つのルールを守ってください。生成されたテストを通すために弱めてはいけません（代わりに仕様を修正し、/propagate を再実行します）。また、本当に曖昧な点は推測せず、人間に確認してください。どちらも収束ゲートで witness によって徹底されるため、信頼に委ねられることはありません。

実装自体は通常のコーディングです。Allium が生成するのは仕様とテストであり、アプリケーションコードではありません。手順全体、図、終了条件、実装プロンプトについては、推奨ループのリファレンスを参照してください。

クイック構文まとめ

エンティティ

entity Candidacy {
    -- Fields
    candidate: Candidate
    role: Role
    status: pending | active | completed | cancelled   -- inline enum
    retry_count: Integer

    -- Relationships
    invitation: Invitation with candidacy = this         -- one-to-one
    slots: InterviewSlot with candidacy = this           -- one-to-many

    -- 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 }

合計型

ベースエンティティでは、判別フィールドを宣言します。このフィールドの大文字で始まる値が、各バリアントの名前になります。バリアントには variant キーワードを使用します。

entity Node {
    path: Path
    kind: Branch | Leaf              -- discriminator field
}

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

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

小文字のパイプ区切り値は列挙リテラルです（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
        -- Non-normative implementation advice.
}

トリガーの種類

• 外部刺激：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 句は、コレクション内の要素ごとにルール本体を実行します。

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 マッピングを持つアクター型、またはエンティティ型を直接指定できます。境界に特定の識別要件がある場合は actor 宣言を使用します。任意のインスタンスがやり取りできる場合（例：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）。宣言構文と参照規則については、契約を参照してください。

式

ナビゲーション: 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              -- expression-form default
    sync_timeout: Duration = core/config.default_timeout           -- config parameter reference
}

ルールは設定値を config.invitation_expiry として参照します。デフォルトのエンティティインスタンスには default を使用します。

デフォルト

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

不変条件

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

式を伴う不変条件 (invariant Name { expression }) は、エンティティの状態に関するプロパティを表明します。これらは論理的な表明であり、実行時のチェックではありません。コントラクト内の散文による注釈 (@invariant Name) とは異なります。後者は @ 記号を使用して、チェッカーが評価しないコンテンツをマークします。詳細は不変条件を参照してください。

遷移グラフ (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 が利用できない場合は、言語リファレンスに照らして検証してください。

参照

• 言語リファレンス — エンティティ、ルール、式、サーフェス、コントラクト、不変条件、バリデーションの完全な構文
• テスト生成 — 仕様からのテストの生成
• 推奨されるループ — コンテキストを集める → アクションを起こす → 検証する → 繰り返すループ。仕様ファーストとコードファーストのウォークスルー付き
• ループの駆動 — /allium が目標を収束へと導くために従う手順 (エントリ検出、ティック、停止条件、台帳)
• スライスの統合 — ファンアウトした目標のための reduce ステップ: スライスを組み立て、allium analyse で継ぎ目をクロスチェックし、全体を照合して witness する
• パターン — 9 つの実例パターン: 認証、RBAC、招待、ソフト削除、通知、使用制限、コメント、ライブラリ仕様の統合、フレームワーク統合コントラクト