allium

Allium

Allium 是一种用于在领域层面描述软件行为的形式语言。它处于非正式功能描述与实现之间，提供一种精确的方式来说明软件的行为，而不规定软件的构建方式。

这个名称源自包含洋葱和青葱的植物科，延续了由 Cucumber 和 Gherkin 开创的行为规范工具传统。

核心原则：

• 描述可观察到的行为，而非实现方式
• 捕捉行为层面重要的领域逻辑
• 生成集成测试和端到端测试（而非单元测试）
• 在实现前揭示歧义
• 与实现无关：同一份规范可以用任何语言实现

Allium 不规定编程语言或框架的选择、数据库架构或存储机制、API 设计或 UI 布局，也不规定内部算法（除非它们属于领域层面的关注点）。

路由表

任务	工具	适用场景
编写或读取 .allium 文件	此技能	你需要了解语言语法和结构
通过对话构建规范	elicit 技能	用户描述了想要构建的功能或行为
从现有代码提取规范	distill 技能	用户有实现代码，并希望从中提取规范
修改现有规范	tend 技能	用户希望对 .allium 文件进行定向修改
检查规范与代码是否一致	weed 技能	用户希望找出或修复规范与实现之间的偏差
根据规范生成测试	propagate 技能	用户希望根据规范生成测试、PBT 属性或状态机测试
证明循环已收敛	witness 技能	用户希望根据真实情况独立确认某次运行的收敛声明——测试确实通过、没有削弱任何生成的测试，也没有悄悄搁置任何阻塞问题
推动整个循环直至收敛	此技能（参见推动循环）	用户希望端到端地构建或协调某项功能——/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 后没有发现新内容），且一次独立的 /witness 检查根据真实情况证实了这一结论时，工作才算“完成”。循环期间有两条始终适用的规则：绝不为了让测试通过而弱化生成的测试（应修复规格并重新运行 /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 适用于规则操作共享实例且这些实例只在每个模块作用域中存在一次的规格。

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

• 状态变更：entity.field = value
• 实体创建：Entity.created(...) — 唯一规范的创建动词
• 触发器发出：TriggerName(params) — 发出事件，供其他规则链接
• 实体移除：not exists entity — 断言实体不再存在

这些形式可以与 for 迭代（for x in collection: ...）、if/else 条件语句和 let 绑定组合使用。

实体创建只使用 .created()。领域含义由实体名称和规则名称体现，而不是由创建动词体现。

在状态变更赋值中，右侧表达式引用规则执行前的字段值。Ensures 块中的条件（if 守卫、创建参数、触发器发出参数）引用结果状态。

Surface

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
}

Surface 在边界处定义契约。facing 子句命名外部参与方，context 限定实体作用域。其余子句无论边界面向用户还是代码间交互，都使用同一套词汇：exposes（可见数据，支持对集合进行 for 迭代）、provides（可用操作，可选用 when 守卫）、contracts:（引用模块级 contract 声明，并用 demands/fulfils 标记方向）、@guarantee（关于边界的具名文字断言）、@guidance（非规范性建议）、related（从当前 Surface 可访问的相关 Surface）、timeout（引用适用于该 Surface 上下文的时间规则）。

facing 子句接受参与者类型（需有对应的 actor 声明和 identified_by 映射）或直接接受实体类型。若边界有特定身份要求，请使用参与者声明；若任何实例都可以交互，请使用实体类型（例如，facing visitor: User）。对于外部参与方为代码的集成 Surface，请声明参与者类型，并使用最简的 identified_by 表达式。在 identified_by 表达式中引用 within 的参与者，必须声明预期的上下文类型：within: Workspace。

Surface 与实现之间的契约

exposes 块是字段级契约：实现恰好返回这些字段，使用方也恰好使用这些字段。不得添加未列出的字段，也不得省略已列出的字段。

Contract

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

Contract 是模块级声明，由 Surface 的 contracts: 子句按名称引用（demands Codec、fulfils EventSubmitter）。声明语法和引用规则请参阅 Contracts。

表达式

导航：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              -- 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 不可用，请根据语言参考进行验证。

参考资料

• 语言参考 — 实体、规则、表达式、界面、合约、不变量和验证的完整语法
• 测试生成 — 根据规格生成测试
• 推荐循环 — gather-context → take-action → verify → repeat 循环，包含规格优先和代码优先的演练
• 驱动循环 — /allium 用于推动目标收敛的流程（入口检测、tick、停止条件、账本）
• 集成切片 — 针对拆分目标的 reduce 步骤：组装切片，使用 allium analyse 交叉检查衔接处，协调并验证整体
• 模式 — 9 个完整示例：身份验证、RBAC、邀请、软删除、通知、使用限额、评论、库规格集成、框架集成合约