allium

Allium

Allium 是一種形式化語言，用於在領域層級捕捉軟體行為。它介於非正式的功能描述與實作之間，提供一種精確的方式來指定軟體做什麼，而不規定如何建構。

名稱來自包含洋蔥和紅蔥頭的植物科，延續了 Cucumber 和 Gherkin 在行為規格工具上的傳統。

關鍵原則：

• 描述可觀察的行為，而非實作
• 捕捉在行為層級重要的領域邏輯
• 產生整合測試和端到端測試（而非單元測試）
• 在實作前強迫模糊之處浮現
• 與實作無關：同一份規格可以用任何語言實作

Allium 不指定程式語言或框架選擇、資料庫 schema 或儲存機制、API 設計或 UI 佈局，或內部演算法（除非它們是領域層級的問題）。

路由表

任務	工具	時機
撰寫或閱讀 .allium 檔案	此技能	你需要語言語法和結構
透過對話建構規格	elicit 技能	使用者描述想要建構的功能或行為
從現有程式碼萃取規格	distill 技能	使用者有實作程式碼並想要從中取得規格
修改現有規格	tend 技能	使用者想要對 .allium 檔案進行有針對性的修改
檢查規格與程式碼的一致性	weed 技能	使用者想要找出或修復規格與實作之間的差異
從規格產生測試	propagate 技能	使用者想要從規格產生測試、PBT 屬性或狀態機測試
驅動整個循環直到收斂	此技能（參閱 驅動循環）	使用者想要端到端建構或調和一個功能 — /allium <goal> 會自動執行收集→行動→驗證→重複循環，直到規格、測試和程式碼一致

回應 /allium（循環優先）

/allium 是進入點。傾向於自主路徑 — 整個循環的價值正是偶爾使用單一技能所錯過的：

• 明確的單一任務 → 直接路由到該技能（根據路由表）；不要讓使用者瀏覽選單。

• 目標或功能（例如「新增禮物卡」、「讓密碼重設運作」）→ 自己驅動整個循環，而不是只執行一個階段。遵循驅動循環。

• 簡潔或模糊 → 以循環優先引導使用者：提供驅動循環作為預設選項，然後列出個別技能作為控制路徑，並附上一行提示，並根據專案狀態建議具體的起點（現有的 .allium 規格？有程式碼但沒有規格？需要調和的偏差？）。例如：

  告訴我一個目標，我會驅動整個循環 — 規格 → 測試 → 程式碼，直到它們一致。或者自己執行一個步驟：elicit（從意圖產生規格）、distill（從現有程式碼萃取規格）、propagate（從規格產生測試）、tend（編輯規格）、weed（修復規格↔程式碼偏差）。你已經有程式碼但還沒有 .allium，所以我會從萃取開始 — 或者直接給我目標，我會端到端處理。

以循環為主；將個別技能保留在一步之遙，供想要手動控制的使用者使用。一旦單一技能完成，主動建議下一步，而不是等待被問。

Allium 循環（建議順序）

這些技能不是一次性指令；它們組合成一個自主風格的循環 — 收集上下文 → 採取行動 → 驗證 → 重複 — 驅動三個產物達成一致：規格（意圖）、測試（合約）和程式碼（實作）。使用 /elicit 或 /distill 收集上下文（規格是持久的上下文）；使用 /propagate 然後實作來採取行動（在規格優先的工作中，先確認新測試失敗 — 一個在實作前就已經通過的測試表示已經覆蓋或空洞）；透過執行測試、然後 /weed、然後 CLI 結構檢查來驗證；重複直到收斂。驗證是最重要的階段，而規格加測試加 weed 的信號使循環值得信賴。在呼叫一個技能後，主動建議下一步，而不是等待被問。要一次執行整個循環直到收斂，只需給 /allium 一個目標 — 它會為你驅動循環，遵循驅動循環。

兩個進入點，一個收斂循環：

• 規格優先（正向，從意圖開始）： /elicit → /propagate → 實作 → /weed；當需求變更時使用 /tend 然後重新 /propagate。
• 程式碼優先（反向，從現有程式碼開始）： /distill → 審查預期與意外的行為 → /propagate → 對程式碼執行測試 → /weed 進行調和 → 按區域重複。

當測試通過、/weed 報告無偏差且沒有未解決的問題時，工作就「完成」了（此外，對於程式碼優先，一次新的 /distill 沒有發現新東西）。循環中的兩條常規規則：永遠不要為了讓測試通過而削弱產生的測試（而是修復規格並重新 propagate），並將真正的模糊之處升級給人類，而不是猜測。

實作本身是普通的編碼 — Allium 產生規格和測試，而不是應用程式碼。請參閱建議循環參考資料以獲得完整的逐步說明、圖表、退出條件和實作提示。

快速語法摘要

實體

entity Candidacy {
    -- 欄位
    candidate: Candidate
    role: Role
    status: pending | active | completed | cancelled   -- 行內列舉
    retry_count: Integer

    -- 關係
    invitation: Invitation with candidacy = this         -- 一對一
    slots: InterviewSlot with candidacy = this           -- 一對多

    -- 投影
    confirmed_slots: slots where status = confirmed
    pending_slots: slots where status = pending

    -- 衍生
    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              -- 鑑別欄位
}

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 用於規則操作共享實例的規格，這些實例在每個模組範圍內存在一次。

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 子句對集合中的每個元素應用規則主體一次：

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 子句有四種結果形式：

• 狀態變更：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:（參考模組層級的 contract 宣告，帶有 demands/fulfils 方向標記）、@guarantee（關於邊界的命名散文斷言）、@guidance（非規範性建議）、related（從此表面可達的相關表面）、timeout（參考適用於表面上下文內的時序規則）。

facing 子句接受一個參與者類型（帶有對應的 actor 宣告和 identified_by 映射）或直接一個實體類型。當邊界有特定身份要求時使用參與者宣告；當任何實例都可以互動時使用實體類型（例如 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)) 產生的值
        -- 對於所有支援的類型，等同於原始值。
}

合約是模組層級的宣告，透過名稱在表面 contracts: 子句中參考（demands Codec、fulfils EventSubmitter）。請參閱合約以了解宣告語法和參考規則。

表達式

導航：interview.candidacy.candidate.email、reply_to?.author（可選）、timezone ?? "UTC"（空值合併）。集合：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 }）斷言關於實體狀態的屬性。它們是邏輯斷言，而非執行期檢查。與合約中的散文註解（@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    -- 參閱：detailed/interviewer-matching.allium

開放問題

open question "管理員所有權 - 管理員是否應被指派到特定角色？"

驗證

當 allium CLI 安裝後，一個鉤子會在每次寫入或編輯後自動驗證 .allium 檔案。在呈現結果前修復任何回報的問題。如果 CLI 不可用，請根據語言參考進行驗證。

參考資料

• 語言參考 — 實體、規則、表達式、表面、合約、不變量和驗證的完整語法
• 測試產生 — 從規格產生測試
• 建議循環 — 收集上下文 → 採取行動 → 驗證 → 重複循環，包含規格優先和程式碼優先的逐步說明
• 驅動循環 — /allium 遵循的程序，用於驅動目標直到收斂（進入點偵測、滴答、停止條件、帳本）
• 模式 — 9 個實作模式：認證、RBAC、邀請、軟刪除、通知、使用限制、評論、函式庫規格整合、框架整合合約