例で見る
ここにあるのは全部、このリポジトリのテストが毎回走らせている規則です。rulec check を通り、書いてある例が実行され、参照評価器と生成したどの言語も同じ答えを返すことまで確かめられています。そのままコピーして動かせます。
小さいものから順に並べてあります。
日付で区分を返す
いちばん小さい例です。入力は注文日ひとつ、出力は期間の区分ひとつ。行は隣り合う日付の範囲で、隙間なく敷き詰めてあります。
rule 期間区分(period) v1
description "注文日で適用期間を決める。両端を含む日付の範囲を、隙間なく隣り合わせに並べた例"
# 通算日で持たないと、月末と翌月初のあいだに実在しない整数の隙間ができて偽の E101 が出る（§2.1）
enum 期間(kind) = 改定前(before) | 春季(spring) | 通常(normal) | 年末(year_end)
inputs
注文日(order_date) : date range >=2026-01-01 <=2026-12-31
outputs
区分(kind) : 期間
table 期間判定(pick)
policy unique
| 注文日 | -> 区分(kind) : 期間 |
| <=2026-03-31 | 改定前 |
| >=2026-04-01 <=2026-06-30 | 春季 |
| >=2026-07-01 <=2026-11-30 | 通常 |
| >=2026-12-01 | 年末 |
examples
| 注文日 | -> 区分 |
| 2026-03-31 | 改定前 |
| 2026-04-01 | 春季 |
| 2026-06-30 | 春季 |
| 2026-07-01 | 通常 |
| 2026-12-01 | 年末 |
この例が見せていること
- 日付は比較と範囲だけです。足し算も引き算もありません。
<=2026-03-31と>=2026-04-01が隣り合っていることを検査が知っています。内部で日付を通算日として持っているからで、20260331のような数で持つと月末と翌月初のあいだに実在しない隙間ができ、偽のエラーが出ます。- 出力が金額ではないので、
roundは要りません。
条件が三つ絡む送料
設計のスケッチをそのまま規則にしたものです。真偽の定義を表の列に置く形、率の出力、default の印、policy first の隠れが一度に出てきます。
rule 送料(shipping_fee) v4
description "設計文書 §1.2 のスケッチを規則にしたもの。真偽定義を列に使う正常系と、率の出力、default の印、policy first の要確認 1 対が出てくる"
import std/都道府県
enum 会員区分(member_kind) = 一般(basic) default | ゴールド(gold) default | プラチナ(platinum)
group 遠隔地(remote) = 北海道, 沖縄県
inputs
届け先(dest) : 都道府県
重量(weight) : mass[g] range >=1g <=40kg
注文金額(total) : money[円, incl_tax] range >=0円 <=1000万円
会員(member) : 会員区分
outputs
送料(fee) : money[円, incl_tax] round up(10円)
# 真偽の定義。条件は入力ひとつを見るだけなので、展開すれば区画の足し合わせになる（§5.3、§6.2）
define 大口(bulk) : bool = 注文金額 >= 3万円
table 基本送料(base_fee)
policy unique
| 届け先 | 重量 | -> 基本送料(base) : money[円, incl_tax] |
| 遠隔地 | <=2000g | 1200円 |
| 遠隔地 | >2000g | 1800円 |
| not: 遠隔地 | <=2000g | 800円 |
| not: 遠隔地 | >2000g | 1100円 |
table 負担判定(payer)
policy first
| 大口 | 会員 | -> 負担率(pay_rate) : rate |
| true | - | 0% |
| - | プラチナ | 50% |
| - | - | 100% |
result 送料 = 基本送料 × 負担率
examples
| 届け先 | 重量 | 注文金額 | 会員 | -> 送料 |
| 沖縄県 | 2500g | 40000円 | 一般 | 0円 |
| 東京都 | 1999g | 12000円 | プラチナ | 400円 |
| 北海道 | 500g | 5000円 | 一般 | 1200円 |
この例が見せていること
define … : boolは表の列に置ける真偽の名前です。条件に名前が付くので、表のほうが読みやすくなります。defaultは「この値に専用の行は要らない」という宣言です。付けないと「どの行にも現れません」と警告されます。policy firstなので、上の行が下の行を隠します。それが階段として自然な形かどうかを、検査が三つに分けて数えます。
実在の運賃表を転記する
日本郵便の基本運賃表（東京発）です。47 都道府県 × 7 サイズ = 329 通りを、6 つのグループで 42 行に畳んでいます。このツールの最初の実用価値がここにあります — 県をひとつ書き落とすと、走らせる前に、その県の名前を出して止まります。
rule ゆうパック運賃(yupack_fee) v1
description "東京から差し出す場合の基本運賃"
import std/都道府県
enum サイズ区分(size_class) = S60(s60) | S80(s80) | S100(s100) | S120(s120) | S140(s140) | S160(s160) | S170(s170)
group 都内(tokyo) = 東京都
group 北海道九州(hk) = 北海道, 福岡県, 佐賀県, 長崎県, 熊本県, 大分県, 宮崎県, 鹿児島県
group 近距離圏(near) = 青森県, 岩手県, 宮城県, 秋田県, 山形県, 福島県, 茨城県, 栃木県, 群馬県, 埼玉県, 千葉県, 神奈川県, 山梨県, 新潟県, 長野県, 富山県, 石川県, 福井県, 岐阜県, 静岡県, 愛知県, 三重県
group 近畿圏(kinki) = 滋賀県, 京都府, 大阪府, 兵庫県, 奈良県, 和歌山県
group 中国四国(cs) = 鳥取県, 島根県, 岡山県, 広島県, 山口県, 徳島県, 香川県, 愛媛県, 高知県
group 沖縄(okinawa) = 沖縄県
inputs
あて先(dest) : 都道府県
三辺合計(girth) : length[cm] range >=1cm <=170cm
重量(weight) : mass[g] range >=1g <=25kg contract_only
outputs
運賃(fee) : money[円, incl_tax] round up(10円)
table サイズ判定(size_of) # 出典: 日本郵便 基本運賃表（東京）のサイズ区分
policy first
| 三辺合計 | -> サイズ(size) : サイズ区分 |
| <=60cm | S60 |
| <=80cm | S80 |
| <=100cm | S100 |
| <=120cm | S120 |
| <=140cm | S140 |
| <=160cm | S160 |
| - | S170 |
table 運賃表(fee_table) # 出典: 日本郵便 基本運賃表（東京）
policy unique
| あて先 | サイズ | -> 運賃(fee) : money[円, incl_tax] |
| 都内 | S60 | 820円 |
| 都内 | S80 | 1130円 |
| 都内 | S100 | 1450円 |
| 都内 | S120 | 1770円 |
| 都内 | S140 | 2120円 |
| 都内 | S160 | 2450円 |
| 都内 | S170 | 3000円 |
| 近距離圏 | S60 | 880円 |
| 近距離圏 | S80 | 1200円 |
| 近距離圏 | S100 | 1500円 |
| 近距離圏 | S120 | 1830円 |
| 近距離圏 | S140 | 2170円 |
| 近距離圏 | S160 | 2500円 |
| 近距離圏 | S170 | 3070円 |
| 近畿圏 | S60 | 990円 |
| 近畿圏 | S80 | 1310円 |
| 近畿圏 | S100 | 1620円 |
| 近畿圏 | S120 | 1940円 |
| 近畿圏 | S140 | 2300円 |
| 近畿圏 | S160 | 2610円 |
| 近畿圏 | S170 | 3750円 |
| 中国四国 | S60 | 1150円 |
| 中国四国 | S80 | 1440円 |
| 中国四国 | S100 | 1780円 |
| 中国四国 | S120 | 2080円 |
| 中国四国 | S140 | 2440円 |
| 中国四国 | S160 | 2750円 |
| 中国四国 | S170 | 3890円 |
| 北海道九州 | S60 | 1410円 |
| 北海道九州 | S80 | 1710円 |
| 北海道九州 | S100 | 2020円 |
| 北海道九州 | S120 | 2340円 |
| 北海道九州 | S140 | 2680円 |
| 北海道九州 | S160 | 3010円 |
| 北海道九州 | S170 | 4140円 |
| 沖縄 | S60 | 1450円 |
| 沖縄 | S80 | 1810円 |
| 沖縄 | S100 | 2160円 |
| 沖縄 | S120 | 2490円 |
| 沖縄 | S140 | 2860円 |
| 沖縄 | S160 | 3180円 |
| 沖縄 | S170 | 4350円 |
examples
| あて先 | 三辺合計 | 重量 | -> 運賃 |
| 東京都 | 55cm | 1kg | 820円 |
| 沖縄県 | 100cm | 3kg | 2160円 |
| 北海道 | 61cm | 20kg | 1710円 |
この例が見せていること
groupは列挙の一部に名前を付けたものです。検査のときは必ずもとの値に展開されるので、グループの分け方が 47 県の過不足ない分割になっているかまで検査されます。import std/都道府県で 47 値が入ります（ASCII の別名つき）。- 行が 42 本あっても、
policy uniqueなので並べ替えても意味が変わらないことが証明されています。
出力が二つある
クーポン 1 枚について、使えるかどうか（可否）と、いくら引くか（素割引）を同時に返します。重ね掛けの順序と反復は呼び出し側の仕事です。
rule クーポン一枚(coupon_step) v1
description "クーポン1枚の適用可否と素割引（設計文書 §5.4 のスケッチ）。重ね掛けの順序と反復は呼び出し側が持つ。複数出力と、出力セルの名前が出てくる"
enum クーポン種別(coupon_kind) = 率引き(percent) | 額引き(fixed) | 送料無料(free_ship)
inputs
商品合計(subtotal) : money[円, incl_tax] range >=0円 <=100万円
適用済割引(applied) : money[円, incl_tax] range >=0円 <=100万円
種別(kind) : クーポン種別
割引率(rate) : rate[step 1%] range >=0% <=100%
額面(face) : money[円, incl_tax] range >=0円 <=10万円
同商品適用済(dup) : bool
outputs
可否(ok) : bool
素割引(raw) : money[円, incl_tax] round down(1円)
# 端数処理は公開規約に記載がないので切り捨てに仮置き（§7.1）
derive 残余(margin) : money[円, incl_tax] = 商品合計 - 適用済割引 - 額面 range >=-110万円 <=100万円
define 率割引(rate_off) : money[円, incl_tax] = 商品合計 × 割引率
table 適用可否(applicable)
policy first
| 種別 | 残余 | 同商品適用済 | -> 可否(ok) : bool |
| - | - | true | false |
| 額引き | <=0円 | - | false |
| - | - | - | true |
table 素の割引(raw_discount)
policy unique
| 可否 | 種別 | -> 素割引(raw) : money[円, incl_tax] |
| false | - | 0円 |
| true | 率引き | 率割引 |
| true | 額引き | 額面 |
| true | 送料無料 | 0円 |
examples
| 商品合計 | 適用済割引 | 種別 | 割引率 | 額面 | 同商品適用済 | -> 可否 | 素割引 |
| 10000円 | 0円 | 率引き | 10% | 0円 | false | true | 1000円 |
| 10000円 | 0円 | 額引き | 0% | 500円 | false | true | 500円 |
| 400円 | 0円 | 額引き | 0% | 500円 | false | false | 0円 |
| 10000円 | 0円 | 率引き | 10% | 0円 | true | false | 0円 |
| 10000円 | 0円 | 送料無料 | 0% | 0円 | false | true | 0円 |
この例が見せていること
- 出力は二つ以上書けます。 二つの表が一つずつ埋め、どちらにも
roundが別々に効きます。 - 出力のセルには値か名前を一つだけ書けます。計算は
defineに出します — 表には分岐だけを残すためです。 - 一つ前の表の出力（
可否）を、次の表の列に使っています。上から下への一方通行なので、依存はいつでも目で追えます。
可否と金額を一度に
同じ題材を別の形で書いたものです。導出（derive）で残額を出し、それを表の列に置いています。
rule クーポン割引(coupon_discount) v1
description "クーポン1枚の適用可否と割引額。順序と反復は呼び出し側。出典: 楽天/Yahoo の公開ヘルプから再構成"
# ※ 出力セルに名前を書ける（§3.2 で採用済み）。式は書けないので、率引きは定義を一枚挟む
enum 種別(kind) = 率引き(rate) | 額引き(amount) | 送料無料(free_ship)
enum 適用範囲(scope) = 店内全商品(shop) default | 対象商品(item)
inputs
元価(list) : money[円,incl_tax] range >=0円 <=1000万円 # 率引きの基準
現在残額(running) : money[円,incl_tax] range >=0円 <=1000万円 # 額引きの基準（率引き適用後）
クーポン種別(kind) : 種別
クーポン範囲(scope): 適用範囲
割引率(rate) : rate[step 1%]
割引額面(face) : money[円,incl_tax] range >=0円 <=100万円
上限額(cap) : money[円,incl_tax] range >=0円 <=100万円
最低購入額(min) : money[円,incl_tax] range >=0円 <=100万円
同商品適用済(used): bool
期限内(alive) : bool
outputs
割引額(discount) : money[円,incl_tax] round down(1円)
# [導出] 実表が要求した形。どちらも「入力 − 入力」の線形結合
derive 最低差(min_gap) : money[円,incl_tax] = 現在残額 − 最低購入額 range >=-100万円 <=1000万円
derive 支払差(pay_gap) : money[円,incl_tax] = 現在残額 − 割引額面 range >=-100万円 <=1000万円
table 適用可否(applicable)
policy first
| 期限内 | 同商品適用済 | クーポン範囲 | クーポン種別 | 最低差 | 支払差 | -> 可否(ok) : bool |
| false | - | - | - | - | - | false |
| - | true | 対象商品 | - | - | - | false |
| - | - | - | - | <0円 | - | false |
| - | - | - | 額引き | - | <=0円 | false |
| - | - | - | - | - | - | true |
# 率引きは元価基準、額引きは割引後（現在残額）基準 — 楽天の原文どおり
define 率割引(rate_off) : money[円,incl_tax] = 元価 × 割引率
table 素の割引(raw_discount)
policy unique
| 可否 | クーポン種別 | -> 素割引(raw) : money[円,incl_tax] |
| false | - | 0円 |
| true | 率引き | 率割引 |
| true | 額引き | 割引額面 |
| true | 送料無料 | 0円 |
result 割引額 = down(min(素割引, 上限額), 1円)
examples
| 元価 | 現在残額 | クーポン種別 | クーポン範囲 | 割引率 | 割引額面 | 上限額 | 最低購入額 | 同商品適用済 | 期限内 | -> 割引額 |
| 10000円 | 10000円 | 率引き | 店内全商品 | 10% | 0円 | 1000円 | 5000円 | false | true | 1000円 |
| 10000円 | 9000円 | 額引き | 店内全商品 | 0% | 500円 | 500円 | 5000円 | false | true | 500円 |
| 10000円 | 400円 | 額引き | 店内全商品 | 0% | 500円 | 500円 | 0円 | false | true | 0円 |
この例が見せていること
deriveは入力どうしの足し算・引き算だけでできた、名前の付いた金額です。数量のまま表の列に置ける唯一の途中の値で、rangeの宣言が要ります。- 宣言した範囲が、実際に起こりうる値を含んでいないと E112 で止まります。範囲は検査が使う「全体集合」だからです。
検査が決められなかったとき
二つの導出が同じ入力を共有しているため、二つの行が同時に当てはまりうるかを検査が決められません。黙って通すことも、嘘のエラーを出すこともしません。警告を出し、生成コードに実行時のガードを入れます。
rule クーポン併用(coupon_stack) v1
description "二つの導出が入力を共有する 一意 の表。列ごとのふるいには重なって見え、消去が起きないと決める題材（§6.2、§15.126）"
enum 判定(verdict) = 対象外(no) default | 対象(yes)
inputs
合計(total) : money[円,incl_tax] range >=0円 <=100万円
割引A(disc_a) : money[円,incl_tax] range >=0円 <=10万円
割引B(disc_b) : money[円,incl_tax] range >=0円 <=10万円
outputs
併用可否(verdict) : 判定
# 割引B は 0 円以上なので、残高B は定義から必ず 残高A 以下になる。
# つまり 残高A <= 1000円 のとき 残高B が 3980円 に届くことはない。
# 検査は導出を一本ずつ独立に見るので、この結びつきが見えない。下の 行1 と 行2 は
# そこでは重なって見え、Fourier-Motzkin 消去が起きないと決める（§15.126）。
derive 残高A(rest_a) : money[円,incl_tax] = 合計 - 割引A range >=-10万円 <=100万円
derive 残高B(rest_b) : money[円,incl_tax] = 合計 - 割引A - 割引B range >=-20万円 <=100万円
table 適用判定(decide)
policy unique
| 残高A | 残高B | -> 併用可否(verdict) : 判定 |
| <=1000円 | - | 対象外 |
| - | >=3980円 | 対象 |
| >1000円 | <3980円 | 対象外 |
examples
| 合計 | 割引A | 割引B | -> 併用可否 |
| 500円 | 0円 | 0円 | 対象外 |
| 10000円 | 1000円 | 1000円 | 対象 |
| 5000円 | 2000円 | 2000円 | 対象外 |
この例が見せていること
- W114 は「証明できなかった」という警告です。重なりがあるともないとも言っていません。
- 生成コードには、万一その条件に当てはまる入力が来たとき、黙って先の行を選ばずにエラーを返すガードが入ります。このガードが動いたなら、重なりは本当にあったということです。
- 静的に決められないことを実行時に持ち越す唯一の場所です。
答えが順序
クーポン二枚のどちらを先に適用するかを返します。並べ替えそのものは呼び出し側がしますが、比較の基準は規則の中にあります — そこが承認の対象だからです。
rule 適用順序(apply_order) v1
description "クーポン二枚のどちらを先に適用するか（§5.4）。反復と並べ替えは呼び出し側で、比較だけが規則になる"
# 楽天の規約は「率引きを先に、次に額引き、額引きどうしは有効期限が近い順」
enum 種別(kind) = 率引き(rate) | 額引き(amount)
enum 先後(order) = 先(first) | 後(second)
inputs
A種別(a_kind) : 種別
B種別(b_kind) : 種別
A期限(a_due) : date
B期限(b_due) : date
outputs
A順序(a_order) : 先後
# 日付どうしの比較。導出にできない型なので、名前どうしを直接比べる第二の原子（§5.3）。
define Aが早いか同じ(a_earlier) : bool = A期限 <= B期限
table 順序判定(decide)
policy first
| A種別 | B種別 | Aが早いか同じ | -> A順序(a_order) : 先後 |
| 率引き | 額引き | - | 先 |
| 額引き | 率引き | - | 後 |
| - | - | true | 先 |
| - | - | - | 後 |
examples
| A種別 | B種別 | A期限 | B期限 | -> A順序 |
| 率引き | 額引き | 2026-12-31 | 2026-01-01 | 先 |
| 額引き | 率引き | 2026-01-01 | 2026-12-31 | 後 |
| 額引き | 額引き | 2026-04-01 | 2026-05-01 | 先 |
| 額引き | 額引き | 2026-05-01 | 2026-04-01 | 後 |
| 率引き | 率引き | 2026-04-01 | 2026-04-01 | 先 |
この例が見せていること
- 返せる答えは金額・可否・区分・順序の四種で、これはその四つめです。
- 入力は「二枚ぶんの属性」で、出力は
先か後。一度の判定に収まる形にしてあります。 - 日付どうしの比較が出てきます。
按分を、一件ずつに割る
一括の値引きを明細に配り切ります。1 明細 = 1 回の判定にしてあり、反復と残額の持ち回りは呼び出し側です。呼ぶ側は明細を順に回して残りを引くだけで、合計は構成上ぴったり合います（2,000 通りの明細で確かめました）。
rule 値引の充当(discount_fill) v1
description "一括値引きを明細に配分する。1 明細 = 1 回の判定で、反復と順序は呼び出し側が持つ"
inputs
明細定価(list) : money[円, incl_tax] range >=0円 <=100万円
残り値引(remaining) : money[円, incl_tax] range >=0円 <=100万円
対象(eligible) : bool
outputs
充当額(applied) : money[円, incl_tax] round down(1円)
define 充てられる額(cap) : money[円, incl_tax] = min(明細定価, 残り値引)
table 充当可否(applies)
policy unique
| 対象 | -> 充当(on) : money[円, incl_tax] |
| true | 充てられる額 |
| false | 0円 |
result 充当額 = 充当
examples
| 明細定価 | 残り値引 | 対象 | -> 充当額 |
| 3000円 | 1000円 | true | 1000円 |
| 500円 | 1000円 | true | 500円 |
| 3000円 | 1000円 | false | 0円 |
この例が見せていること
- 「配り方」を決めるのが規則、「配って回る」のが呼び出し側、という切り分けです。
minが使えます。上限で頭打ちにする形は、これで一行に収まります。- 定価の比で割り付ける按分は、この形ではなく
allocateで書きます（下の「比で配る按分」）。
1% より細かい率
契約ごとに決まる手数料率から、取引一件の手数料を出します。率の刻みが 0.1% なので、0.5% のような値を書けます。
rule 決済手数料(payment_fee) v1
description "契約ごとに決まる手数料率から取引一件の手数料を出す。率が 1% より細かい刻みで決まる例"
inputs
取引額(amount) : money[円, incl_tax] range >=0円 <=100万円
手数料率(rate) : rate[step 0.1%] range >=0% <=10%
少額(small) : bool
outputs
手数料(fee) : money[円, incl_tax] round up(1円)
# 0.5% 以下は徴収しない、という契約上の下限（率の刻みが 0.1% なのでこの行が書ける）
define 率手数料(rate_fee) : money[円, incl_tax] = 取引額 × 手数料率
table 手数料表(fee_table)
policy unique
| 手数料率 | 少額 | -> 手数料(fee) : money[円, incl_tax] |
| <=0.5% | - | 0円 |
| >0.5% | true | 50円 |
| >0.5% | false | 率手数料 |
result 手数料 = 手数料
examples
| 取引額 | 手数料率 | 少額 | -> 手数料 |
| 10000円 | 0.5% | false | 0円 |
| 10000円 | 0.6% | false | 60円 |
| 10000円 | 3.6% | false | 360円 |
| 10000円 | 3.6% | true | 50円 |
この例が見せていること
rate[step 0.1%]は「実行時の値は 0.1% の整数倍」という宣言です。0.5% は 5 刻み、10% は 100 刻みとして運ばれます。- 刻みの間の値は書けません。
rate[step 0.1%]の列に0.05%と書くと E114 で止まります。黙って近い刻みに寄せると、表で読める境界と生成コードの境界が食い違うからです。 - 率のまま計算して、最後に一度だけ丸めます。途中で丸めないのは、丸め方が業務の判断だからです。
点数を合算して、達成率でランクを付ける
お金がまったく出てこない例です。四つの評価項目を重み付きで足し、満点に対する達成率でランクを決めます。「表で書かれてはいないが、書き出せば表と少しの式で足りる」ルールの典型です。
rule 評価ランク(rank) v1
description "四つの評価項目を重み付きで合算し、満点に対する達成率でランクを決める。金額の出てこない例"
enum ランク(grade) = S(s) | A(a) | B(b) | C(c)
inputs
品質(quality) : number range >=0 <=10
納期(delivery) : number range >=0 <=10
価格(price) : number range >=0 <=10
対応(support) : number range >=0 <=10
outputs
評価(grade) : ランク
# 重みは 2:1:1:1、満点は 50 点
derive 合計点(total) : number = 品質 × 2 + 納期 + 価格 + 対応 range >=0 <=50
define 達成率(ratio) : rate = 合計点 ÷ 50
table ランク表(grade_table)
policy first
| 達成率 | -> 評価(grade) : ランク |
| >=90% | S |
| >=80% | A |
| >=60% | B |
| - | C |
result 評価 = 評価
examples
| 品質 | 納期 | 価格 | 対応 | -> 評価 |
| 10 | 10 | 10 | 10 | S |
| 9 | 8 | 8 | 7 | A |
| 6 | 6 | 6 | 6 | B |
| 3 | 3 | 3 | 3 | C |
この例が見せていること
deriveは入力どうしの足し算・引き算と整数倍でできた名前です。重み付きの合計はこれで書けます。define 達成率 : rate = 合計点 ÷ 50と宣言すると、表のセルに>=90%と割合のまま書けます。無次元の値を率と呼ぶか数と呼ぶかは、宣言する側が決めます。- 実行時に割り算は起きません。
>=90%は生成コードでは合計点 >= 45になります。満点が定数なので、境界が定数に畳めるからです。逆に満点が入力だと書けません — 変数で割ることになり、E115 で止まります（割合そのものをrateの入力で受け取ってください）。
単位のない数を返す
100 円につき 1 点。金額を金額で割ると単位が消えて、number（単位のない整数）になります。
rule ポイント付与(points) v1
description "会計 1 件で貯まる点数。100 円につき 1 点で、区分とキャンペーンで倍になる。単位のない数を使う例"
enum 会員区分(member_kind) = 一般(basic) | 上級(gold)
inputs
税込金額(paid) : money[円, incl_tax] range >=0円 <=100万円
区分(kind) : 会員区分
キャンペーン(campaign) : bool
outputs
点数(pts) : number round down(1)
# 100 円につき 1 点。端数は最後に一度だけ落とす（§7.2）
define 基本点(base) : number = 税込金額 ÷ 100円
define 倍付け(boost) : number = 基本点 × 2
table 点数表(pts_table)
policy unique
| 区分 | キャンペーン | -> 点数(pts) : number |
| 上級 | - | 倍付け |
| 一般 | true | 倍付け |
| 一般 | false | 基本点 |
result 点数 = 点数
examples
| 税込金額 | 区分 | キャンペーン | -> 点数 |
| 1050円 | 一般 | false | 10 |
| 1050円 | 上級 | false | 21 |
| 1050円 | 一般 | true | 21 |
| 99円 | 一般 | false | 0 |
この例が見せていること
numberは件数・日数・点数のような、単位を持たない整数のための型です。税込金額 ÷ 100円の割り算は整数を割りません。内部の刻みを 100 倍するだけなので、1050 円は 10.5 点のまま最後まで運ばれ、round down(1)が一度だけ 10 点に落とします。Python の//や Go の/の切り捨ての向きの違いが入り込む余地がありません。- 割り算は定数でだけ書けます。割る数が業務データなら、それは率か定数表として表に現れるはずです。
表を三段重ねて、出力を二つ返す
重量から重さ区分、重さ区分と会員区分から帯、帯と支払額から送料と倍率。前の表が出した値が、そのまま次の表の列になります。返るのは請求額とポイントの二つです。
rule 会員特典(member_perk) v1
description "会員区分と重量から請求額とポイントを一度に出す。出力が二つ、result が一本、率が表の列から来る例"
enum 会員(member) = 一般(basic) | 上位(gold)
enum 重さ区分(wclass) = 軽(light) | 中(mid) | 重(heavy)
enum 帯(tier) = ブロンズ(bronze) | シルバー(silver) | ゴールド(gold)
inputs
会員区分(m) : 会員
重量(weight) : mass[g] range >=1g <=20kg
商品合計(gross) : money[円, incl_tax] range >=0円 <=100万円
値引(off) : money[円, incl_tax] range >=0円 <=10万円
# 宣言順（請求額 → 付与点）と文字の並び順（付与点 → 請求額）がわざと逆。
# 生成コードの返す順序が言語ごとにぶれていないかは、この順序でしか出ない。
outputs
請求額(total) : money[円, incl_tax] round half_up(10円)
付与点(pts) : number round down(1)
derive 支払額(net) : money[円, incl_tax] = 商品合計 - 値引 range >=-10万円 <=100万円
# 金額を金額の定数で割ると単位が消えて number になる（§2.3）
define 基本点(base) : number = 商品合計 ÷ 100円
table 重さ判定(w_of)
policy first
| 重量 | -> 区分(wc) : 重さ区分 |
| <=2kg | 軽 |
| <=10kg | 中 |
| - | 重 |
table 帯判定(tier_of)
policy unique
| 区分 | 会員区分 | -> 帯(t) : 帯 |
| 軽 | 一般 | ブロンズ |
| 軽 | 上位 | シルバー |
| 中 | 一般 | シルバー |
| 中 | 上位 | ゴールド |
| 重 | - | ゴールド |
# 一つの表が二つの列を出し、そのうち率の列を下の define が使う。
# 率の刻み（10%）が列の保持スケールに入らないと、付与点が 10 倍になる。
table 送料表(ship)
policy unique
| 帯 | 支払額 | -> 送料(s) : money[円, incl_tax] | 倍率(r) : rate[step 10%] |
| ブロンズ | <3000円 | 800円 | 100% |
| ブロンズ | >=3000円 | 400円 | 100% |
| シルバー | - | 300円 | 120% |
| ゴールド | - | 0円 | 150% |
# 二つ目の出力は、その出力と同じ名前の define から取る（result は最初の出力にしか効かない）
define 付与点(pts) : number = 基本点 × 倍率
result 請求額 = max(支払額, 0円) + 送料
examples
| 会員区分 | 重量 | 商品合計 | 値引 | -> 請求額 | 付与点 |
| 一般 | 1kg | 2000円 | 500円 | 2300円 | 20 |
| 上位 | 5kg | 20000円 | 2000円 | 18000円 | 300 |
| 一般 | 15kg | 5000円 | 0円 | 5000円 | 75 |
この例が見せていること
- 前の表の出力は、後の表の列にそのまま書けます。 段数に上限はありません（検査の予算を超えたら E109 で止まります）。
rulec checkが落ちたときの「当てはまった行」も、表 重さ判定 行2 / 表 帯判定 行4 / 表 送料表 行4と段の数だけ出ます。 - 一つの表が出力列を複数持てます。
送料表は送料と倍率を同時に出し、下のdefineがその率を使います。率の刻み（step 10%）は列に入っても保たれるので、基本点 × 倍率は最後に一度だけ丸められます。 deriveが列になります。支払額 = 商品合計 − 値引を宣言してあるので、「値引き後の金額で判定する」が一本の式ではなく送料表の一つの列になります。resultが組み立てるのは最初の出力だけです（E015）。二つ目からは、その出力と同じ名前のdefineから取ります — ここではdefine 付与点。resultを二本書くと E016 で止まります。
並びを順にたどって、一つの答えに畳む
呼び出し側が運賃行を何件か渡し、規則が上から順に見ていきます。一件ごとの判定は表がして、fold がその判定ごとに「次へ」「打ち切り」「これを採る」「持ち越す」を書き分けます。件数の決まっていない入力を受けられる、ただ一つの形です。
rule 全国運賃(freight) v1
description "呼び出し側が渡す運賃行を順に見て、一つの運賃に畳む。並びをたどる規則の例"
enum 採用区分(verdict) = スキップ(skip) | 打ち切り(halt) | 確定(take) | 持ち越し(hold)
enum ゾーン区分(zone) = 近畿圏(kinki) | 遠隔地(remote)
# 一件ぶんの欄。呼び出し側はこの欄のそろった要素を何件でも渡す
elements 運賃行(freight_rows)
行ゾーン(row_zone) : ゾーン区分
閾値(threshold) : money[円, incl_tax] range >=0円 <=100万円
行運賃(row_fee) : money[円, incl_tax] range >=0円 <=10万円
outputs
運賃(fee) : money[円, incl_tax] round up(1円)
# 一件の要素に対する判定。表の検査はいままでどおり効く（この四行で 採用区分 を覆いきる）
table 行判定(row_of)
policy unique
| 行ゾーン | 閾値 | -> 採用(verdict) : 採用区分 |
| 近畿圏 | <=1000円 | 確定 |
| 近畿圏 | >1000円 | 持ち越し |
| 遠隔地 | <=1000円 | スキップ |
| 遠隔地 | >1000円 | 打ち切り |
# 判定ごとの行き先。どの判定にも行き先が要る（E024）
fold 採用 over 運賃行
スキップ -> next
打ち切り -> stop with 0円
確定 -> take_unique 行運賃
持ち越し -> keep_max 行運賃 by 閾値
empty -> 0円
exhausted -> held
sequence 近い一件(near)
| 行ゾーン | 閾値 | 行運賃 |
| 近畿圏 | 500円 | 800円 |
| 近畿圏 | 2000円 | 1500円 |
sequence 空(none)
| 行ゾーン | 閾値 | 行運賃 |
examples
| 運賃行 | -> 運賃 |
| 近い一件 | 800円 |
| 空 | 0円 |
この例が見せていること
elementsが一件ぶんの欄を宣言します。 書き方はinputsと同じで、範囲も単位もそのまま効きます。呼び出し側は、この欄のそろった要素を何件でも渡します。- 表の検査はいままでどおりです。 一件の要素が一件の判定なので、完全性も重なりも単位も、これまでと同じように証明されます。上の表は
採用区分の四つの値を過不足なく出します。 foldは、判定ごとの行き先を書くところです。next（次へ）、stop with <値>（そこで打ち切る）、take_unique <値>（一件だけ採る。二件当たれば実行時にエラー）、keep_max <値> by <鍵>（鍵がいちばん大きいものを持ち越す）。行き先の無い判定があれば E024 で止まります。- 要素ゼロ件のときと、最後まで見終えたときの答えは必須です（E022・E023）。空の並びは必ず来ますし、「持ち越していたものを返す」も書いて初めて決まります（
exhausted -> held）。 - 例は
sequenceに名前を付けて指します。 例のセルに書けるのは値一つなので、並びのほうに名前を付けます。行がゼロ本のsequenceが、要素ゼロ件の例です。 - SQL と NumPy には生成しません。 一つの問い合わせには、行から行へ値を持ち越して途中で打ち切る場所がないからです。NumPy のほうは、要素から要素へ状態を運ぶ走査が列の演算ではないからです。ほかの対象には出て、参照評価器と一致することを毎回確かめています。
並びを数えて、その数で判定する
請求書の宛名を、取引先台帳の候補と一件ずつ照合します。判定するのは表で、count がその判定に当てはまった件数を数え、次の表がその数で手続きを決めます。「一件なら自動、複数なら目視」を、人が数えてから渡すのではなく、規則の中で決められます。
rule 納入先照合(supplier_match) v1
description "請求書の宛名を取引先台帳と一件ずつ照合し、一致した件数で次の手を決める。並びを数える例"
enum 照合(match_kind) = 一致(same) | 不一致(diff)
enum 次の手(action_kind) = 新規登録(register) | 自動確定(auto) | 目視確認(review)
inputs
自動確定可(auto_ok) : bool
# 台帳の候補。一件ぶんの欄で、呼び出し側は何件でも渡す
elements 候補(candidates)
会社名一致(name_match) : bool
住所一致(addr_match) : bool
outputs
手続き(action) : 次の手
# 一件の候補に対する判定。表の検査はいままでどおり効く
table 候補判定(row_of)
policy unique
| 会社名一致 | 住所一致 | -> 照合結果(kind) : 照合 |
| true | true | 一致 |
| true | false | 不一致 |
| false | - | 不一致 |
# 歩いたあとに残るのは数だけ。範囲は完全性の全体集合であり、並びの長さの上限でもある
count 一致数(hits) over 候補 where 照合結果 = 一致 range >=0 <=50
table 手続き判定(action_of)
policy unique
| 一致数 | 自動確定可 | -> 手続き(action) : 次の手 |
| 0 | - | 新規登録 |
| 1 | true | 自動確定 |
| 1 | false | 目視確認 |
| >=2 | - | 目視確認 |
sequence 一件だけ一致(one)
| 会社名一致 | 住所一致 |
| true | true |
| true | false |
sequence 二件一致(two)
| 会社名一致 | 住所一致 |
| true | true |
| true | true |
sequence 候補なし(none)
| 会社名一致 | 住所一致 |
examples
| 自動確定可 | 候補 | -> 手続き |
| true | 一件だけ一致 | 自動確定 |
| false | 一件だけ一致 | 目視確認 |
| true | 二件一致 | 目視確認 |
| true | 候補なし | 新規登録 |
この例が見せていること
countは歩いたあとに残る数です。count 一致数(hits) over 候補 where 照合結果 = 一致は、要素ごとの判定が一致だった件数。そこから先はnumberの値なので、表の列に置けます。- 数を判定に変えるのは、ふつうの表です。
0/1/>=2の境界に穴や重なりがあれば、いつもどおり検査が止めます。数えることと、数から決めることが、別々に検査に掛かります。 - 範囲は二つの意味を持ちます（
range >=0 <=50）。完全性の検査が見る全体集合であり、並びの長さの上限でもあります。51 件渡すと、生成コードが入口で受け付けません — 範囲外の数を受け付けないのと同じことです。 - 数えるのは
count、足すのはsumです（下の「明細を足し上げる」）。平均は、丸めの中で合計を件数で割って出します（下の「値で割る：平均単価」）。 foldとcountは一つの規則に一緒に書けます。 並びが二本以上あっても、一回目にたどって求めた値を二回目に読んでも構いません（下の「二つの並びと二回目の歩き」）。止まるのは、一つの項目が二つの並びの要素を読むとき（E031）です。
明細を足し上げる
「合計 5,000 円以上で送料無料」。何件あるか分からない明細を歩いて金額を足し、その合計で送料を決めます。count が件数を残すのと同じ場所に、sum は額を残します。
rule 買物かごの送料(cart_shipping) v1
description "明細の金額を合計して送料を決める。並びを合計する例"
enum 会員区分(tier) = 一般(regular) | 優待(premium)
inputs
区分(tier) : 会員区分
# 一件ぶんの明細。呼び出し側は何件でも渡す
elements 明細(lines)
金額(amount) : money[円] range >=0円 <=100000円
# 歩いたあとに残るのは合計だけ。範囲は完全性の全体集合であり、走っている途中の合計が
# ここを出た時点で入口が受け付けなくなる境目でもある
sum 合計(total) over 明細 of 金額 range >=0円 <=1000000円
outputs
送料(fee) : money[円] round up(1円)
table 送料表(fee_table)
policy unique
| 合計 | 区分 | -> 送料(fee) : money[円] |
| >=5000円 | - | 0円 |
| >=3000円 <5000円 | 優待 | 0円 |
| >=3000円 <5000円 | 一般 | 250円 |
| <3000円 | - | 500円 |
examples
| 明細 | 区分 | -> 送料 |
| 二点 | 一般 | 0円 |
| 二点 | 優待 | 0円 |
| 少額 | 一般 | 500円 |
| 中くらい | 一般 | 250円 |
| 中くらい | 優待 | 0円 |
| 空 | 一般 | 500円 |
sequence 二点(two)
| 金額 |
| 3000円 |
| 2500円 |
sequence 少額(small)
| 金額 |
| 1200円 |
sequence 中くらい(middle)
| 金額 |
| 2000円 |
| 1500円 |
sequence 空(empty)
| 金額 |
この例が見せていること
sum 合計(total) over 明細 of 金額が残すのは一つの額です。 そこから先はふつうの列なので、>=5000円が軸の境目になり、完全性も重なりもいつもどおり止まります。- 足す列は負になれません（E029）。走っている途中の合計が上がる一方だから、宣言範囲を出た瞬間に入口でエラーにできて、長さの分からない並びについても int64 の主張が本当になります。差を取りたいなら、非負の列を二つ足して引きます。
- 平均は、丸めの中で割って出します。 合計を件数で割るのは値で割ることなので、
half_up(合計 / max(件数, 1), 1円)のように丸めのいちばん外側に書きます（下の「値で割る：平均単価」）。
品番の頭で振り分ける
SKU の前置きで冷凍・冷蔵・常温を決めます。文字列の列に書けるのは前方一致だけで、それ以外は書けません。
rule 品番の扱い(sku_handling) v1
description "品番の前置きと箱数で、輸送の扱いを決める。文字列の前方一致の例"
enum 扱い(handling) = 冷凍便(frozen) | 冷蔵便(chilled) | 常温便(ambient) | 常温混載(ambient_mixed)
inputs
品番(sku) : string
箱数(boxes) : number range >=1 <=200
outputs
扱い(handling) : 扱い
# 文字列は数え上げられないので、切れるのは前置きだけ。前置きの集合は有限なので、
# 完全性も重なりも、列挙の列とまったく同じように止まる
table 扱い表(handling_of)
policy first
| 品番 | 箱数 | -> 扱い(handling) : 扱い |
| starts_with "FZ-" | - | 冷凍便 |
| starts_with "CH-", "CL-" | - | 冷蔵便 |
| - | >=20 | 常温便 |
| - | <20 | 常温混載 |
examples
| 品番 | 箱数 | -> 扱い |
| "FZ-1001" | 1 | 冷凍便 |
| "CH-2002" | 5 | 冷蔵便 |
| "CL-0003" | 5 | 冷蔵便 |
| "AB-0004" | 30 | 常温便 |
| "AB-0004" | 3 | 常温混載 |
この例が見せていること
- 前置きの集合は有限に切れます。 文字列の全体は無限でも、その列のセルに書かれた前置きから作られる分割は有限なので、§6.2 の仕組みがそのまま動きます — 穴があれば、それを起こす文字列がそのまま返ってきます。
- 比べるのはバイトです。 大文字小文字も Unicode 正規化もしません。そうしないと 12 言語が同じ答えを返しません。
- 等号も集合も書けません（E110）。値が数えられるなら
enumのほうが向いています。部分一致と正規表現はありません。
比で配る按分
値引き総額を、明細に定価の比で割り付けます。上の「一件ずつに割る」が順に充てていく形なら、こちらは比で配る形です。一行ぶんは「ここまでの配分」から「直前までの配分」を引いた差になります。
rule 比例配分(pro_rata) v1
description "一括値引きを明細に定価の比で割り付ける。1 明細 = 1 回の判定で、累計は呼び出し側が持つ。端数は最後の明細に寄り、配った合計はかならず値引き総額に一致する"
inputs
値引き総額(total_off) : money[円] range >=0円 <=100万円
直前までの定価(before) : money[円] range >=0円 <=1000万円
ここまでの定価(upto) : money[円] range >=0円 <=1000万円
定価合計(base) : money[円] range >=1円 <=1000万円
対象(eligible) : bool
constraint 直前までの定価 <= ここまでの定価
constraint ここまでの定価 <= 定価合計
outputs
配分額(share) : money[円] round down(1円) range >=0円 <=100万円
derive 直前までの配分(to_before) : money[円] = allocate(値引き総額, 直前までの定価, 定価合計) range >=0円 <=100万円
derive ここまでの配分(to_upto) : money[円] = allocate(値引き総額, ここまでの定価, 定価合計) range >=0円 <=100万円
define 差分(gap) : money[円] = ここまでの配分 - 直前までの配分
table 配分可否(applies)
policy unique
| 対象 | -> 配る(on) : money[円] |
| true | 差分 |
| false | 0円 |
result 配分額 = 配る
examples
| 値引き総額 | 直前までの定価 | ここまでの定価 | 定価合計 | 対象 | -> 配分額 |
| 1000円 | 0円 | 3000円 | 10000円 | true | 300円 |
| 1000円 | 3000円 | 10000円 | 10000円 | true | 700円 |
| 100円 | 0円 | 333円 | 1000円 | true | 33円 |
| 100円 | 333円 | 666円 | 1000円 | true | 33円 |
| 100円 | 666円 | 1000円 | 1000円 | true | 34円 |
| 0円 | 0円 | 500円 | 1000円 | true | 0円 |
| 1000円 | 0円 | 3000円 | 10000円 | false | 0円 |
この例が見せていること
allocate(配る額, 累計, 全体)は、値で割ります。 答えは配る額 × 累計 ÷ 全体を下に丸めた値で、単位の整数になります。ほかに値で割れるのは、丸めの中のいちばん外側の割り算だけです。- 差にすると、配った合計が総額にぴったり一致します。 隣り合う行で同じ値が足されて引かれるので、端数は最後の行に寄ります。
proofs/に定理があります（runTotal_exact）。 constraint 累計 <= 全体が要ります（E117）。これが無いと配る分が配る額を超えることがあり、区間も二つの範囲の積になってしまいます。制約は二行に分けて書いても、つながって効きます。- 出力の行に書いた
rangeを、検査が確かめます。range >=0円 <=100万円は、どの明細の配分額も 0 円を下回らず、値引き総額を超えないという約束です。rulec checkは、配分額がとりうる値がこの範囲に収まることを確かめ、収まらなければ E140 で止まります。二つのallocateは同じ額を同じ全体で配り、累計の順は制約が決めているので、差は 0 以上で配る額以下だと読めます。
呼び出し側の注文から入力を取る（JSON Schema）
注文オブジェクトから送料を決めます。呼び出し側はもう JSON Schema で注文の形を決めているので、それを shape で借り、入力ごとにその中のどこから来るかを from で書きます。表そのものは、ほかの例と同じ平たい入力の表です。
rule 注文の送料(order_shipping) v1
description "注文オブジェクトから送料を決める。呼び出し側の契約から入力を取り出す例（§15.125）"
# 呼び出し側はもう JSON Schema で注文の形を決めている。それを借りて、入力がその形の
# どこから来るかを書くと、平たくするコードは生成され、パスは毎回の check で契約に照らされる。
shape 注文(order) = jsonschema "contracts/order.schema.json" "#/$defs/Order"
enum 地域(zone) = honshu(honshu) | hokkaido(hokkaido) | okinawa(okinawa)
inputs
あて先(zone) : 地域 from 注文.shipping.zone
冷蔵あり(cold) : bool from any 注文.lines where chilled = true
明細数(lines) : number range >=1 <=50 from count 注文.lines
outputs
送料(fee) : money[円] round up(10円)
# 冷蔵は地域を問わず 500円 増し、明細が 10 件を超えると 200円 増し。
table 地域別(by_zone)
policy unique
| あて先 | -> 地域料(zone_fee) : money[円] |
| honshu | 800円 |
| hokkaido | 1200円 |
| okinawa | 1500円 |
table 冷蔵加算(cold_extra)
policy unique
| 冷蔵あり | -> 冷蔵料(cold_fee) : money[円] |
| true | 500円 |
| false | 0円 |
table 件数加算(bulk_extra)
policy unique
| 明細数 | -> 件数料(bulk_fee) : money[円] |
| >10 | 200円 |
| <=10 | 0円 |
define 合計(total) : money[円] = 地域料 + 冷蔵料 + 件数料
result 送料 = 合計
examples
| あて先 | 冷蔵あり | 明細数 | -> 送料 |
| honshu | false | 1 | 800円 |
| honshu | true | 1 | 1300円 |
| okinawa | true | 11 | 2200円 |
| hokkaido | false | 10 | 1200円 |
規則が読む契約（contracts/order.schema.json）:
{
"$schema": "https://json-schema.org/draft/2020-12/schema",
"title": "Order",
"$defs": {
"Order": {
"type": "object",
"properties": {
"id": { "type": "string" },
"shipping": { "$ref": "#/$defs/Shipping" },
"lines": { "type": "array", "minItems": 1, "maxItems": 50, "items": { "$ref": "#/$defs/Line" } }
},
"required": ["shipping", "lines"]
},
"Shipping": {
"type": "object",
"properties": {
"zone": { "type": "string", "enum": ["honshu", "hokkaido", "okinawa"] },
"postcode": { "type": "string" }
},
"required": ["zone"]
},
"Line": {
"type": "object",
"properties": {
"sku": { "type": "string" },
"chilled": { "type": "boolean" },
"amount_jpy": { "type": "integer" }
},
"required": ["sku", "chilled", "amount_jpy"]
}
}
}
この例が見せていること
fromの形は七つです。 フィールドの値（from 注文.shipping.zone）、要素のどれかが当てはまるか（from any 注文.lines where chilled = true）、全部が当てはまるか（from all …）、何件あるか（from count 注文.lines）、フィールドの合計（from sum 注文.lines of amount_usd）、いちばん大きい値と小さい値（from max …・from min …。要素が無いときの値はemptyに書きます）。結合や量化のネストは書けません。rulec genはorder_shipping_from(order)も書きます。 注文オブジェクトをそのまま渡すと、入力を取り出して規則を呼びます。この関数が出るのは、読み込んだ JSON を連想配列のまま使うことの多い Python・TypeScript・JavaScript・Ruby・PHP です。Go・Swift・Java・Rust・SQL・NumPy・Wasm には出ません。- パスは
rulec checkのたびに契約に照らされます。 契約に無いフィールドを書けば E121 で、どこまで届いたかと、そこにあったフィールドを言います。型が合わなければ E120 です。 - 契約の検証も、入力の宣言と突き合わせます。 契約は
linesを 1〜50 件（minItems・maxItems）に限っていて、規則の明細数のrange >=1 <=50と同じです。maxItemsを消すと、51 件の注文は契約を通るのに規則は受け付けないので、E122 で止まります。fix.textは契約に書き足すキーワード（"minItems": 1, "maxItems": 50）そのものです。 - 表の検査には触れません。 射影から出てくるのはただのスカラーの入力で、完全性も重なりも、
fromが無いときと同じに決まります。
Connect のリクエストから入力を取る（.proto と Protovalidate）
出荷のリクエストから送料を決めます。リクエストの形は .proto で決まっていて、フィールドには Protovalidate の注釈が付いています。規則はその .proto を借り、入力の宣言を注釈とそろえてあります。
rule 出荷の送料(shipment_fee) v1
description "出荷の要求（.proto）から送料を決める。Protovalidate の注釈と入力の宣言をそろえた例（§15.132、§15.133）"
# 呼び出し側は Connect のサービスで、要求の形は .proto で決まっている。それを借りて、入力が
# 要求のどこから来るかを書く。生成する shipment_fee_from は、protojson で届いた要求をそのまま読む。
shape 出荷(shipment) = proto "contracts/shipment.proto" shop.v1.CreateShipmentRequest
enum 地域(region) = honshu(honshu) | hokkaido(hokkaido) | okinawa(okinawa)
enum 時間帯(window) = morning(morning) | evening(evening)
inputs
あて先(region) : 地域 from 出荷.destination.region
割れ物あり(fragile) : bool from any 出荷.parcels where handling = HANDLING_FRAGILE
個数(parcels) : number range >=1 <=20 from count 出荷.parcels
申告額(declared) : money[円] range >=0円 <=100万円 from 出荷.declared_value_jpy
時間帯(window) : 時間帯? from 出荷.delivery_window
outputs
送料(fee) : money[円] round up(10円)
# 一個あたりの運賃に個数を掛け、割れ物・補償・時間帯指定の加算を足す。
table 地域別(by_region)
policy unique
| あて先 | -> 一個の運賃(per_parcel) : money[円] |
| honshu | 800円 |
| hokkaido | 1200円 |
| okinawa | 1500円 |
table 割れ物加算(fragile_extra)
policy unique
| 割れ物あり | -> 割れ物料(fragile_fee) : money[円] |
| true | 300円 |
| false | 0円 |
table 補償(insurance)
policy unique
| 申告額 | -> 補償料(insurance_fee) : money[円] |
| <=3万円 | 0円 |
| >3万円 <=10万円 | 200円 |
| >10万円 | 500円 |
table 時間帯指定(window_extra)
policy unique
| 時間帯 | -> 指定料(window_fee) : money[円] |
| none | 0円 |
| morning, evening | 100円 |
define 合計(total) : money[円] = 一個の運賃 × 個数 + 割れ物料 + 補償料 + 指定料
result 送料 = 合計
examples
| あて先 | 割れ物あり | 個数 | 申告額 | 時間帯 | -> 送料 |
| honshu | false | 1 | 0円 | none | 800円 |
| hokkaido | true | 2 | 5万円 | none | 2900円 |
| okinawa | false | 3 | 20万円 | evening | 5100円 |
| honshu | true | 20 | 100万円 | morning | 16900円 |
規則が読む契約（contracts/shipment.proto）:
syntax = "proto3";
package shop.v1;
import "buf/validate/validate.proto";
// The request the shipping service takes, validated by Protovalidate before anything reads it.
message CreateShipmentRequest {
Destination destination = 1 [(buf.validate.field).required = true];
repeated Parcel parcels = 2 [(buf.validate.field).repeated = {min_items: 1, max_items: 20}];
int64 declared_value_jpy = 3 [(buf.validate.field).int64 = {gte: 0, lte: 1000000}];
optional string delivery_window = 4 [(buf.validate.field).string = {in: ["morning", "evening"]}];
}
message Destination {
string region = 1 [(buf.validate.field).string = {in: ["honshu", "hokkaido", "okinawa"]}];
string postcode = 2;
}
message Parcel {
int64 weight_g = 1 [(buf.validate.field).int64 = {gte: 1, lte: 30000}];
Handling handling = 2;
}
enum Handling {
HANDLING_STANDARD = 0;
HANDLING_FRAGILE = 1;
}
この例が見せていること
- 生成する
shipment_fee_fromは、protojson の JSON をそのまま読みます。 フィールドは lowerCamelCase の名前（declaredValueJpy）でも.protoに書いた名前（declared_value_jpy）でも読み、省かれたフィールドは proto の既定値として読みます。int64 は文字列で届いても、数として読みます。 optionalのフィールドはT?の入力で受けます。delivery_windowは送られないことがあるので時間帯?にして、無いとき（none）の行を表に書いています。- 列挙のフィールドは、
whereで値の名前を比べます。handlingは.protoの列挙で、protojson は値の名前（HANDLING_FRAGILE）を運びます。番号 0 の値（HANDLING_STANDARD）のときはフィールドごと省かれますが、そのときもHANDLING_STANDARDとして読みます。 - 注釈と宣言がそろっているので、
checkは通ります。destinationからrequired = trueを外すと、リクエストはdestinationを省けるようになり、そのときregionは""として届きます。地域は""を受け付けないので E122 で止まり、fix.textは[(buf.validate.field).required = true]です。
契約がフィールドのあいだに置く条件（CEL）
見積のリクエストから運賃を決めます。リクエストを検証する .proto は、Protovalidate の CEL で二つのことを約束しています。速達は 5kg まで、申告額は補償額を超えない、の二つです。規則はその約束に乗って書いてあります。
rule 速達の見積(express_quote) v1
description "見積の要求（.proto）から運賃を決める。契約がフィールドのあいだに置く条件を、規則の制約と行に照らす例（§15.140）"
# 呼び出し側の契約は、速達を 5kg までに限り、申告額が補償額を超えないことを CEL で約束している。
# 規則はその約束を constraint に書き、補償料の表はそれに頼って、申告額が補償額を超える行を持たない。
shape 見積(quote) = proto "contracts/quote.proto" shop.v1.QuoteRequest
inputs
重さ(weight) : mass[g] range >=1g <=30kg from 見積.weight_g
速達(express) : bool from 見積.express
申告額(declared) : money[円] range >=0円 <=30万円 from 見積.declared_jpy
補償額(cover) : money[円] range >=0円 <=30万円 from 見積.cover_jpy
constraint 申告額 <= 補償額
outputs
運賃(fee) : money[円] round up(10円)
# 速達は 2kg を境に二段。契約が 5kg を超える速達を通さないので、その先の行は書かない。
table 重さ別(by_weight)
policy unique
| 速達 | 重さ | -> 基本料(base) : money[円] |
| false | <=2kg | 700円 |
| false | >2kg <=10kg | 1100円 |
| false | >10kg | 1600円 |
| true | <=2kg | 1200円 |
| true | >2kg | 1800円 |
table 補償(insurance)
policy unique
| 申告額 | 補償額 | -> 補償料(cover_charge) : money[円] |
| <=5万円 | <=5万円 | 0円 |
| <=5万円 | >5万円 | 300円 |
| >5万円 | >5万円 | 600円 |
define 合計(total) : money[円] = 基本料 + 補償料
result 運賃 = 合計
examples
| 重さ | 速達 | 申告額 | 補償額 | -> 運賃 |
| 1kg | false | 0円 | 0円 | 700円 |
| 3kg | true | 2万円 | 10万円 | 2100円 |
| 12kg | false | 8万円 | 10万円 | 2200円 |
| 2kg | true | 5万円 | 5万円 | 1200円 |
規則が読む契約（contracts/quote.proto）:
syntax = "proto3";
package shop.v1;
import "buf/validate/validate.proto";
// A quote for one parcel, validated by Protovalidate before anything reads it. Two of its
// rules relate one field to another: express takes a parcel of up to 5 kg, and the value
// declared never exceeds the cover the caller chose.
message QuoteRequest {
option (buf.validate.message).cel = {
id: "express_weight",
message: "express takes a parcel of up to 5 kg",
expression: "!this.express || this.weight_g <= 5000"
};
option (buf.validate.message).cel = {
id: "declared_within_cover",
message: "the declared value exceeds the cover",
expression: "this.declared_jpy <= this.cover_jpy"
};
int64 weight_g = 1 [(buf.validate.field).int64 = {gte: 1, lte: 30000}];
bool express = 2;
int64 declared_jpy = 3 [(buf.validate.field).int64 = {gte: 0, lte: 300000}];
int64 cover_jpy = 4 [(buf.validate.field).int64 = {gte: 0, lte: 300000}];
}
この例が見せていること
constraint 申告額 <= 補償額は、契約が約束しているから書けます。 補償料の表には、申告額が補償額を超える行がありません。制約があるので、完全性の検査はその組み合わせに行を求めません。契約の CEL（this.declared_jpy <= this.cover_jpy）が同じことを約束しているので、checkは通ります。制約を<にすると、契約は申告額と補償額が等しいリクエストを通すので E123 で止まり、そのリクエストを例に出します。- 5kg を超える速達の行は書いていません。 契約の
!this.express || this.weight_g <= 5000が、そのリクエストを通さないからです。書き足すと、その行は W124 になります。セルを一つずつ見れば契約の通す値なのに、組み合わせとしては通らない行だからです。 - CEL は、読める部分を読みます。 整数の一次式の比較、
in、size()、has()、&&・||・!・? :です。剰余や文字列の関数のように読めない部分は真として扱うので、見逃すことはありません。
続いていく注文の、一回のイベント（machine）
通販の注文が、入金・出荷・配達・取消依頼のイベントでどの状態に移り、いくら返金するかを決めます。状態は呼び出す側が持ちます（データベースの注文の行など）。規則は今の状態と一つのイベントを受け取って次の状態を返す純関数のままで、machine の節が、その関数を何回続けて呼んでも崩れないことを言います。
rule 注文の状態(order_state) v1
description "通販の注文が、入金・出荷・配達・取消依頼の出来事でどの状態に移り、いくら返金するか。状態は呼び出す側が持ち、規則は一回の出来事だけを判定する。書き下ろしの例"
enum 状態(state) = 受付(received) | 入金済(paid) | 出荷済(shipped) | 配達済(delivered) | 取消(cancelled)
enum 出来事(event) = 入金(pay) | 出荷(ship) | 配達(deliver) | 取消依頼(cancel)
inputs
状態(state) : 状態
出来事(event) : 出来事
支払額(paid) : money[円, incl_tax] range >=0円 <=100万円
outputs
次の状態(next_state) : 状態
返金額(refund) : money[円, incl_tax] round down(1円)
受理(accepted) : bool
table 遷移(step)
policy unique
| 状態 | 出来事 | -> 次の状態 | 返金額 | 受理 |
| 受付 | 入金 | 入金済 | 0円 | true |
| 受付 | 取消依頼 | 取消 | 0円 | true |
| 受付 | 出荷, 配達 | 状態 | 0円 | false |
| 入金済 | 出荷 | 出荷済 | 0円 | true |
| 入金済 | 取消依頼 | 取消 | 支払額 | true |
| 入金済 | 入金, 配達 | 状態 | 0円 | false |
| 出荷済 | 配達 | 配達済 | 0円 | true |
| 出荷済 | 入金, 出荷, 取消依頼 | 状態 | 0円 | false | # 出荷のあとの取消は、返品の手続きで受ける
| 配達済 | - | 状態 | 0円 | false |
| 取消 | - | 状態 | 0円 | false | # 取消のあとに届いた入金の通知では、注文を戻さない
machine 注文(order) over 遷移
carry 状態 -> 次の状態
held 支払額
initial 受付
final 配達済, 取消
never 出荷済 after 取消
once 返金額 >0円
scenario 配達まで(delivered)
| 出来事 | 支払額 | -> 次の状態 | 返金額 | 受理 |
| 入金 | 3000円 | 入金済 | 0円 | true |
| 出荷 | 3000円 | 出荷済 | 0円 | true |
| 配達 | 3000円 | 配達済 | 0円 | true |
scenario 取消のあとの入金(late_pay)
| 出来事 | 支払額 | -> 次の状態 | 返金額 | 受理 |
| 入金 | 3000円 | 入金済 | 0円 | true |
| 取消依頼 | 3000円 | 取消 | 3000円 | true |
| 入金 | 3000円 | 取消 | 0円 | false |
examples
| 状態 | 出来事 | 支払額 | -> 次の状態 | 返金額 | 受理 |
| 受付 | 取消依頼 | 0円 | 取消 | 0円 | true |
| 出荷済 | 取消依頼 | 3000円 | 出荷済 | 0円 | false |
この例が見せていること
- 意味として新しいのは
carry 状態 -> 次の状態の一行だけです。 この呼び出しが返した次の状態を、次の呼び出しでは状態として渡す、という宣言です。表はふつうの表で、完全性の検査が「出荷のあとに取消依頼が来たら」の行を求めます。出力のセルの状態は、状態をそのまま返すという意味です。 held 支払額は、呼び出す側が守る約束です。 一つの注文は、どの呼び出しにも同じ支払額を渡します。constraintが起きない組み合わせを言うのと同じように、主張はこの約束を守る呼び出しの並びについてのものになり、途中で支払額を変える並びが反例に出ることはありません。final・never・onceは、呼び出しのあらゆる並びについての主張です。 最後の行を、取消のあとに届いた入金で注文を入金済に戻す行に書き換えると、checkは三つのエラーで止まります。終わったはずの取消から出ていく（E124）、取消依頼・入金・出荷の三回で取消のあとに出荷済に着く（E126）、四回の呼び出しで二度返金する（E127）。どれも、崩す最短の呼び出しの並びつきです。一行ずつ読めば、どの行ももっともらしく見えます。scenarioは、何回かの呼び出しにわたる例です。 持ち越す状態の列はありません。一行目はinitialの受付から始まり、二行目からは一つ前が答えた状態から始まります。- 生成コードには、始まりの状態と、終わったかどうかの判定が付きます（Python なら
INITIALとis_final）。ベクタには呼び出しの並びが加わり、rulec testは各言語に、自分が返した状態をそのまま次の呼び出しへ渡させて照合します。 - 改定の差分は、処理中の案件の言葉で出ます。 二つの版の
rulec diffは、違う答えを返す最短の呼び出しの並びと、改定のあとで終わりの状態に行けなくなる状態を言います。replayは、過去のログをtagごとに一つの案件として、新しい版に通し直します。
会員の段階で送料が変わる
会員の段階（一般 < シルバー < ゴールド < プラチナ）に順があり、表のセルは段階と比べます。キャンペーンは、その注文に限って会員をキャンペーンの段階まで引き上げます。
rule 会員段階の送料(tier_shipping) v1
description "会員の段階で決まる送料。ゴールドから上は無料で、キャンペーンはその注文に限って会員をキャンペーンの段階まで引き上げる"
# 段階は低い順に並べる。セルは段階と比べられる（`>=ゴールド`）。
enum 段階(tier) = 一般(basic) < シルバー(silver) < ゴールド(gold) < プラチナ(platinum)
inputs
会員(member) : 段階 # 会員自身の段階
キャンペーン(campaign) : 段階 range >=一般 <=ゴールド # キャンペーンが引き上げるのはゴールドまで
小計(subtotal) : money[USD] range >=0USD <=100000USD
outputs
送料(shipping) : money[USD] round down(1USD)
適用段階(effective) : 段階
引き上げ(lifted) : bool
# 二つの段階のうち後のほうで送る。
define 適用段階 : 段階 = max(会員, キャンペーン)
define 引き上げ : bool = キャンペーン > 会員
table 送料表(shipping_fee)
policy unique
| 適用段階 | 小計 | -> 送料 |
| >=ゴールド | - | 0USD |
| シルバー | >=50USD | 0USD |
| シルバー | <50USD | 5USD |
| 一般 | >=100USD | 0USD |
| 一般 | <100USD | 8USD |
examples
| 会員 | キャンペーン | 小計 | -> 送料 | 適用段階 | 引き上げ |
| プラチナ | 一般 | 10USD | 0USD | プラチナ | false |
| 一般 | ゴールド | 10USD | 0USD | ゴールド | true |
| シルバー | 一般 | 60USD | 0USD | シルバー | false |
| シルバー | シルバー | 10USD | 5USD | シルバー | false |
| 一般 | 一般 | 99USD | 8USD | 一般 | false |
この例が見せていること
enum 段階 = 一般 < シルバー < ゴールド < プラチナと<で書くと、値に順が付きます。セルの>=ゴールドは「ゴールド以上」で、ゴールドとプラチナの二つを覆います。max(会員, キャンペーン)は二つの段階のうち後の方、キャンペーン > 会員は真偽の値です。- 入力の範囲も段階で書けます。キャンペーンは
range >=一般 <=ゴールドなので、プラチナへは引き上げません。範囲の外の値は、生成したコードの入口が拒みます。
二つの規則が一つの列挙を分け合う
品目と配送の地域の列挙は、enums のファイル shared/品目.rule にだけ書いてあり、送料と返品の二つの規則が import enum で読みます。
rule 品目の送料(goods_shipping) v1
description "荷物の配送料。届け先までの遠さと重さで決まり、壊れ物には上乗せがある"
# 種類と地域は品目のファイルのもので、順、表示名、グループの「壊れ物」もそこから来る。
# この規則はどれも書き直さない。
import enum 種類 from "shared/品目.rule"
import enum 地域 from "shared/品目.rule"
inputs
品目(goods) : 種類
届け先(destination) : 地域
重さ(weight) : mass[kg] range >=1kg <=30kg
outputs
配送料(fee) : money[USD] round up(1USD)
table 基本料金(base_fee)
policy unique
| 届け先 | 重さ | -> 基本(base) : money[USD] |
| <=地方 | <=5kg | 5USD |
| <=地方 | >5kg | 9USD |
| 全国 | <=5kg | 8USD |
| 全国 | >5kg | 14USD |
| 海外 | - | 30USD |
# 壊れ物は手で梱包し、遠くへ送るほど梱包の費用がかかる。
table 取扱い(handling)
policy unique
| 品目 | 届け先 | -> 上乗せ(surcharge) : money[USD] |
| 壊れ物 | <全国 | 3USD |
| 壊れ物 | >=全国 | 7USD |
| 食品, 衣料 | - | 0USD |
define 配送料 : money[USD] = 基本 + 上乗せ
examples
| 品目 | 届け先 | 重さ | -> 配送料 |
| 食品 | 市内 | 2kg | 5USD |
| 衣料 | 地方 | 6kg | 9USD |
| 電子機器 | 全国 | 10kg | 21USD |
| 家具 | 海外 | 20kg | 37USD |
| 電子機器 | 地方 | 1kg | 8USD |
この例が見せていること
- 見出しが
enumsのファイルは、列挙と群だけを持ち、何も決めません。規則はimport enum 種類 from "shared/品目.rule"で読み、値・順・表示名・群をそのまま使います。 - 地域は順のある列挙（
市内 < 地方 < 全国 < 海外）で、<=地方のように比べます。種類と地域には表示名（食品(food) "食品・飲料"）が付き、ページと、生成コードの表示名の関数に出ます。 - 二つの規則の生成コードは、同じ型を使います。列挙の型だけのモジュールを
rulec genが書き、二つの規則のモジュールがそれを import します。
値で割る：平均単価
合計を個数で割って平均を出します。値で割れるのは丸めの中のいちばん外側だけで、割る数が 0 になりうると E132 で止まります。
rule 平均単価の場合分け(average_price_split) v1
description "注文の品の平均の単価を、品の無い注文を表で分けて出す。一つめの表が割る数を選ぶ。品があればその個数、無ければ 1 なので、割り算が 0 に当たることはない。もう一つの表が、品の無い注文の平均を 0 円にする"
inputs
合計(total) : money[円] range >=0円 <=100万円
個数(units) : number range >=0 <=1000
outputs
平均(average) : money[円] round half_up(1円)
# 行2 は、セルが 個数 を 1 以上に保つところでだけ 個数 を書くので、割る数 は 0 にならない。
table 割る数の表(divisor)
policy unique
| 個数 | -> 割る数(per) : number |
| 0 | 1 |
| >=1 | 個数 |
define 一つあたり(per_unit) : money[円] = half_up(合計 / 割る数, 1円)
table 答え(answer)
policy unique
| 個数 | -> 平均 : money[円] |
| 0 | 0円 |
| >=1 | 一つあたり |
examples
| 合計 | 個数 | -> 平均 |
| 1000円 | 3 | 333円 |
| 1000円 | 6 | 167円 |
| 1001円 | 2 | 501円 |
| 500円 | 0 | 0円 |
この例が見せていること
half_up(合計 / 割る数, 1円)のように、丸めの関数の第一引数のいちばん外側でだけ値で割れます。丸めの刻みが、商の型を決めます。- 個数が 0 の注文は表で分けます。表
割る数の表は個数が 1 以上の行でだけ個数を書くので、割る数は 0 になりません。検査は行のセルが狭めた範囲を読み、E132 を出しません。 - もう一つの書き方は
max(個数, 1)で割る形で、平均単価.ruleにあります。
余りで決める当番
三つの班が、決まった順で週ごとに当番を回します。始めた週からの週の数を 3 で割った余りが、当番の班を決めます。
rule 当番の持ち回り(duty_turn) v1
description "ある週に当番をする班。三つの班が決まった順に回り、回し始めた週から数える。それからの週の数を 3 で割った余りで班を決める。回し始める前の週も、余りが負にならないので、どれかの班に当たる"
enum 班(team) = 北(north) | 東(east) | 南(south)
inputs
週(week) : number range >=1 <=53
始めの週(first_week) : number range >=1 <=53
outputs
当番(on_duty) : 班
# `mod` は正の定数で割り、週の差の符号によらず 0、1、2 のどれかを返す。
define 順番(turn) : number = mod(週 - 始めの週, 3)
table 持ち回り(rotation)
policy unique
| 順番 | -> 当番 : 班 |
| 0 | 北 |
| 1 | 東 |
| 2 | 南 |
examples
| 週 | 始めの週 | -> 当番 |
| 10 | 10 | 北 |
| 11 | 10 | 東 |
| 12 | 10 | 南 |
| 13 | 10 | 北 |
| 9 | 10 | 南 |
| 1 | 53 | 南 |
この例が見せていること
mod(週 - 始めの週, 3)は 0、1、2 のどれかです。割る数は正の整数の定数で、引き算が負になっても余りは 0 以上です（床の余り）。- 余りが 0〜2 と決まるので、表は三行で隙間なく埋まり、検査がそれを確かめます。
平方根：経済的発注量
一回に発注する数量を、年間の需要、一回の発注の費用、一個を一年保管する費用から出します。
rule 経済的発注量(order_lot) v1
description "一度に発注する個数。年間の需要と一回の発注の費用を掛けて 2 倍し、一個を一年保管する費用で割った値の平方根。根の中は先に整数に切り捨て、平方根は二乗がそれを超えない最大の整数とする"
inputs
年間の需要(yearly_demand) : number range >=1 <=100万
発注の費用(order_cost) : money[円] range >=1円 <=10万円
保管の費用(holding_cost) : money[円] range >=1円 <=10万円
outputs
発注量(order_quantity) : number round down(1)
# 円を円で割ると単位の無い比になるので、丸めの刻みは数の 1。
define 発注量の二乗(quantity_squared) : number = down(2 * 年間の需要 * 発注の費用 / 保管の費用, 1)
define 量(quantity) : number = isqrt(発注量の二乗)
result 発注量 = 量
examples
| 年間の需要 | 発注の費用 | 保管の費用 | -> 発注量 |
| 1000 | 5000円 | 100円 | 316 |
| 1200 | 3000円 | 200円 | 189 |
| 1 | 1円 | 10万円 | 0 |
| 100万 | 10万円 | 1円 | 447213 |
この例が見せていること
isqrt(x)は、二乗が x を超えない最大の整数です。引数が負になりうると E139 で止まります。- 根の中は、先に
down(…, 1)で整数に丸めます。円を円で割った比には単位が無いので、丸めの刻みは数の 1 です。 - どの言語の生成コードも、同じ整数の二分探索で根を求めます。浮動小数点を使わないので、どの言語でも同じ答えになります。
和の前提：割り当ての残り
申し込みを認めたあとに割り当てがどれだけ残るかで、残りの状態を決めます。使った分と申し込む分の和が割り当てを超えないことは、呼ぶ側が保証します。
rule 割り当ての申し込み(quota_left) v1
description "申し込みを受けたあとに、割り当ての残りがどれだけあるか。呼び出し側は割り当てを超えて申し込まない。使った量と申し込む量を足しても割り当てを超えないので、残りは 0 を下回らない"
enum 残りの具合(headroom) = 使い切り(used_up) | 少ない(low) | 十分(ample)
inputs
使った量(used) : number range >=0 <=1000
申し込む量(requested) : number range >=1 <=1000
割り当て(quota) : number range >=1 <=1000
# constraint の片側は、入力を足した形にできる。
constraint 使った量 + 申し込む量 <= 割り当て
outputs
状態(status) : 残りの具合
derive 残り(left) : number = 割り当て - 使った量 - 申し込む量 range >=-1999 <=999
# 残りが負の行は無い。constraint がそれを起こさず、検査もそう読む。
table 残りの表(remaining)
policy unique
| 残り | -> 状態 : 残りの具合 |
| 0 | 使い切り |
| >=1 <=99 | 少ない |
| >=100 | 十分 |
examples
| 使った量 | 申し込む量 | 割り当て | -> 状態 |
| 400 | 600 | 1000 | 使い切り |
| 400 | 550 | 1000 | 少ない |
| 0 | 1 | 1000 | 十分 |
| 0 | 1 | 1 | 使い切り |
この例が見せていること
constraint 使った量 + 申し込む量 <= 割り当てのように、前提の片側に入力の和を書けます。生成したコードは、前提を破る呼び出しを入口で拒みます。- 残りが負になる行はありません。前提がその組み合わせを除くので、完全性の検査はその行を求めません。
- この前提は、規則を呼ぶワークフローにも効きます（ritsu の言語をまたぐ検査の E201）。
回数を持ち越す：カードの請求の再試行
カードの請求を三回まで試し、三回断られたら諦めます。状態と試した回数は呼ぶ側が持ち、規則は一回ぶんを決めます。
rule 再試行の回数(retry_count) v1
description "カードの引き落としを試すたびに、回収がどう進むか。試すのは三回までで、三回断られたら回収をあきらめる。状態と試した回数は呼び出す側が持ち、規則は一回の試行だけを判定する。書き下ろしの例"
enum 回収の状態(charge_status) = 未回収(pending) | 回収済(collected) | 断念(given_up)
enum 試行の結果(attempt_result) = 承認(approved) | 拒否(declined)
inputs
状態(status) : 回収の状態
結果(outcome) : 試行の結果
試行回数(attempts) : number range >=0 <=3 # この試行より前に試した回数
outputs
次の状態(next_status) : 回収の状態
次の試行回数(next_attempts) : number round down(1)
define 今回までの回数(made) : number = 試行回数 + 1
table 試行(step)
policy unique
| 状態 | 結果 | 試行回数 | -> 次の状態 | 次の試行回数 |
| 未回収 | 承認 | - | 回収済 | 今回までの回数 |
| 未回収 | 拒否 | <=1 | 未回収 | 今回までの回数 |
| 未回収 | 拒否 | >=2 | 断念 | 今回までの回数 | # 三回目の拒否
| 回収済 | - | - | 状態 | 試行回数 |
| 断念 | - | - | 状態 | 試行回数 |
machine 回収(collection) over 試行
carry 状態 -> 次の状態
carry 試行回数 -> 次の試行回数
initial 未回収
initial 試行回数 0
final 回収済, 断念
never 回収済 after 断念
always 試行回数 >=1 when 回収済
always 試行回数 3 when 断念
# 二回断られ、三回目であきらめる。
scenario 三回の拒否(three_declines)
| 結果 | -> 次の状態 | 次の試行回数 |
| 拒否 | 未回収 | 1 |
| 拒否 | 未回収 | 2 |
| 拒否 | 断念 | 3 |
| 承認 | 断念 | 3 |
# 一回断られ、二回目で承認される。
scenario 二回目の承認(approved_on_the_second)
| 結果 | -> 次の状態 | 次の試行回数 |
| 拒否 | 未回収 | 1 |
| 承認 | 回収済 | 2 |
examples
| 状態 | 結果 | 試行回数 | -> 次の状態 | 次の試行回数 |
| 未回収 | 承認 | 0 | 回収済 | 1 |
| 未回収 | 拒否 | 2 | 断念 | 3 |
この例が見せていること
carry 試行回数 -> 次の試行回数で、状態のほかに数も持ち越します。始まりの値はinitial 試行回数 0です。always 試行回数 3 when 断念は「断念した状態では、いつも三回試している」という主張です。どの呼び出しの並びでも成り立つことを検査が確かめ、破れれば最短の並びつきで E135 になります。- 持ち越す数が範囲（0〜3）を出る呼び出しは E134 です。
二つの並びと二回目の歩き
注文の明細と支払いの二つの並びを受け取ります。明細の合計といちばん高い単価を一回目の歩きで求め、いちばん高い単価の明細に一割の値引きを当てるのは、明細を二回目にたどるときです。歩きの順はどこにも書いてありません。
rule 注文の精算(order_settle) v1
description "注文の請求額を求める。明細を合計し、単価がいちばん高い明細から一割を引き、支払い済みの額を差し引く。いちばん高い単価は明細を全部見るまで決まらないので、値引きは明細を二回目にたどって求める。二つの並びと二回目の歩きの例"
enum 明細の扱い(line_pick) = 最高値(top) | その他(rest)
# 注文の明細一件。呼び出し側は何件でも渡す
elements 明細(lines)
数量(quantity) : number range >=1 <=50
単価(price) : money[USD] range >=1USD <=500USD
# この注文に対して支払い済みの一件。明細とは別の並び
elements 支払い(payments)
支払額(amount) : money[USD] range >=1USD <=5000USD
outputs
小計(subtotal) : money[USD] round down(1USD)
値引き(discount) : money[USD] round down(1USD)
支払済(paid) : money[USD] round down(1USD)
残額(balance) : money[USD] round down(1USD)
define 明細額(line_total) : money[USD] = 数量 × 単価
# 明細を一回目にたどって、合計といちばん高い単価を求める。範囲はどちらも完全性の全体集合で、
# 合計の範囲は入口が受け付けなくなる境目でもある
sum 小計 over 明細 of 明細額 range >=0USD <=25000USD
max 最高単価(top_price) over 明細 of 単価 empty 0USD
# 支払いは別にたどる
sum 支払済 over 支払い of 支払額 range >=0USD <=25000USD
# 明細を二回目にたどって、一回目に求めたいちばん高い単価と一件ずつ比べる
define 差(gap) : money[USD] = 最高単価 - 単価
table 明細の判定(pick_line)
policy unique
| 差 | -> 扱い(pick) : 明細の扱い |
| <=0USD | 最高値 |
| >0USD | その他 |
define 値引き額(top_off) : money[USD] = half_down(明細額 × 10%, 1USD)
# いちばん高い単価の最初の明細が値引きを受ける。同じ単価の二件目は受けない
fold 扱い over 明細 -> 値引き
最高値 -> take_first 値引き額
その他 -> next
empty -> 0USD
exhausted -> held
define 残額 : money[USD] = 小計 - 値引き - 支払済
examples
| 明細 | 支払い | -> 小計 | 値引き | 支払済 | 残額 |
| 三行 | 一回払い | 240USD | 12USD | 100USD | 128USD |
| 三行 | 支払いなし | 240USD | 12USD | 0USD | 228USD |
| 同じ単価 | 二回払い | 320USD | 8USD | 120USD | 192USD |
| 明細なし | 一回払い | 0USD | 0USD | 100USD | -100USD |
sequence 三行(three_lines)
| 数量 | 単価 |
| 2 | 30USD |
| 1 | 120USD |
| 4 | 15USD |
sequence 同じ単価(tied_lines)
| 数量 | 単価 |
| 1 | 80USD |
| 3 | 80USD |
sequence 明細なし(no_lines)
| 数量 | 単価 |
sequence 一回払い(one_payment)
| 支払額 |
| 100USD |
sequence 二回払い(two_payments)
| 支払額 |
| 50USD |
| 70USD |
sequence 支払いなし(no_payments)
| 支払額 |
この例が見せていること
elementsは何本でも書けます。集計はそれぞれ、どの並びをたどるかをoverで言います。- 歩きの順は読むものから決まります。
gapは単価と、一回目の歩きで求めたtop_priceを読むので、二回目の歩きに入ります。それを読む表と fold も同じです。 max top_price over lines of price empty 0USDのemptyは必須です。明細が一つも無いときの答えで、業務の判断だからです。範囲は単価の範囲とemptyの値から計算します。- fold の答えに
-> discountで名前を付けると、後ろのdefineが読めます。その範囲は fold が答えうる値から決まり、balanceの int64 の主張も立ちます。
科目の履修の前提
科目ごとに、何年次の科目か、単位数、履修の前に合格していなければならない科目を決めます。前提は prerequisites の塊に一度だけ書き、年次の表と食い違わないことも検査します。
rule 科目の履修(course_enrollment) v1
description "情報系の学位の科目。科目ごとに、何年次の科目か、単位数、履修の前に合格していなければならない科目を決める。書き下ろしの例"
# 年次は低い順に並べる。どの科目も、それに要る科目より前の年次には置かない（下の `ordered by
# 年次表`）。
enum 年次(year) = 一年(first) < 二年(second) < 三年(third) < 四年(fourth)
enum 科目(course) = プログラミング入門(intro_programming) | 離散数学(discrete_math) | 微積分(calculus) | 統計学(statistics) | 線形代数(linear_algebra) | データ構造(data_structures) | データベース(databases) | アルゴリズム(algorithms) | オペレーティングシステム(operating_systems) | ネットワーク(networks) | 機械学習(machine_learning) | コンパイラ(compilers) | 卒業研究(capstone) | メインフレームCOBOL(mainframe_cobol)
inputs
科目(course) : 科目
outputs
年次(year) : 年次
単位(credits) : number round down(1)
table 年次表(level_of)
policy unique
| 科目 | -> 年次 |
| プログラミング入門, 離散数学, 微積分 | 一年 |
| 統計学, 線形代数, データ構造, データベース | 二年 |
| アルゴリズム, オペレーティングシステム, ネットワーク | 三年 |
| 機械学習, コンパイラ, 卒業研究, メインフレームCOBOL | 四年 |
table 単位表(credit_of)
policy unique
| 科目 | -> 単位 |
| 卒業研究 | 8 |
| not: 卒業研究 | 4 |
# 履修の前に合格していなければならない科目。`start` の科目は何も要らない。科目ごとの行では、
# `,` で区切ったものは全部が要り、`or` でつないだものはどれか一つで足りる。
prerequisites 履修(enrollment) over 科目
start プログラミング入門, 離散数学, 微積分
統計学 requires 微積分
線形代数 requires 微積分
データ構造 requires プログラミング入門
データベース requires プログラミング入門
アルゴリズム requires データ構造, 離散数学
オペレーティングシステム requires データ構造
ネットワーク requires オペレーティングシステム
機械学習 requires アルゴリズム, 統計学 or 線形代数
コンパイラ requires アルゴリズム
卒業研究 requires データベース, ネットワーク or コンパイラ
メインフレームCOBOL requires nothing "2026 年に科目の一覧から外した"
ordered by 年次表
examples
| 科目 | -> 年次 | 単位 |
| プログラミング入門 | 一年 | 4 |
| データベース | 二年 | 4 |
| ネットワーク | 三年 | 4 |
| 卒業研究 | 四年 | 8 |
この例が見せていること
startの科目は何も要りません。ほかの科目は一行ずつrequiresで前提を書き、,で区切ったものは全部が、orでつないだものはどれか一つが要ります。requires nothing "…"は、取れなくなった科目です。それを前提にした科目があると、startからたどり着けないと言われます（E137）。ordered by 年次表は、どの科目も前提より前の年次に置かないことを確かめます（E138）。生成コードは、科目に要るものと、合格した科目でその科目を取れるかを、どの言語でも返します。
注文の合計と最大、明細の並びを契約から取る
店の API が受け取る注文オブジェクトから、取扱手数料を決めます。注文の合計と、割れ物の明細でいちばん高い額は、オブジェクトの明細から from sum と from max で読みます。明細そのものは elements … from で、規則がたどる並びとして取ります。
rule 注文の取扱手数料(order_handling) v1
description "店の API が受け取る注文オブジェクトから、取扱手数料を決める。注文の合計と、割れ物の明細でいちばん高い額はオブジェクトから読み、明細はそのまま規則がたどる並びになる。合計・最大・並びを契約から取る例"
# 呼び出し側はもう JSON Schema で注文の形を決めている。合計、割れ物の最高額、明細の並びをそこから読む。
# 注文を平たくするコードは生成され、どのパスも毎回の check で契約に照らされる。
shape 注文(order) = jsonschema "contracts/order_lines.schema.json" "#/$defs/Order"
inputs
合計(total) : money[USD] range >=0USD <=100_000USD from sum 注文.lines of amount_usd
割れ物の最高額(top_fragile) : money[USD] range >=0USD <=5_000USD from max 注文.lines of amount_usd where fragile = true empty 0USD
# 注文の明細一件。注文オブジェクトからそのまま取る
elements 明細(lines) from 注文.lines
数量(quantity) : number range >=1 <=99 from quantity
金額(amount) : money[USD] range >=1USD <=5000USD from amount_usd
outputs
手数料(fee) : money[USD] round up(1USD)
# 50 個以上の明細と、2000USD 以上の明細は、パレットに載せる
table パレット(pallet)
policy unique
| 数量 | 金額 | -> パレット行(pallet_line) : bool |
| >=50 | - | true |
| <50 | >=2000USD | true |
| <50 | <2000USD | false |
count パレット数(pallet_lines) over 明細 where パレット行 range >=0 <=20
# 大きな注文は無料で扱い、高い割れ物は丁寧に梱包する
table 取扱い(handling)
policy unique
| 合計 | 割れ物の最高額 | -> 基本料(base) : money[USD] |
| >=10000USD | - | 0USD |
| <10000USD | >=1000USD | 25USD |
| <10000USD | <1000USD | 5USD |
# パレットが二枚以上ならフォークリフトを使う
table フォークリフト(forklift)
policy unique
| パレット数 | -> 荷役料(lift) : money[USD] |
| >=2 | 10USD |
| <2 | 0USD |
define 取扱料(handling_fee) : money[USD] = 基本料 + 荷役料
result 手数料 = 取扱料
examples
| 合計 | 割れ物の最高額 | 明細 | -> 手数料 |
| 120USD | 0USD | 小さな注文 | 5USD |
| 12000USD | 0USD | 大きな注文 | 10USD |
| 2100USD | 1500USD | 割れ物の注文 | 25USD |
| 900USD | 0USD | まとめ買い | 15USD |
sequence 小さな注文(small_order)
| 数量 | 金額 |
| 2 | 40USD |
| 1 | 80USD |
sequence 大きな注文(large_order)
| 数量 | 金額 |
| 3 | 5000USD |
| 2 | 5000USD |
| 1 | 2000USD |
sequence 割れ物の注文(glass_order)
| 数量 | 金額 |
| 1 | 1500USD |
| 4 | 600USD |
sequence まとめ買い(bulk_order)
| 数量 | 金額 |
| 60 | 300USD |
| 80 | 400USD |
| 5 | 200USD |
この例が見せていること
from sum 注文.lines of amount_usdは、明細のamount_usdの合計です。from max 注文.lines of amount_usd where fragile = true empty 0USDは、割れ物の明細のうちいちばん高い額です。割れ物が一つも無いときの値をemptyに書きます。書かなければ E074 です。elements 明細 from 注文.linesで、明細を契約の配列からそのまま取ります。 フィールドはそれぞれ、要素の中のどこから読むかをfrom quantityのように書きます。取り出した要素は、呼び出し側が並びを渡すときとまったく同じに検査され、たどられます。- 契約の検証とも突き合わせます。 契約は明細を 20 件まで、一件の額を 5000 まで通すので、合計は 10 万まで届き、規則の
合計の範囲と同じです。maxItemsを消すと、合計が範囲を超える注文と、21 件の明細を持つ注文が契約を通ってしまうので、どちらも E122 で止まります。 rulec genが書くorder_handling_from(order)は、注文をそのまま受け取ります。 明細の並びは関数の中で組み立てるので、引数は注文だけです。この関数が出るのは Python・TypeScript・JavaScript・Ruby・PHP で、Go・Swift・Java・Rust・SQL・NumPy・Wasm には出ません。- 読む値は、規則の型どおりかを確かめます。 明細の
amount_usdが1.5や"7"なら、関数は答えを返さず、注文.lines[].amount_usd is not an integer: 1.5のように値の場所を言ってRuleInputErrorで止まります。五つの言語で同じ文です。
ポスターの確率を、表と突き合わせる
店のくじの景品です。券の番号は 0 から 999 のどれかが引かれ、キャンペーン中は三等に当たる番号が増えます。番号の入力に random を付けると、ポスターに刷る確率を chances の表に書けて、rulec check が表の行から数えて確かめます。
rule くじの景品(lottery_prize) v1
description "店のくじの券が当たる景品。券の番号は 0 から 999 のどれかが引かれ、キャンペーン中は三等に当たる番号が増える。ポスターに刷る確率を下の主張にしているので、ポスターとコードが一つの元から出る。書き下ろしの例"
enum 景品(prize) = 一等(first) | 二等(second) | 三等(third) | はずれ(no_prize)
inputs
番号(ticket) : number range >=0 <=999 random
キャンペーン中(campaign) : bool
outputs
景品(prize) : 景品
table 番号表(numbers)
policy unique
| 番号 | キャンペーン中 | -> 景品 |
| 0 | - | 一等 |
| >=1 <=9 | - | 二等 |
| >=10 <=99 | true | 三等 |
| >=10 <=59 | false | 三等 |
| >=60 <=99 | false | はずれ |
| >=100 | - | はずれ |
# ポスターに刷る確率。
chances
| キャンペーン中 | -> 景品 | chance |
| - | 一等 | 0.1% |
| - | 二等 | 0.9% |
| true | 三等 | 9% |
| false | 三等 | 5% |
| true | はずれ | 90% |
| false | はずれ | 94% |
examples
| 番号 | キャンペーン中 | -> 景品 |
| 0 | false | 一等 |
| 9 | false | 二等 |
| 59 | false | 三等 |
| 60 | false | はずれ |
| 99 | true | 三等 |
| 100 | true | はずれ |
この例が見せていること
randomは、呼び出し側がその入力を範囲から一様に引いて渡す、という宣言です。 規則の関数は変わりません。引くのは呼び出し側で、同じ入力からは同じ景品が出ます。chancesの行は、乱数でない入力のどの組み合わせでも、その確率で答えが出ることを主張します。 確率は1/1000、0.9%、>=1/2のように書けます。表の行は区画なので、rulec checkは番号の点を区間ごとに数え、正確な有理数で比べます。- 表とポスターが食い違えば止まります。 キャンペーン外の三等を 6% と書くと E133 になり、「キャンペーン中 = false のとき、景品 = 三等 の確率は 1/20（5.0%）です」と言います。
rulec genは、確率を数える関数も書きます。lottery_prize_chances(campaign)は、景品ごとに当たる番号の数と、番号の全部の数を返します。SQL と Wasm のほかのどの生成先にもあり、HTML のページの「試してみる」は、この関数で景品ごとの確率を出します。
重ねる値引き、重ねない値引き、上限を開いておく
注文の値引きを、ほかのファイルが足せる三つの値で組み立てます。重ねられる値引きは足し合わせ、重ねられない値引きはいちばん大きいものだけを使い、上限はいちばん低いものを使います。キャンペーンは、別のファイルからこの三つに足します。
rule 注文の値引き(order_savings) v1
description "注文の値引き。重ねられる値引きは足し合わせ、重ねられない値引きはいちばん大きいものだけを使い、合計は上限と小計を超えない。キャンペーンは、三つの開いた値に別のファイルから足す"
enum 経路(channel) = ウェブ(web) | 店頭(store) default | 電話(phone) default open
inputs
小計(subtotal) : money[USD] range >=0USD <=5000USD
会員(member) : bool
クーポン(coupon) : bool
注文経路(via) : 経路
outputs
値引き(discount) : money[USD] round down(1USD)
table 会員の分
policy unique
| 会員 | -> 会員値引 : money[USD] |
| true | 5USD |
| false | 0USD |
table 経路の分
policy first
| 注文経路 | -> 経路値引 : money[USD] |
| ウェブ | 3USD |
| - | 0USD |
table クーポンの分
policy unique
| クーポン | -> クーポン値引 : money[USD] |
| true | 10USD |
| false | 0USD |
# 重ねられる値引き: どれも使う。
open 重ねる値引 : money[USD] combine sum range >=0USD <=100USD
会員値引
経路値引
# 重ねられない値引き: いちばん大きいものだけを使う。
open 重ねない値引 : money[USD] combine max empty 0USD range >=0USD <=60USD
クーポン値引
# 値引き全体の上限: キャンペーンが決めたうちでいちばん低いもの。決めていなければ 50 ドル。
open 上限 : money[USD] combine min empty 50USD range >=0USD <=50USD
define 値引き : money[USD] = min(min(重ねる値引 + 重ねない値引, 上限), 小計)
examples
| 小計 | 会員 | クーポン | 注文経路 | -> 値引き |
| 200USD | true | true | ウェブ | 18USD |
| 200USD | false | false | 店頭 | 0USD |
| 12USD | true | true | ウェブ | 12USD |
| 200USD | true | false | 電話 | 5USD |
この例が見せていること
open 重ねる値引 : money[USD] combine sum range …が、ほかのファイルが足せる値です。下に、この規則の項を一行ずつ書きます。合わせ方はsum・product・max・minの四つで、どれも項の順によりません。- 範囲は必ず書き、下の表はその範囲の全体で検査されます。 だから、この規則の検査は、どんなキャンペーンが来ても成り立ちます。キャンペーンを合わせた値が範囲を出れば E131 です。
maxとminのemptyは、項があっても合わせに加わる出発の値です。上限のempty 50USDは「決めていなければ 50 ドル」で、50 ドルより高い上限は何も抑えないので W132 と言われます。- キャンペーンは
contributionのファイル（contrib/注文の値引き/地域のキャンペーン.rule）に書き、into 重ねる値引で足します。rulec check 注文の値引き.rule contrib/注文の値引き/が、規則だけと、合わせた規則の両方を検査します。
Stripe の PaymentIntent の状態（machine）
Stripe のドキュメントから、PaymentIntent の状態が confirm・認証・capture・cancel と、あとで届く支払いの結果でどう移るかを転記したものです。事業者の API の仕様から作った例で、状態は Stripe の七つをそのまま使っています。
rule payment_intent v1
description "Where a Stripe PaymentIntent's status goes when it is confirmed, authenticated, captured or canceled, and when a delayed payment settles. Transcribed from Stripe's documentation"
# Read on 25 September 2026. The comments name the pages as follows:
# lifecycle https://docs.stripe.com/payments/paymentintents/lifecycle
# status https://docs.stripe.com/payments/payment-intents/verifying-status
# confirm https://docs.stripe.com/api/payment_intents/confirm
# cancel https://docs.stripe.com/api/payment_intents/cancel
# capture https://docs.stripe.com/api/payment_intents/capture
# hold https://docs.stripe.com/payments/place-a-hold-on-a-payment-method
# 3ds https://docs.stripe.com/payments/3d-secure/authentication-flow
# errors https://docs.stripe.com/error-codes (payment_intent_unexpected_state)
# A row the pages do not settle says so at its end, with what was assumed.
enum status = requires_payment_method | requires_confirmation | requires_action | processing | requires_capture | succeeded | canceled
enum event = attach | confirm | authenticate | settle | capture | cancel | expire
# The two methods are Stripe's own enums, and both have `automatic` and `manual`. The hold
# page also describes `automatic_delayed`, in private preview and not in the object's enum.
enum capture_method = automatic | automatic_async | manual
enum confirmation_method = automatic | manual
enum funds = untouched | held | captured | released
group unconfirmed = requires_payment_method, requires_confirmation
inputs
status : status
event : event # attach: a payment method is attached without confirming
limit_reached : bool # this confirmation is past the limit Stripe puts on one PaymentIntent, which varies
needs_action : bool # the payment method asks for a further step, such as 3D Secure
approved : bool # the issuer or the bank lets the attempt through; for a cancel, Stripe accepts it
delayed : bool # the payment method confirms success only days later, as a bank debit does
capture_method : capture_method
confirmation_method : confirmation_method
outputs
next_status : status
funds : funds
refused : bool # the status does not take this event: an API call gets payment_intent_unexpected_state
# The 3ds page tells the step after authentication differently: Stripe attempts the charge and
# the PaymentIntent moves to processing, card or not. The lifecycle and status pages keep
# processing for payment methods that confirm later, and the rows below follow them.
table transition # lifecycle, status, and the API reference for each call
policy unique
| status | event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| unconfirmed | attach | - | - | - | - | - | - | requires_confirmation | untouched | false | # lifecycle; from requires_confirmation, assumed the same
| unconfirmed | confirm | true | - | - | - | - | - | canceled | untouched | false | # confirm
| unconfirmed | confirm | false | true | - | - | - | - | requires_action | untouched | false | # confirm
| unconfirmed | confirm | false | false | false | - | - | - | requires_payment_method | untouched | false | # confirm
| unconfirmed | confirm | false | false | true | - | manual | - | requires_capture | held | false | # confirm
| unconfirmed | confirm | false | false | true | true | automatic, automatic_async | - | processing | untouched | false | # lifecycle
| unconfirmed | confirm | false | false | true | false | automatic, automatic_async | - | succeeded | captured | false | # confirm
| unconfirmed | cancel | - | - | - | - | - | - | canceled | untouched | false | # cancel
| unconfirmed | authenticate, settle, capture, expire | - | - | - | - | - | - | status | untouched | true | # capture, errors
| requires_action | authenticate | - | - | false | - | - | - | requires_payment_method | untouched | false | # 3ds
| requires_action | authenticate | - | - | true | - | - | manual | requires_confirmation | untouched | false | # confirm
| requires_action | authenticate | - | - | true | - | manual | automatic | requires_capture | held | false | # 3ds
| requires_action | authenticate | - | - | true | true | automatic, automatic_async | automatic | processing | untouched | false | # lifecycle
| requires_action | authenticate | - | - | true | false | automatic, automatic_async | automatic | succeeded | captured | false | # 3ds, lifecycle
| requires_action | cancel | - | - | - | - | - | - | canceled | untouched | false | # cancel
| requires_action | attach, confirm, settle, capture, expire | - | - | - | - | - | - | status | untouched | true | # errors; for attach and confirm the pages say nothing, assumed refused
| processing | settle | - | - | true | - | - | - | succeeded | captured | false | # lifecycle, status
| processing | settle | - | - | false | - | - | - | requires_payment_method | untouched | false | # lifecycle
| processing | cancel | - | - | true | - | - | - | canceled | untouched | false | # lifecycle: ACH, ACSS, AU BECS, BACS, NZ BECS and SEPA, inside a window
| processing | cancel | - | - | false | - | - | - | status | untouched | true | # lifecycle; cancel says "in rare cases"
| processing | attach, confirm, authenticate, capture, expire | - | - | - | - | - | - | status | untouched | true | # errors
| requires_capture | capture | - | - | - | false | - | - | succeeded | captured | false | # capture, lifecycle
| requires_capture | capture | - | - | - | true | - | - | processing | untouched | false | # lifecycle names no method; hold says bank debits cannot be held
| requires_capture | cancel | - | - | - | - | - | - | canceled | released | false | # cancel
| requires_capture | expire | - | - | - | - | - | - | canceled | released | false | # hold, capture
| requires_capture | attach, confirm, authenticate, settle | - | - | - | - | - | - | status | untouched | true | # errors
| succeeded | - | - | - | - | - | - | - | status | untouched | true | # lifecycle, status: refunds go through the Refunds API
| canceled | - | - | - | - | - | - | - | status | untouched | true | # cancel, lifecycle
# A case keeps the two methods it was created with, and may change payment method between
# attempts. Whether a retry uses a card or a bank debit is `delayed`, passed on every call.
machine payment over transition
carry status -> next_status
held capture_method, confirmation_method
initial requires_payment_method
final succeeded, canceled
never succeeded after canceled
once funds captured
# 3ds: a card that asks for 3D Secure, and a customer who passes it.
scenario card_with_3ds
| event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| confirm | false | true | false | false | automatic_async | automatic | requires_action | untouched | false |
| authenticate | false | false | true | false | automatic_async | automatic | succeeded | captured | false |
# hold: a hotel authorizes at booking and captures at check-out.
scenario authorize_then_capture
| event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| confirm | false | false | true | false | manual | automatic | requires_capture | held | false |
| capture | false | false | true | false | manual | automatic | succeeded | captured | false |
# hold, capture: nobody captures, and the authorization runs out.
scenario hold_expires
| event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| confirm | false | false | true | false | manual | automatic | requires_capture | held | false |
| expire | false | false | false | false | manual | automatic | canceled | released | false |
| capture | false | false | true | false | manual | automatic | canceled | untouched | true |
# lifecycle: a bank debit that fails days later, and a card that goes through on the retry.
scenario debit_fails_card_retries
| event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| confirm | false | false | true | true | automatic | automatic | processing | untouched | false |
| cancel | false | false | false | true | automatic | automatic | processing | untouched | true |
| settle | false | false | false | true | automatic | automatic | requires_payment_method | untouched | false |
| confirm | false | false | true | false | automatic | automatic | succeeded | captured | false |
# confirm: with manual confirmation, the server confirms again after the customer's step.
scenario manual_confirmation
| event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| attach | false | false | false | false | automatic | manual | requires_confirmation | untouched | false |
| confirm | false | true | false | false | automatic | manual | requires_action | untouched | false |
| authenticate | false | false | true | false | automatic | manual | requires_confirmation | untouched | false |
| confirm | false | false | true | false | automatic | manual | succeeded | captured | false |
# confirm: declines until Stripe's limit on confirmations is reached.
scenario too_many_confirmations
| event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| confirm | false | false | false | false | automatic | automatic | requires_payment_method | untouched | false |
| confirm | true | false | false | false | automatic | automatic | canceled | untouched | false |
| confirm | false | false | true | false | automatic | automatic | canceled | untouched | true |
examples
| status | event | limit_reached | needs_action | approved | delayed | capture_method | confirmation_method | -> next_status | funds | refused |
| requires_capture | cancel | false | false | false | false | manual | automatic | canceled | released | false |
| succeeded | cancel | false | false | false | false | automatic | automatic | succeeded | untouched | true |
| processing | cancel | false | false | true | true | automatic | automatic | canceled | untouched | false |
この例が見せていること
- ドキュメントが決めていない組み合わせが、行として出てきます。 表の完全性が、状態とイベントの組み合わせを全部埋めさせるからです。
requires_actionで支払い方法を付け直したときなど、どのページにも書いていないものは仮に決め、行末に assumed と書いてあります。人が Stripe に確かめるのは、その行です。 - ページどうしの読みの違いは、表の上の注記にあります。 3D セキュアのページは、認証のあとカードでも
processingに移ると書きます。ライフサイクルのページは、processingをあとで結果が分かる支払い方法のときだけの状態としています。表は後者に従っています。 - 二つの列挙が同じ名前の値を持っています。
capture_methodとconfirmation_methodは、どちらもautomaticとmanualを持ちます。値は、書かれた列の列挙で読みます。 - 値は予約語と同じ綴りでも書けます。 資金の状態の
held（与信で押さえた資金）は、machineの節のheldと同じ綴りです。値は行の頭に来ないので、取り違えられることがありません。 - 主張は四つで、どれも成り立ちます。
succeededとcanceledで終わる、canceledのあとにsucceededに着かない、funds capturedは一回まで、どの状態からでも終われる。例は、ドキュメントに書かれている六つの流れ（3D セキュア、与信と確定、与信の有効期限切れ、口座振替の失敗など）です。
返品できるかどうかを英語で書く
金額がどこにも出てこない例を、名前もセルも英語で書いたものです。答えは四つの語のどれか一つで、入力の組み合わせはどれもちょうど一行に当たります。お店の規約を想定した作り物で、どこかの規約の転記ではありません。
rule return_eligibility v1
description "Whether a return is accepted. Written in English, and with no money in it anywhere: the answer is a class"
# A sketch of a shop's own terms, not a transcription. The shape is the point: the answer is
# one of four words, and every combination of the four inputs reaches exactly one row.
enum category = electronics | clothing | perishable
enum verdict = accepted | outside_window | condition_failed | not_returnable
inputs
item : category
days : number range >=0 <=365
opened : bool
receipt : bool
outputs
answer : verdict
# Written as `policy unique`, so the rows are disjoint and the checker proves that every
# input reaches exactly one of them. `policy first` would take three rows fewer by letting
# the refusals at the top swallow the rest — and then which row answers a given case would
# be a question about the order of the rows rather than about the row itself.
table decide
policy unique
| item | receipt | days | opened | -> answer : verdict |
| perishable | - | - | - | not_returnable |
| not: perishable | false | - | - | condition_failed |
| electronics | true | >14 | - | outside_window |
| electronics | true | <=14 | true | condition_failed |
| electronics | true | <=14 | false | accepted |
| clothing | true | >30 | - | outside_window |
| clothing | true | <=30 | - | accepted |
examples
| item | days | opened | receipt | -> answer |
| clothing | 10 | true | true | accepted |
| clothing | 31 | false | true | outside_window |
| electronics | 3 | true | true | condition_failed |
| electronics | 14 | false | true | accepted |
| perishable | 0 | false | true | not_returnable |
| clothing | 10 | false | false | condition_failed |
この例が見せていること
- 答えが金額でない規則も、形は同じです。 出力は列挙の値で、丸めの宣言は要りません。
policy uniqueで書いてあります。 行が重ならないように書くと、どの入力もちょうど一行に当たることを検査が証明します。policy firstなら三行減らせますが、そのぶん「どの行が答えたのか」が行の並び順の話になります。not:は列挙の値そのものにも使えます。not: perishableは「生鮮以外」で、グループを作らなくても書けます。
ポンドとインチの運賃表
英語で書いた運賃表です。重さはポンド、寸法はインチ、金額は USD。これも作り物で、金額は架空のものです。コーパスでヤード・ポンド法の単位を使っているのはこの規則だけです。
rule parcel_rate v1
description "A parcel tariff in pounds and inches, written in English. A sketch, not a transcription: the amounts are made up"
# Nothing else in the corpus is priced in USD by weight, and nothing at all reached oz, lb
# or in — an unexercised unit is an unchecked unit (§15.9).
enum size_class = envelope | small | large
enum zone = domestic | canada | overseas
group north_america = domestic, canada
inputs
weight : mass[lb] range >=1lb <=70lb
girth : length[in] range >=1in <=130in
dest : zone
signature : bool
outputs
fee : money[USD, incl_tax] round up(1USD)
# One table decides the class and the next one prices it: what the first produces is a
# column of the second.
table size_of
policy first
| girth | -> size : size_class |
| <=22in | envelope |
| <=60in | small |
| - | large |
table base_rate
policy unique
| dest | size | weight | -> base : money[USD, incl_tax] |
| north_america | envelope | - | 6USD |
| north_america | small | <=160oz | 12USD |
| north_america | small | >160oz | 18USD |
| north_america | large | <=160oz | 22USD |
| north_america | large | >160oz | 30USD |
| overseas | envelope | - | 16USD |
| overseas | small | - | 38USD |
| overseas | large | - | 60USD |
# A fuel surcharge is a percentage of the base, which is what the rounding on the output is
# there to settle: 12USD at 5% is 12.60USD, and up(1USD) makes that 13USD.
table fuel_rate
policy unique
| dest | -> fuel : rate[step 1%] |
| north_america | 5% |
| overseas | 12% |
table signature_fee
policy unique
| signature | -> extra : money[USD, incl_tax] |
| true | 4USD |
| false | 0USD |
result fee = base + base × fuel + extra
examples
| weight | girth | dest | signature | -> fee |
| 5lb | 10in | domestic | false | 7USD |
| 5lb | 40in | canada | false | 13USD |
| 20lb | 40in | domestic | true | 23USD |
| 5lb | 10in | overseas | false | 18USD |
この例が見せていること
- ヤード・ポンド法の単位も、ほかの単位と同じに扱えます。
mass[lb]の入力を、行では160ozと書いて引いています（16oz = 1lb）。単位は型の一部なので、inの列にcmと書けば E103 で止まります。 - 表を積んでいます。 上の表が出す
sizeが、下の表の列になります。寸法から区分を決める表と、区分から値段を決める表を分けて書けるということです。 - 丸めの宣言が効くのはこういうところです。 基本料に 5% を掛けると 12.60USD のような端数が出ます。
up(1USD)と書いてあるので 13USD になりますが、どちらに寄せるかは商売の決めごとで、ツールの側では決めません。
EU 旅客権利規則を英語で書く
名前もセルも英語なので、ASCII 別名が一つも出てきません。金額は EUR、距離は km です。公開されている法令（(EC) No 261/2004 第 7 条）をそのまま転記したもので、条文そのものが決定表の形をしています。
rule ec261 v1
description "Article 7 of EU air passenger rights Regulation (EC) No 261/2004. The example in English, in EUR and km"
# Published law, transcribed as it stands: the amounts are paragraph 1, the halving is
# paragraph 2. Distance and whether the flight is intra-EU decide the band, and that one
# band decides both the amount and the time threshold.
enum band = short | medium | long
inputs
distance : length[km] range >=1km <=20000km
intra_eu : bool
delay : duration[h] range >=0h <=48h
outputs
compensation : money[EUR, incl_tax] round down(1EUR)
# Article 7(1). (a) 1500km or less, (b) intra-EU over 1500km and other flights of 1500 to
# 3500km, (c) everything else. Whether "between 1500 and 3500 kilometres" takes in either
# end cannot be read out of the text. Since (a) is "1500 kilometres or less", the lower end
# is open here — and having to decide it is the point of the tool: undecided, there is no
# table to write.
table band_of
policy unique
| distance | intra_eu | -> band : band |
| <=1500km | - | short |
| >1500km | true | medium |
| >1500km <=3500km | false | medium |
| >3500km | false | long |
table amount
policy unique
| band | -> base : money[EUR, incl_tax] |
| short | 250EUR |
| medium | 400EUR |
| long | 600EUR |
# Article 7(2). The amount may be halved where the re-routing arrives no later than
# (a) two hours, (b) three hours, (c) four hours after the scheduled time. The article's
# (a)(b)(c) restate the distance conditions of paragraph 1 in full, so this table keys on
# distance too, not on the band. The band would fit in two rows, and would put "which
# distance gets four hours" one step further from the text.
table reduction
policy unique
| distance | intra_eu | delay | -> factor : rate[step 50%] |
| <=1500km | - | <=2h | 50% |
| <=1500km | - | >2h | 100% |
| >1500km | true | <=3h | 50% |
| >1500km | true | >3h | 100% |
| >1500km <=3500km | false | <=3h | 50% |
| >1500km <=3500km | false | >3h | 100% |
| >3500km | false | <=4h | 50% |
| >3500km | false | >4h | 100% |
result compensation = base × factor
examples
| distance | intra_eu | delay | -> compensation |
| 900km | true | 5h | 250EUR |
| 900km | true | 2h | 125EUR |
| 2000km | true | 5h | 400EUR |
| 3000km | false | 3h | 200EUR |
| 6000km | false | 5h | 600EUR |
| 6000km | false | 4h | 300EUR |
この例が見せていること
- ASCII の名前には別名が要りません。 漢字は Go の公開識別子になれないので
運賃(fee)のような別名が要りますが、distanceにはその必要がありません。英語で書けば、カッコはどこにも出てきません。 - 通貨どうしは換算されません。
money[EUR]の列に100円を書くと E103 で止まります。為替レートはこのツールの中に無く、あってはいけないものだからです（単位の一覧）。 - 条文が決めていないことを、表が決めさせます。 第 7 条 1 項の (b) は「between 1500 and 3500 kilometres」で、両端を含むかが読めません。(a) が「1500km 以下」なので下端は開く、とここで決めています。決めなければ抜けか重なりで止まるので、あいまいなまま先へは進めません。
- 同じ条件を二度書くほうが正しいこともあります。 5 割引きの閾値（2 / 3 / 4 時間）は帯で引けば二列で済みますが、条文の 2 項は距離の条件を丸ごと書き直しています。ここでも距離で引いたのは、そのほうが原文と行が一対一で並ぶからです。
最低賃金と、それを上書きする例外
2026 年 4 月からの英国の最低賃金です。GOV.UK は年齢帯ごとの時給を並べ、そのあとに「見習いはこの額」という例外を書いています。だから表も二つで、二つめが一つめを上書きします。
rule uk_minimum_wage v1
description "The UK hourly minimum wage from 1 April 2026, transcribed from GOV.UK. An English transcription with a main rule and its exception"
# GOV.UK states a rate for each age band, and then states the apprentice rate as an
# exception to it: an apprentice takes the apprentice rate while under 19, or while in the
# first year of the apprenticeship, and the rate for their age afterwards. Two tables, the
# second overriding the first, is that sentence. One table with an apprentice column would
# give the same answers with the shape of the source lost.
source gov = file "sources/uk-nmw.md" sha256:bc45eedf7f908896 # GOV.UK, Open Government Licence v3.0
table1 sha256:3c2fa10da7e3bf65
inputs
age : number range >=16 <=70
apprentice : bool
first_year : bool
# A wage is not a price, so there is no tax flag on it. The rates are whole pence, and the
# rounding is declared because every numeric output must declare one.
outputs
hourly : money[GBPc] round down(1GBPc)
table by_age @gov table1
policy unique
| age | -> hourly : money[GBPc] |
| <18 | 800GBPc |
| >=18 <=20 | 1085GBPc |
| >=21 | 1271GBPc |
table apprentice_rate @gov table1
policy unique
overrides by_age
| apprentice | first_year | age | -> hourly : money[GBPc] |
| true | - | <19 | 800GBPc |
| true | true | >=19 | 800GBPc |
examples
| age | apprentice | first_year | -> hourly |
| 25 | false | false | 1271GBPc |
| 19 | false | false | 1085GBPc |
| 17 | false | false | 800GBPc |
| 25 | true | true | 800GBPc |
| 25 | true | false | 1271GBPc |
| 18 | true | false | 800GBPc |
この例が見せていること
- 本則と例外は、一枚の広い表ではなく二枚の表です。
overrides by_ageが「見習いの行が優先する」と宣言し、検査は二つをひとつの集合として完全性と重なりに掛けます。例外が本則に穴を空けることはできません。 - 文書は規則の隣に置いて、digest で留めてあります。
source gov = file "…" sha256:…と、表に付けた@gov table1です。ここから先は、文書のコピーに無い時給を書くと E116 で止まります。 - 見習いの一文が二行になっているのは、条件が二つだからです。 「19 歳未満」と「19 歳以上で見習い一年目」を、ページが書いているとおりに二行で書いています。
逓減する控除と、その上の税率帯
英国の個人控除（Personal Allowance）と、所得がどの税率帯に入るかです。控除は 10 万ポンドを超えた分 2 ポンドにつき 1 ポンドずつ減ります。これは行ではなく計算なので、derive に書いて、それを行が名前で呼びます。
rule uk_income_tax v1
description "The UK Personal Allowance and the Income Tax band an income falls in, for England, Wales and Northern Ireland. Transcribed from GOV.UK"
source gov = file "sources/uk-income-tax.md" sha256:8aa392743f75ce6f # GOV.UK, Open Government Licence v3.0
table1 sha256:7d9ba57e7bb838a7
enum band = personal_allowance | basic | higher | additional
inputs
income : money[GBP] range >=0GBP <=10000000GBP
outputs
allowance : money[GBP] round down(1GBP)
in_band : band
rate : rate[step 1%] round down(1%)
# "Your personal allowance goes down by £1 for every £2 that your adjusted net income is
# above £100,000." Half of the excess, taken off the standard allowance — and because it is
# £1 per £2, an odd pound is dropped, which is what the rounding on the output settles.
derive above_100k : money[GBP] = income − 100000GBP range >=-100000GBP <=9900000GBP
derive tapered : money[GBP] = 12570GBP − above_100k × 50% range >=-4937430GBP <=62570GBP
# The third row could be left to the taper, which reaches zero at £125,140 on its own. It is
# written out because the page writes it out: "your allowance is zero if your income is
# £125,140 or above".
table allowance_of
policy unique
| income | -> allowance : money[GBP] |
| <=100000GBP | 12570GBP |
| >100000GBP <125140GBP | tapered |
| >=125140GBP | 0GBP |
# The page writes each band from the first pound that falls in it (£12,571 to £50,270). A
# pound is the unit here, so "from £12,571" and "above £12,570" are the same set, and the
# second form is the one the checker reads as adjacent to the row above.
table band_of @gov table1
policy unique
| income | -> in_band : band | rate : rate[step 1%] |
| <=12570GBP | personal_allowance | 0% |
| >12570GBP <=50270GBP | basic | 20% |
| >50270GBP <=125140GBP | higher | 40% |
| >125140GBP | additional | 45% |
examples
| income | -> allowance | in_band | rate |
| 10000GBP | 12570GBP | personal_allowance | 0% |
| 30000GBP | 12570GBP | basic | 20% |
| 100000GBP | 12570GBP | higher | 40% |
| 110000GBP | 7570GBP | higher | 40% |
| 125140GBP | 0GBP | higher | 40% |
| 200000GBP | 0GBP | additional | 45% |
この例が見せていること
- 行には計算した値の名前を書けます。
allowance_ofの真ん中の行がtaperedというderiveを指しています。上下の行は、ページが書いている二つの金額そのものです。 - 「2 ポンドにつき 1 ポンド」は率の掛け算で、端数は丸めの宣言が決めます。 出力に書いた
round down(1GBP)がそれで、宣言は省けません。 - ページの「£12,571 から」は、ここでは「£12,570 を超える」と書いてあります。 単位がポンドなので同じ集合ですが、後者のほうが上の行と隣り合っていることを検査が読み取れます。
米国の連邦所得税を、段ごとに
2025 年分、単身者の連邦所得税です。IRS の税率表（Rev. Proc. 2024-40）からの転記で、日本の速算表と形は同じ — 段と、税率と、そこから足し始める金額。
rule us_income_tax v1
description "The 2025 federal income tax of an unmarried individual, transcribed from the IRS rate table. The English counterpart of 所得税.rule"
source irs = file "sources/us-tax-rate-tables.md" sha256:0abe29cfe35eeb22 # Rev. Proc. 2024-40, a US government work
table1 sha256:94648a4eb1ff7b80
inputs
taxable : money[USDc] range >=0USDc <=100000000000USDc # up to a billion dollars, in cents
outputs
tax : money[USDc] round down(1USDc)
# The table states each bracket as "$X plus Y% of the excess over $Z", so all three of X, Y
# and Z are transcribed and the arithmetic is written out below. Folding them into one
# deduction — the form Japan's own quick table uses — would be a number the source does not
# print, and E116 would be right to stop it.
#
# The citation sits on the rows rather than on the table: the first bracket is stated as
# "10% of the taxable income", with no amount in it, so its two zeros are this rule's way of
# writing that and not something the copy shows.
table brackets
policy unique
| taxable | -> base : money[USDc] | rate : rate[step 1%] | floor : money[USDc] |
| <=1192500USDc | 0USDc | 10% | 0USDc |
| >1192500USDc <=4847500USDc | 119250USDc | 12% | 1192500USDc | @irs table1
| >4847500USDc <=10335000USDc | 557850USDc | 22% | 4847500USDc | @irs table1
| >10335000USDc <=19730000USDc | 1765100USDc | 24% | 10335000USDc | @irs table1
| >19730000USDc <=25052500USDc | 4019900USDc | 32% | 19730000USDc | @irs table1
| >25052500USDc <=62635000USDc | 5723100USDc | 35% | 25052500USDc | @irs table1
| >62635000USDc | 18876975USDc | 37% | 62635000USDc | @irs table1
define excess : money[USDc] = taxable − floor
define tax : money[USDc] = base + excess × rate
examples
| taxable | -> tax |
| 1000000USDc | 100000USDc | # $10,000, all of it in the first bracket
| 1192500USDc | 119250USDc | # the top of the first bracket, which is the second one's base
| 5000000USDc | 591400USDc | # $50,000: $5,578.50 + 22% of $1,525
| 100000000USDc | 32702025USDc | # $1,000,000: $188,769.75 + 37% of $373,650
この例が見せていること
- 「$X plus Y% of the excess over $Z」は、三つの列と二行の計算になります。 base・rate・floor をそのまま転記し、
excessとtaxをdefineで書いています。控除額ひとつに畳むと、出典が印刷していない数が出てくるので、そうしていません。 - 最初の段にだけ出典が付いていません。 ページは「10% of the taxable income」と書くだけで金額を書いていないので、その行の二つのゼロは規則側の書き方です。出典は表ではなく行に付けてあり、行の出典は「その行がどこから来たか」だけを言います。
- ドルではなくセントです。 $1,192.50 は整数のドルではないので
money[USDc]で数えます。単位は型の一部なので、ドルとセントが取り違えられることもありません。
米国の連邦規則から、条ひとつ
消火器まで何フィート歩くことになるか。29 CFR 1910.157(d) の転記で、条文は eCFR から日付を指定して取ってきたコピーに留めてあります。日本の法令を e-Gov に留めるのと同じ仕組みが、そのまま英語圏の法令で動きます。
rule osha_extinguisher v1
description "How far an employee may have to walk to a portable fire extinguisher. Transcribed from 29 CFR 1910.157(d), read out of the eCFR"
# The rule an English-speaking reader gets from a statute database, as the Japanese rules get
# theirs from e-Gov: the section is fetched as of a date, kept as a copy beside the rule and
# pinned, and `rulec source outdated` asks the eCFR whether a later amendment touched it.
source osha = law ecfr "29 CFR 1910" asof 2026-01-01
"§1910.157" sha256:c2a9ce966c7e2269
enum fire_class = a | b | c | d
enum pattern = class_a | class_b
# (d)(5) sends a Class C hazard to "the appropriate pattern for the existing Class A or Class
# B hazards", so which of the two is present has to be an input. For the other three classes
# it is not read, and the `-` cells below say so.
inputs
hazard : fire_class
nearby : pattern
outputs
travel : length[ft] round down(1ft)
# The section states the distances in feet with the metre in brackets — "75 feet (22.9 m)" —
# so feet is the unit the rule is written in. A length is one integer in its declared unit,
# and there is no conversion to decide.
table distance @osha "§1910.157"
policy unique
| hazard | nearby | -> travel : length[ft] |
| a | - | 75ft |
| b | - | 50ft |
| c | class_a | 75ft |
| c | class_b | 50ft |
| d | - | 75ft |
examples
| hazard | nearby | -> travel |
| a | class_a | 75ft |
| b | class_a | 50ft |
| c | class_b | 50ft |
| d | class_a | 75ft |
この例が見せていること
- 法令データベースは
lawの後の語で選びます。law ecfr "29 CFR 1910"のecfrがそれで、省略すると e-Gov です。id は title と part、引くのは section ひとつです。 - 語として読めない箇所は引用符で囲みます。
@osha "§1910.157"のように。コピーはsources/law/29-CFR-1910@2026-01-01/1910.157.xmlに保存され、rulec source pinがそのハッシュを書きます。 rulec source outdatedが改正を教えます。 eCFR はその section の改正日を返し、体裁だけの直しかどうかも言うので、本文が動いたときだけ読み直しになります。- 単位はフィートです。 条文が「75 feet (22.9 m)」と書くので
length[ft]で転記しました。換算はしません。
英国の印紙税、本則と軽減
住宅の売買にかかる SDLT が、どの税率帯に入るか。GOV.UK からの転記で、本則の表と、初めて家を買う人の軽減の表という形が 印紙税の本則と軽減.rule とそのまま重なります。
rule uk_stamp_duty v1
description "The SDLT rate band a residential purchase falls in, and the surcharge on a second home. Transcribed from GOV.UK. The English counterpart of 印紙税の本則と軽減.rule"
source gov = file "sources/uk-sdlt.md" sha256:799106ea8a821a00 # GOV.UK, Open Government Licence v3.0
table1 sha256:360409a5675d3552
table2 sha256:15d4ed0baca64189
inputs
price : money[GBP] range >=0GBP <=20000000GBP
first_time : bool
additional : bool
outputs
band : rate[step 1%] round down(1%)
surcharge : rate[step 1%] round down(1%)
# The main rule. The first row carries no citation: the page writes that band as "Zero"
# rather than as a percentage, so `0%` is this rule's way of writing it.
table standard
policy unique
| price | -> band : rate[step 1%] |
| <=125000GBP | 0% |
| >125000GBP <=250000GBP | 2% | @gov table1
| >250000GBP <=925000GBP | 5% | @gov table1
| >925000GBP <=1500000GBP | 10% | @gov table1
| >1500000GBP | 12% | @gov table1
# The relief, which stops at £500,000: "If the price is over £500,000, you cannot claim".
# Above that the main rule shows through on its own, which is what `overrides` on a table
# that covers only part of the input space means. A first-time buyer who already owns a
# property is not one, so the rows say so rather than leaving it to the reader.
table first_time_relief @gov table2
policy unique
overrides standard
| first_time | additional | price | -> band : rate[step 1%] |
| true | false | <=300000GBP | 0% |
| true | false | >300000GBP <=500000GBP | 5% |
# "You'll usually have to pay 5% on top of SDLT rates if buying a new residential property
# means you'll own more than one" is a sentence, not a table, so this cites the document
# whole. What it is on top of is the band above; the two are not added here, because the tax
# itself is worked out slice by slice and the page tabulates no such total.
table second_home @gov
policy unique
| additional | -> surcharge : rate[step 1%] |
| true | 5% |
| false | 0% |
examples
| price | first_time | additional | -> band | surcharge |
| 100000GBP | false | false | 0% | 0% |
| 200000GBP | false | false | 2% | 0% |
| 200000GBP | true | false | 0% | 0% |
| 400000GBP | true | false | 5% | 0% |
| 600000GBP | true | false | 5% | 0% |
| 200000GBP | false | true | 2% | 5% |
| 2000000GBP | false | false | 12% | 0% |
この例が見せていること
- 軽減は途中で切れます。 「£500,000 を超えると使えない」と書いてあるので、軽減の表は £500,000 までしか行を持ちません。その上では本則がそのまま顔を出します。
overridesが「一部だけを覆う表」であるというのは、こういうことです。 - 最初の行にだけ出典が付いていません。 ページはその帯を「Zero」と書くだけで率を書いていないので、
0%は規則側の書き方です。 - 第二の住宅の 5% は文章です。 表ではないので、その行は文書を丸ごと引用しています（
@gov）。帯の率と足し合わせていないのは、税額そのものが帯ごとの積み上げで、ページがその合計を表にしていないからです。
騒音にどれだけさらしてよいか
29 CFR 1910.95 の Table G-16。dBA の水準ごとに一日の許容時間が決まります。条文は eCFR から日付を指定して取ってきたコピーに留めてあります。
rule osha_noise v1
description "The daily exposure to continuous noise a workplace may permit, from Table G-16 of 29 CFR 1910.95"
source osha = law ecfr "29 CFR 1910" asof 2026-01-01
"§1910.95" sha256:f83a1303a004b5ae
inputs
level : sound[dB] range >=90dB <=130dB
outputs
permitted : duration[min] round down(1min)
# Table G-16 lists nine levels and the time permitted at each: 8 hours at 90 dBA, 6 at 92,
# and so on down to a quarter of an hour at 115. A level between two of the listed ones is
# read here as **the shorter of the two** — 91 dBA is given the 92 dBA row — and that is a
# decision made here, not in the text. The appendix says the reference duration "is computed
# by" a formula, but the formula is a picture in the document and no text of it comes out of
# the copy; rounding the other way would permit longer exposure than the formula does, which
# is the wrong direction to be wrong in.
table exposure @osha "§1910.95"
policy first
| level | -> permitted : duration[min] |
| <=90dB | 480min |
| >90dB <=92dB | 360min |
| >92dB <=95dB | 240min |
| >95dB <=97dB | 180min |
| >97dB <=100dB | 120min |
| >100dB <=102dB | 90min |
| >102dB <=105dB | 60min |
| >105dB <=110dB | 30min |
| - | 15min |
examples
| level | -> permitted |
| 90dB | 480min |
| 92dB | 360min |
| 95dB | 240min |
| 100dB | 120min |
| 105dB | 60min |
| 110dB | 30min |
| 115dB | 15min |
| 91dB | 360min |
この例が見せていること
- 表に無い水準をどう読むかは、こちらで決めています。 91 dBA は 92 dBA の行として読む — つまり短いほうの時間を採ります。附録は許容時間が式で計算されると書いていますが、その式は文書の中では画像で、コピーのテキストには出てきません。逆に丸めると式より長くさらしてよいことになるので、そちらには倒しません。
- 音は比較と範囲だけの型です。
sound[dB]は足し算ができません。デシベルは対数なので、二つ足しても二つぶんの音にならないからです。 - 時間は分で持っています。 表に 1½ 時間と ¼ 時間があるので、時間単位では整数になりません。
duration[min]なら 90 分・15 分とそのまま書けます。
掘削に防護が要るかどうか
29 CFR 1926.652(a)(1)。同じ title の別の part なので、出典も別に宣言しています。答えは金額ではなく「要る／要らない」です。
rule osha_excavation v1
description "Whether an excavation needs a protective system against cave-ins, from 29 CFR 1926.652(a)(1)"
# A second part of the same title, and so a source of its own: the id names the part, and
# `rulec source fetch` brings the section from the eCFR as of the date on the line.
source osha = law ecfr "29 CFR 1926" asof 2026-01-01
"§1926.652" sha256:088a630a1ae9a4d7
enum verdict = required | not_required
# The section gives two exceptions. One is that the excavation "are made entirely in stable
# rock". The other is two conditions at once: less than five feet deep, **and** an
# examination by a competent person giving "no indication of a potential cave-in". What the
# rule asks for is the examination's answer, not whether one was made — no examination is not
# the same as one that found nothing, and the row for it is the one that requires the system.
inputs
depth : length[ft] range >=1ft <=30ft
stable_rock : bool
cave_in_indication : bool
outputs
protection : verdict
table needed @osha "§1926.652"
policy unique
| stable_rock | depth | cave_in_indication | -> protection : verdict |
| true | - | - | not_required |
| false | <5ft | false | not_required |
| false | <5ft | true | required |
| false | >=5ft | - | required |
examples
| depth | stable_rock | cave_in_indication | -> protection |
| 4ft | false | false | not_required |
| 4ft | false | true | required |
| 5ft | false | false | required |
| 12ft | true | true | not_required |
この例が見せていること
- 例外は二つで、片方は条件が二つあります。 岩盤だけを掘るとき、または「5 フィート未満で、資格のある者が見て崩落の兆候が無いとき」。後者が二列になっているのは、条文がそう書いているからです。
- 「調べていない」は「調べて何も無かった」ではありません。 だから入力は調査の結果であって、調査をしたかどうかではありません。調べていない現場は、兆候ありの行に落ちます。
- フィートで書いてあります。 条文が「5 feet (1.52m)」と書くので、そのまま
length[ft]です。
PayPal の決済手数料
米国の PayPal Checkout の手数料です。公開されている料金表からの転記で、法令ではなく事業者の規約から作った例。決済手数料.rule の英語圏版にあたります。
rule paypal_fee v1
description "The PayPal Checkout fee on one payment in the United States. Transcribed from PayPal's published merchant fees"
source paypal = file "sources/paypal-us-fees.md" sha256:0318950a982c3c7d # PayPal's own published figures
table1 sha256:5e481ef40e570eeb
inputs
amount : money[USDc] range >=1USDc <=100000000USDc
international : bool
# The fee has fractions of a cent in it, and the page does not say which way they settle, so
# the direction here is a placeholder — the thing a person has to decide before this ships.
outputs
fee : money[USDc] round half_up(1USDc)
# The page prints the domestic rate and, separately, what an international transaction adds.
# It does not print the sum, so neither does this: the row for a domestic payment adds
# nothing, and that row carries no citation because `0%` is not a figure the copy shows.
table surcharge
policy unique
| international | -> extra : rate[step 0.01%] |
| false | 0% |
| true | 1.5% | @paypal table1
define fee : money[USDc] = amount × 3.49% + amount × extra + 49USDc @paypal table1
examples
| amount | international | -> fee |
| 10000USDc | false | 398USDc |
| 10000USDc | true | 548USDc |
この例が見せていること
- 率と定額の両方が出典から来ています。 3.49% と 0.49 ドル。合計の率（4.99%）はページに無いので、こちらでも作りません。国際取引の 1.5% は別の行です。
- 丸めの向きは仮置きです。 セント未満が出るのにページが何も言っていないので、
half_upと書いたうえで「これは決め事の置き場所だ」と注に書いてあります。決めるのは人です。 - セントで数えています。
money[USDc]はセントの整数で、$0.49 は 49USDc。ドルとセントが取り違えられることはありません。
領収書の印紙税
国税庁タックスアンサー No.7141 の第17号文書（売上代金に係る金銭又は有価証券の受取書）の税額表です。受取金額のほかに、金額の記載があるか、営業に関するものかで決まります。
rule 領収書の印紙税(receipt_stamp) v1
description "売上代金に係る金銭又は有価証券の受取書（第17号の1文書）の印紙税額。5万円未満と、営業に関しないものは非課税"
inputs
受取金額(amount) : money[円] range >=0円 <=10000億円
金額の記載あり(stated) : bool
営業に関する(business) : bool
outputs
印紙税額(tax) : money[円] round down(1円)
table 税額(tax_table) # 出典: 国税庁 タックスアンサー No.7141 印紙税額の一覧表（その2）第17号文書（令和8年4月1日現在法令等）
policy unique
| 営業に関する | 金額の記載あり | 受取金額 | -> 印紙税額(tax) : money[円] |
| false | - | - | 0円 | # 営業に関しないものは非課税
| true | false | - | 200円 | # 受取金額の記載のないもの
| true | true | <5万円 | 0円 | # 非課税
| true | true | >=5万円 <=100万円 | 200円 |
| true | true | >100万円 <=200万円 | 400円 |
| true | true | >200万円 <=300万円 | 600円 |
| true | true | >300万円 <=500万円 | 1000円 |
| true | true | >500万円 <=1000万円 | 2000円 |
| true | true | >1000万円 <=2000万円 | 4000円 |
| true | true | >2000万円 <=3000万円 | 6000円 |
| true | true | >3000万円 <=5000万円 | 10000円 |
| true | true | >5000万円 <=1億円 | 20000円 |
| true | true | >1億円 <=2億円 | 40000円 |
| true | true | >2億円 <=3億円 | 60000円 |
| true | true | >3億円 <=5億円 | 100000円 |
| true | true | >5億円 <=10億円 | 150000円 |
| true | true | >10億円 | 200000円 |
examples
| 受取金額 | 金額の記載あり | 営業に関する | -> 印紙税額 |
| 49999円 | true | true | 0円 | # 5万円未満は非課税
| 50000円 | true | true | 200円 |
| 1000000円 | true | true | 200円 | # 100万円以下
| 1000001円 | true | true | 400円 | # 100万円を超え
| 0円 | false | true | 200円 | # 記載のないもの
| 3000000円 | true | false | 0円 | # 営業に関しないもの
この例が見せていること
- 非課税は 0 円の行です。 5 万円未満と、営業に関しないものは非課税で、表はそれを
0円の行として持ちます。「課税されない」も規則の答えのひとつです。 - 金額の記載が無いものは金額を見ません。
金額の記載ありが false の行は受取金額の列が-で、いくらでも 200 円です。三つの入力のどの組み合わせもちょうど一行に当たることを、検査が証明しています。
所得税の速算表
国税庁タックスアンサー No.2260 の速算表です。課税される所得金額の段ごとに税率と控除額があり、課税所得 × 税率 − 控除額 で所得税が出ます。復興特別所得税はその 2.1% です。
rule 所得税(income_tax) v1
description "所得税の速算表。課税される所得金額に税率を掛けて控除額を引き、復興特別所得税を上乗せする"
inputs
課税所得(taxable) : money[円] range >=1000円 <=100億円 # 1,000円未満の端数を切り捨てた後の金額。速算表は 1,000円 から始まる
outputs
所得税(tax) : money[円] round down(1円) # 課税所得が 1,000円 単位で税率が整数の % なので、端数は出ない
復興特別所得税(surtax) : money[円] round down(1円) # 基準所得税額の 2.1%。1円未満の端数の扱いはこのページに無いので、切り捨てに仮置き
# 速算表は「1,000円 から 1,949,000円まで」「1,950,000円 から」のように書く。課税所得は 1,000円 単位なので、
# 各段の上端は次の段の始まりの手前と同じこと。ここではそのまま「次の段の始まり未満」と書く。
table 速算表(brackets) # 出典: 国税庁 タックスアンサー No.2260 所得税の税率（令和8年4月1日現在法令等）
policy unique
| 課税所得 | -> 税率(rate) : rate[step 1%] | 控除額(deduction) : money[円] |
| <1950000円 | 5% | 0円 |
| >=1950000円 <3300000円 | 10% | 97500円 |
| >=3300000円 <6950000円 | 20% | 427500円 |
| >=6950000円 <9000000円 | 23% | 636000円 |
| >=9000000円 <18000000円 | 33% | 1536000円 |
| >=18000000円 <40000000円 | 40% | 2796000円 |
| >=40000000円 | 45% | 4796000円 |
define 所得税(tax) : money[円] = 課税所得 × 税率 − 控除額
define 復興特別所得税(surtax) : money[円] = 所得税 × 2.1% # 出典: 同ページ「基準所得税額の2.1パーセント」
examples
| 課税所得 | -> 所得税 | 復興特別所得税 |
| 7000000円 | 974000円 | 20454円 | # 同ページの計算例: 7,000,000円 × 0.23 − 636,000円 = 974,000円
| 1949000円 | 97450円 | 2046円 | # 5% の段の上端。2,046.45円 → 切り捨て（仮置き）
| 1950000円 | 97500円 | 2047円 | # 10% の段の下端。控除額のおかげで上の行と 50円 しか違わない
この例が見せていること
- 一つの表が率と金額を同時に出します。 税率の列は
rate[step 1%]、控除額の列はmoney[円]で、defineがその二つを掛けて引きます。ページの計算例（7,000,000円 × 0.23 − 636,000円 = 974,000円）が、そのままexamplesの行です。 - 段の境目は「次の段の始まり未満」で書いています。 ページは「1,000円 から 1,949,000円まで」「1,950,000円 から」と書きますが、課税所得は 1,000円 単位なので同じことです。整数の全体で完全性を証明するには、隙間の無い書き方のほうが要ります。
- 書いていないことは仮置きと明記します。 復興特別所得税に 1 円未満の端数が出たときの扱いは、このページにはありません。
round downに仮置きして、宣言の横のコメントに出典が無いことを残しています。読む人はrulec docでそれを読みます。
契約書の印紙税と、期限つきの軽減税率
不動産の譲渡に関する契約書（第1号文書）の印紙税額です。本則（No.7140）と、令和9年3月31日までに作成された契約書の軽減税率（No.7108）を一つの表に持ちます。作成日が入力です。
rule 印紙税(stamp_duty) v1
description "不動産の譲渡に関する契約書（第1号文書）の印紙税額。記載された契約金額と作成日で決まり、令和9年3月31日までに作成されたものは軽減税率"
inputs
契約金額(amount) : money[円] range >=0円 <=10000億円
金額の記載あり(stated) : bool
作成日(made) : date range >=2014-04-01 <=2030-12-31 # 軽減措置の始まり（平成26年4月1日）から
outputs
印紙税額(tax) : money[円] round down(1円)
define 軽減期間(reduced) : bool = 作成日 <= 2027-03-31 # 出典: No.7108。平成26年4月1日から令和9年3月31日までの間に作成される契約書。始まりは入力の範囲の下端
# 軽減税率は契約金額が 10万円 を超えるものだけ（No.7108）。10万円以下は期間によらず本則で、記載のないものは 200円。
table 税額(tax_table) # 出典: 国税庁 タックスアンサー No.7140 印紙税額の一覧表（その1）第1号文書、No.7108 不動産の譲渡契約書等の印紙税の軽減措置（令和8年4月1日現在法令等）
policy unique
| 金額の記載あり | 軽減期間 | 契約金額 | -> 印紙税額(tax) : money[円] |
| false | - | - | 200円 | # 契約金額の記載のないもの
| true | - | <1万円 | 0円 | # 非課税
| true | - | >=1万円 <=10万円 | 200円 |
| true | true | >10万円 <=50万円 | 200円 | # ここから軽減後の税額（No.7108）
| true | true | >50万円 <=100万円 | 500円 |
| true | true | >100万円 <=500万円 | 1000円 |
| true | true | >500万円 <=1000万円 | 5000円 |
| true | true | >1000万円 <=5000万円 | 10000円 |
| true | true | >5000万円 <=1億円 | 30000円 |
| true | true | >1億円 <=5億円 | 60000円 |
| true | true | >5億円 <=10億円 | 160000円 |
| true | true | >10億円 <=50億円 | 320000円 |
| true | true | >50億円 | 480000円 |
| true | false | >10万円 <=50万円 | 400円 | # ここから本則の税額（No.7140）
| true | false | >50万円 <=100万円 | 1000円 |
| true | false | >100万円 <=500万円 | 2000円 |
| true | false | >500万円 <=1000万円 | 10000円 |
| true | false | >1000万円 <=5000万円 | 20000円 |
| true | false | >5000万円 <=1億円 | 60000円 |
| true | false | >1億円 <=5億円 | 100000円 |
| true | false | >5億円 <=10億円 | 200000円 |
| true | false | >10億円 <=50億円 | 400000円 |
| true | false | >50億円 | 600000円 |
examples
| 契約金額 | 金額の記載あり | 作成日 | -> 印紙税額 |
| 30000000円 | true | 2026-09-16 | 10000円 | # 3,000万円の売買契約。軽減期間なので 1万円（本則は 2万円）
| 30000000円 | true | 2027-04-01 | 20000円 | # 軽減期間が終わった翌日
| 100000円 | true | 2026-09-16 | 200円 | # 10万円ちょうどは軽減の対象外で、本則も 200円
| 5000円 | true | 2026-09-16 | 0円 | # 1万円未満は非課税
| 0円 | false | 2026-09-16 | 200円 | # 契約金額の記載のないもの
この例が見せていること
- 期限のある特例は、日付の定義と一つの列になります。
define 軽減期間 = 作成日 <= 2027-03-31を列に置き、軽減の行はtrue、本則の行はfalse、期間によらない行は-です。policy uniqueなので、どの契約金額もどの作成日も、ちょうど一行に当たることが証明されています。 - 軽減の対象外は本則の行が受けます。 軽減は契約金額が 10 万円を超えるものだけなので、1 万円未満（非課税）と 10 万円以下の行は、期間の列が
-です。 - この規則がジェネレーターの欠陥を一つ見つけました。 定義の中の日付リテラルが、全言語で 0 として生成されていました。参照評価器は正しく読んでいたので、
rulec testの突き合わせで食い違いとして出ました。
厚生年金保険料の等級表
日本年金機構の厚生年金保険料額表（令和8年度版）です。32 等級で、料率は一般の被保険者なら 18.3% ですが、厚生年金基金の加入員は基金ごとに違うので入力にしてあります。
rule 厚生年金保険料(pension_premium) v1
description "厚生年金保険料。報酬月額から標準報酬月額を引き、料率を掛けて折半し、給与から控除する額と現金で納める額を出す"
source 機構 = file "sources/nenkin/R08ryougaku.xlsx" sha256:462a199ad4f3b69c # 日本年金機構 令和2年9月分（10月納付分）からの厚生年金保険料額表（令和8年度版）
表1 sha256:09a23ce9620373c4
inputs
報酬月額(monthly) : money[円] range >=0円 <=1000万円
料率(rate) : rate[step 0.1%] range >=0% <=30% # 一般・坑内員・船員は 18.3%。厚生年金基金の加入員は基金ごとに 13.3%〜15.9% なので入力にする
outputs
標準報酬月額(std) : money[円] round down(1円)
給与控除額(deduct) : money[円] round half_down(1円) # 出典: 保険料額表の注記①。給与から控除するとき、50銭以下は切り捨て、50銭を超えれば切り上げ
現金納付額(cash) : money[円] round half_up(1円) # 出典: 保険料額表の注記②。現金で納めるとき、50銭未満は切り捨て、50銭以上は切り上げ
table 等級(grade) @機構 表1 # 保険料額表の 1〜32 等級をそのまま転記した
policy unique
| 報酬月額 | -> 標準報酬月額(std) : money[円] |
| <93000円 | 88000円 |
| >=93000円 <101000円 | 98000円 |
| >=101000円 <107000円 | 104000円 |
| >=107000円 <114000円 | 110000円 |
| >=114000円 <122000円 | 118000円 |
| >=122000円 <130000円 | 126000円 |
| >=130000円 <138000円 | 134000円 |
| >=138000円 <146000円 | 142000円 |
| >=146000円 <155000円 | 150000円 |
| >=155000円 <165000円 | 160000円 |
| >=165000円 <175000円 | 170000円 |
| >=175000円 <185000円 | 180000円 |
| >=185000円 <195000円 | 190000円 |
| >=195000円 <210000円 | 200000円 |
| >=210000円 <230000円 | 220000円 |
| >=230000円 <250000円 | 240000円 |
| >=250000円 <270000円 | 260000円 |
| >=270000円 <290000円 | 280000円 |
| >=290000円 <310000円 | 300000円 |
| >=310000円 <330000円 | 320000円 |
| >=330000円 <350000円 | 340000円 |
| >=350000円 <370000円 | 360000円 |
| >=370000円 <395000円 | 380000円 |
| >=395000円 <425000円 | 410000円 |
| >=425000円 <455000円 | 440000円 |
| >=455000円 <485000円 | 470000円 |
| >=485000円 <515000円 | 500000円 |
| >=515000円 <545000円 | 530000円 |
| >=545000円 <575000円 | 560000円 |
| >=575000円 <605000円 | 590000円 |
| >=605000円 <635000円 | 620000円 |
| >=635000円 | 650000円 |
define 折半額(half) : money[円] = 標準報酬月額 × 料率 ÷ 2 # 全額の折半。円未満の端数は上の二つの出力の丸めで決まる
define 給与控除額(deduct) : money[円] = 折半額
define 現金納付額(cash) : money[円] = 折半額
examples
| 報酬月額 | 料率 | -> 標準報酬月額 | 給与控除額 | 現金納付額 |
| 90000円 | 18.3% | 88000円 | 8052円 | 8052円 | # 表の 1 等級。全額 16,104.00円、折半額 8,052.00円
| 250000円 | 18.3% | 260000円 | 23790円 | 23790円 | # 表の 17 等級。250,000円以上 270,000円未満
| 700000円 | 18.3% | 650000円 | 59475円 | 59475円 | # 表の 32 等級（上限）。折半額 59,475.00円
この例が見せていること
- 健康保険料と同じ形です。 表が 50 等級から 32 等級になり、上限が 650,000 円になるだけで、折半と二つの端数処理はそのままです。同じ形の規則は、同じ形に転記できます。
- この表では二つの端数処理が同じ答えになります。 18.3% × 標準報酬月額は必ず偶数の円なので、折半額に端数が出ません。規則には二つの丸め方が書いてありますが、この料率では表に現れない、ということまで
examplesが示しています。 - 印刷された 32 等級すべてと突き合わせてあります。 表の折半額を転記した記録（
tests/oracle/）にrulec replayを当て、全件一致することをテストが確かめます。 - 転記元の Excel に縛ってあります。
sourceが日本年金機構の保険料額表（.xlsx）そのものを指し、@機構 表1がその一枚目のシートを引きます。rulec source fetchがシートを取り出して規則の隣に置き、以後rulec checkは、この表の 32 個の標準報酬月額がそのコピーに出てくる値であることを確かめます（E116）。470000円を480000円と転記すれば、刻みにも載っていて抜けも重なりもないのに、そこだけが落ちます。
保険料額表を転記して、二つの端数処理を出す
協会けんぽの保険料額表（東京支部、令和8年3月分から）です。報酬月額から 50 等級の標準報酬月額を引き、料率を掛けて折半します。円未満の端数は、給与から控除するときと現金で納めるときで丸め方が違います。この表を転記するために half_down が言語に入りました。
rule 健康保険料(kenpo_premium) v1
description "協会けんぽの健康保険料。報酬月額から標準報酬月額を引き、料率を掛けて折半し、給与から控除する額と現金で納める額を出す"
inputs
報酬月額(monthly) : money[円] range >=0円 <=1000万円
健康保険料率(rate) : rate[step 0.01%] range >=0% <=20% # 都道府県ごと、年度ごとに変わるので入力にする
介護保険料率(care_rate) : rate[step 0.01%] range >=0% <=5% # 介護保険第2号被保険者（40〜64歳）に加わる分
介護該当(care) : bool
outputs
標準報酬月額(std) : money[円] round down(1円)
給与控除額(deduct) : money[円] round half_down(1円) # 出典: 保険料額表の注記①。給与から控除するとき、50銭以下は切り捨て、50銭を超えれば切り上げ
現金納付額(cash) : money[円] round half_up(1円) # 出典: 保険料額表の注記②。現金で納めるとき、50銭未満は切り捨て、50銭以上は切り上げ
derive 合算率(both) : rate[step 0.01%] = 健康保険料率 + 介護保険料率 range >=0% <=25%
table 等級(grade) # 出典: 全国健康保険協会 令和8年3月分（4月納付分）からの健康保険・厚生年金保険の保険料額表（東京支部）
policy unique
| 報酬月額 | -> 標準報酬月額(std) : money[円] |
| <63000円 | 58000円 |
| >=63000円 <73000円 | 68000円 |
| >=73000円 <83000円 | 78000円 |
| >=83000円 <93000円 | 88000円 |
| >=93000円 <101000円 | 98000円 |
| >=101000円 <107000円 | 104000円 |
| >=107000円 <114000円 | 110000円 |
| >=114000円 <122000円 | 118000円 |
| >=122000円 <130000円 | 126000円 |
| >=130000円 <138000円 | 134000円 |
| >=138000円 <146000円 | 142000円 |
| >=146000円 <155000円 | 150000円 |
| >=155000円 <165000円 | 160000円 |
| >=165000円 <175000円 | 170000円 |
| >=175000円 <185000円 | 180000円 |
| >=185000円 <195000円 | 190000円 |
| >=195000円 <210000円 | 200000円 |
| >=210000円 <230000円 | 220000円 |
| >=230000円 <250000円 | 240000円 |
| >=250000円 <270000円 | 260000円 |
| >=270000円 <290000円 | 280000円 |
| >=290000円 <310000円 | 300000円 |
| >=310000円 <330000円 | 320000円 |
| >=330000円 <350000円 | 340000円 |
| >=350000円 <370000円 | 360000円 |
| >=370000円 <395000円 | 380000円 |
| >=395000円 <425000円 | 410000円 |
| >=425000円 <455000円 | 440000円 |
| >=455000円 <485000円 | 470000円 |
| >=485000円 <515000円 | 500000円 |
| >=515000円 <545000円 | 530000円 |
| >=545000円 <575000円 | 560000円 |
| >=575000円 <605000円 | 590000円 |
| >=605000円 <635000円 | 620000円 |
| >=635000円 <665000円 | 650000円 |
| >=665000円 <695000円 | 680000円 |
| >=695000円 <730000円 | 710000円 |
| >=730000円 <770000円 | 750000円 |
| >=770000円 <810000円 | 790000円 |
| >=810000円 <855000円 | 830000円 |
| >=855000円 <905000円 | 880000円 |
| >=905000円 <955000円 | 930000円 |
| >=955000円 <1005000円 | 980000円 |
| >=1005000円 <1055000円 | 1030000円 |
| >=1055000円 <1115000円 | 1090000円 |
| >=1115000円 <1175000円 | 1150000円 |
| >=1175000円 <1235000円 | 1210000円 |
| >=1235000円 <1295000円 | 1270000円 |
| >=1295000円 <1355000円 | 1330000円 |
| >=1355000円 | 1390000円 |
table 適用料率(applied) # 介護保険第2号被保険者は、健康保険料率に介護保険料率を足した率になる
policy unique
| 介護該当 | -> 料率(applied_rate) : rate[step 0.01%] |
| true | 合算率 |
| false | 健康保険料率 |
define 折半額(half) : money[円] = 標準報酬月額 × 料率 ÷ 2 # 全額の折半。円未満の端数は上の二つの出力の丸めで決まる
define 給与控除額(deduct) : money[円] = 折半額
define 現金納付額(cash) : money[円] = 折半額
examples
| 報酬月額 | 健康保険料率 | 介護保険料率 | 介護該当 | -> 標準報酬月額 | 給与控除額 | 現金納付額 |
| 60000円 | 9.85% | 1.62% | false | 58000円 | 2856円 | 2857円 | # 折半額 2,856.5円。給与控除は切り捨て、現金納付は切り上げ
| 134000円 | 9.85% | 1.62% | false | 134000円 | 6599円 | 6600円 | # 折半額 6,599.5円
| 134000円 | 9.85% | 1.62% | true | 134000円 | 7685円 | 7685円 | # 折半額 7,684.9円。どちらも切り上げ
| 300000円 | 9.85% | 1.62% | true | 300000円 | 17205円 | 17205円 | # 折半額 17,205.0円
この例が見せていること
- 同じ折半額から、丸め方の違う二つの出力を返します。 表の注記は、給与から控除するなら「50銭以下は切り捨て、50銭を超える場合は切り上げ」、現金で納めるなら「50銭未満は切り捨て、50銭以上は切り上げ」と書いています。後者は
half_up、前者はhalf_downです。折半額が 6,599.5 円の等級で、二つの出力は 1 円違います。 - 料率は入力です。 都道府県ごと、年度ごとに変わるものを規則に焼き込むと、改定のたびに表を書き換えることになります。
deriveで健康保険料率と介護保険料率を足し、介護保険第2号被保険者かどうかで、表が使う率を選びます。 - 表の全等級と突き合わせてあります。 印刷された折半額を転記した記録（
tests/oracle/）にrulec replayを当て、100 件すべてで一致することをテストが確かめます。
本則と特例を二つの表に分け、出典に縛る
上の印紙税と同じ決まりを、印紙税法の別表第一（本則）と、租税特別措置法第 91 条（軽減）の二つの表に分け、非課税の決まりを節にしたものです。それぞれの表が自分の出典を引用し、出典は政府の法令データベース（e-Gov 法令検索）から取った条文のコピーのハッシュに縛られています。
rule 印紙税の本則と軽減(stamp_duty_split) v1
description "不動産の譲渡に関する契約書（第1号文書）の印紙税額。本則の表に、令和9年3月31日までの軽減税率の表が優先する"
source 法 = law "342AC0000000023" asof 2026-04-01
別表第一 sha256:0ba69792e960021e
source 措置法 = law "332AC0000000026" asof 2026-04-01
第91条 sha256:85faf53f6f6e8196
inputs
契約金額(amount) : money[円] range >=0円 <=10000億円
金額の記載あり(stated) : bool
作成日(made) : date range >=2014-04-01 <=2030-12-31
outputs
印紙税額(tax) : money[円] round down(1円)
define 軽減期間(reduced) : bool = 作成日 <= 2027-03-31 @措置法 第91条
table 本則(base) @法 別表第一 # 第1号文書の欄
policy unique
| 金額の記載あり | 契約金額 | -> 印紙税額(tax) : money[円] |
記載なし | false | - | 200円 |
r3 | true | >=1万円 <=10万円 | 200円 |
r4 | true | >10万円 <=50万円 | 400円 |
r5 | true | >50万円 <=100万円 | 1000円 |
r6 | true | >100万円 <=500万円 | 2000円 |
r7 | true | >500万円 <=1000万円 | 10000円 |
r8 | true | >1000万円 <=5000万円 | 20000円 |
r9 | true | >5000万円 <=1億円 | 60000円 |
r10 | true | >1億円 <=5億円 | 100000円 |
r11 | true | >5億円 <=10億円 | 200000円 |
r12 | true | >10億円 <=50億円 | 400000円 |
r13 | true | >50億円 | 600000円 |
clause 非課税(exempt) -> 印紙税額 @法 別表第一 # 第1号文書の非課税物件の欄（記載された契約金額が1万円未満のもの）
when 金額の記載あり true and 契約金額 <1万円
then 0円
table 軽減(reduced_rate) @措置法 第91条
policy unique
overrides 本則
| 軽減期間 | 金額の記載あり | 契約金額 | -> 印紙税額 |
| true | true | >10万円 <=50万円 | 200円 |
| true | true | >50万円 <=100万円 | 500円 |
| true | true | >100万円 <=500万円 | 1000円 |
| true | true | >500万円 <=1000万円 | 5000円 |
| true | true | >1000万円 <=5000万円 | 10000円 |
| true | true | >5000万円 <=1億円 | 30000円 |
| true | true | >1億円 <=5億円 | 60000円 |
| true | true | >5億円 <=10億円 | 160000円 |
| true | true | >10億円 <=50億円 | 320000円 |
| true | true | >50億円 | 480000円 |
examples
| 契約金額 | 金額の記載あり | 作成日 | -> 印紙税額 |
| 30000000円 | true | 2026-09-16 | 10000円 |
| 30000000円 | true | 2027-04-01 | 20000円 |
| 100000円 | true | 2026-09-16 | 200円 |
| 5000円 | true | 2026-09-16 | 0円 |
| 0円 | false | 2026-09-16 | 200円 |
この例が見せていること
overrides 本則が、特例を本則に優先させます。 一つの表に軽減期間の列を足す代わりに、原文ごとに表を分けて、どちらが勝つかを一行で書きます。検査は二つの表をまとめて、完全性と重なりを見ます。- 非課税の決まりは
clauseです。 別表第一では、非課税の物件は課税物件の表の外の欄に書かれているので、表の行にはせず文のまま書いています。 sourceと@が出典を縛ります。rulec source fetchが e-Gov から別表第一と第 91 条のコピーを取り、rulec source pinがハッシュを書きます。条文が変われば、その箇所を引用している表を挙げて止まります（E038）。- 行のラベル（
r1…）は、記録に出る名前であり、overrides 本則:r3のように行を指す名前です。
ただし書を、文のまま書く
運賃表が基本運賃を決め、送料は二つの節で決まります。本文の「通常」と、会員の 3,900 円以上の注文を無料にするただし書です。ただし書は条件が列に並ばないので、表ではなく clause で書いています。
rule 送料のただし書(shipping_proviso) v1
description "通常便の送料。運賃表で基本運賃を決め、会員の 3,900円 以上の注文を無料にするただし書が本則に優先する（DESIGN.md §15.67 のスケッチ）"
import std/都道府県
enum サイズ区分(size_class) = S60(s60) | S80(s80)
group 遠隔地 = 北海道, 沖縄県
inputs
あて先(dest) : 都道府県
サイズ(size) : サイズ区分
会員(member) : bool
注文金額(total) : money[円] range >=0円 <=1000万円
outputs
送料(fee) : money[円] round up(10円)
table 運賃表(fee_table) # 出典: 基本運賃表（スケッチ）別表第一
policy unique
| あて先 | サイズ | -> 基本運賃(base) : money[円] |
| 遠隔地 | S60 | 1150円 |
| 遠隔地 | S80 | 1400円 |
| not: 遠隔地 | S60 | 820円 |
| not: 遠隔地 | S80 | 1050円 |
clause 通常(regular) -> 送料 # 出典: 第3条第1項（本文）
when always
then 基本運賃
clause 無料(free) -> 送料 # 出典: 第3条第2項ただし書
when 注文金額 >=3900円 and 会員 true
then 0円
overrides 通常
examples
| あて先 | サイズ | 会員 | 注文金額 | -> 送料 |
| 北海道 | S60 | true | 3900円 | 0円 |
| 北海道 | S60 | true | 3899円 | 1150円 |
| 東京都 | S80 | false | 10000円 | 1050円 |
この例が見せていること
clauseは一行の表です。whenに条件、thenに値。検査も生成も記録も表と同じで、記録には{"table":"無料","row":1}と出ます。overrides 通常で、ただし書が本文に優先します。 人が読む資料は「節 無料 は 節 通常 に優先します。交わる 1 対のすべてで、無料の行は通常の行に収まります（例外）」と書きます。- 別名の無い群（
group 遠隔地 = 北海道, 沖縄県）も書けます。生成コードではg1のような番号つきの名前になります。
準用される側の規則
次の例が準用する元の規則です。勤続年数と退職事由で支給月数を決め、自己都合退職の減額の節が本則に優先します。実在の法令ではなく、設計文書の例を規則にしたものです。
rule 退職手当(retirement_allowance) v1
description "退職手当の本則。勤続年数で支給月数を決め、自己都合退職の減額が本則に優先する（DESIGN.md §15.69 のスケッチ）"
enum 事由(reason_kind) = 定年(retirement_age) | 自己都合(voluntary) | 死亡(death)
inputs
勤続年数(years) : number range >=1 <=40
退職事由(reason) : 事由
基本給(base_pay) : money[円] range >=10万円 <=100万円
outputs
手当(allowance) : money[円] round down(1円)
table 支給表(schedule) # 出典: 第20条第1項（スケッチ）
policy unique
| 勤続年数 | 退職事由 | -> 支給月数(months) : number |
短期 | <10 | 定年, 自己都合 | 5 |
中期 | >=10 <25 | 定年, 自己都合 | 20 |
長期 | >=25 | 定年, 自己都合 | 40 |
死亡 | - | 死亡 | 40 |
define 満額(full) : money[円] = 基本給 × 支給月数
define 減額後(reduced) : money[円] = 満額 × 80%
clause 本則(main) -> 手当 # 出典: 第20条第1項（スケッチ）
when always
then 満額
clause 減額(reduction) -> 手当 # 出典: 第20条第2項（スケッチ）
when 退職事由 自己都合
then 減額後
overrides 本則
examples
| 勤続年数 | 退職事由 | 基本給 | -> 手当 |
| 3 | 定年 | 30万円 | 150万円 |
| 3 | 自己都合 | 30万円 | 120万円 |
| 30 | 死亡 | 30万円 | 1200万円 |
この例が見せていること
- この規則は単独で検査され、単独で生成できます。 準用する側は、このファイルのハッシュを見出しに書いて縛ります。
減額の節は、準用する側がexceptで外せます。 「第 20 条（第 2 項を除く。）の規定は…準用する」の形です。
ほかの規則を読み替えて準用する
上の退職手当の規則を、非常勤職員に準用します。「勤続年数」を「在職期間」と、「退職事由」を「任期終了事由」と読み替え、減額の節は準用しません。
rule 非常勤退職手当(part_time_allowance) v1
description "非常勤職員の退職手当。退職手当の規定を、在職期間と任期終了事由に読み替えて準用し、減額の規定は準用しない（DESIGN.md §15.69 のスケッチ）"
enum 終了事由(end_kind) = 任期満了(term_end) | 辞職(resignation)
inputs
在職期間(tenure) : number range >=1 <=3
任期終了事由(end_reason) : 終了事由
報酬月額(monthly_pay) : money[円] range >=10万円 <=50万円
outputs
非常勤手当(allowance) : money[円] round down(1円)
apply 退職手当(retirement) = "退職手当.rule" meaning:6812e6cdf8088ad4 # 出典: 第31条（スケッチ）
勤続年数 = 在職期間
退職事由 = 任期終了事由 with 任期満了 -> 定年, 辞職 -> 自己都合
基本給 = 報酬月額
except 減額
手当 -> 非常勤手当
examples
| 在職期間 | 任期終了事由 | 報酬月額 | -> 非常勤手当 |
| 3 | 任期満了 | 30万円 | 150万円 |
| 3 | 辞職 | 30万円 | 150万円 |
この例が見せていること
- 読み替えは
<元の規則の入力> = <この規則の値>です。 列挙どうしはwith 任期満了 -> 定年, 辞職 -> 自己都合で値を対応づけます。 - 渡す値が元の規則の範囲に収まることを check が確かめます（E043）。 在職期間は 1〜3 年で、勤続年数の 1〜40 年に収まります。0 から書けば、その値を例に挙げて止まります。
- 元の規則の表は、この規則の中に展開されて検査・生成されます。 記録は
{"table":"退職手当:支給表","row":1,"label":"短期"}と、元の表の名前で返ります。勤続年数 10 年以上の行はこの規則では当たらないので、エラーにはせず、人が読む資料に「この準用では当たらない行」として挙がります。 - 元の規則が変われば E040 で止まります。
rulec diffで何件いくら動くかを見て、それでよければrulec source pinでハッシュを書き直します。
温度と容量で、貼る表示を決める
食品の保存基準を転記したものです。摂氏の温度、ミリリットルの容量、そして「まだ決まっていない」を持てる列が一度に出てきます。
rule 保存基準(storage) v1
description "食品の保存温度と容量から、貼る表示と取るべき措置を決める（食品衛生法の規格基準のスケッチ）"
enum 区分(kind) = 冷凍(frozen) | 冷蔵(chilled) | 常温(ambient)
enum 措置(action) = 適合(ok) | 要冷却(cool) | 廃棄(discard)
inputs
保存温度(temp) : temperature[℃] range >=-30℃ <=40℃
容量(volume) : volume[mL] range >=0mL <=5000mL
表示区分(label) : 区分
再検区分(recheck) : 区分?
outputs
判定(verdict) : 措置
表示(text) : string
table 温度判定(temp_of)
policy unique
| 表示区分 | 保存温度 | -> 適温(in_range) : bool |
| 冷凍 | <=-15℃ | true |
| 冷凍 | >-15℃ | false |
| 冷蔵 | >=0℃ <=10℃ | true |
| 冷蔵 | <0℃ | false |
| 冷蔵 | >10℃ | false |
| 常温 | - | true |
table 再検判定(recheck_of)
policy unique
| 再検区分 | 容量 | -> 小分け(small) : bool |
| none | - | false |
| 冷凍 | - | true |
| 冷蔵 | <=1000mL | true |
| 冷蔵 | >1000mL | false |
| 常温 | - | false |
table 措置判定(action_of)
policy first
| 適温 | 小分け | 保存温度 | -> 判定(verdict) : 措置 | 表示(text) : string |
| true | - | - | 適合 | "適合" |
| false | true | - | 要冷却 | "要冷却・小分け" |
| false | - | >25℃ | 廃棄 | "廃棄" |
| false | - | - | 要冷却 | "要冷却" |
examples
| 保存温度 | 容量 | 表示区分 | 再検区分 | -> 判定 | 表示 |
| -20℃ | 500mL | 冷凍 | none | 適合 | "適合" |
| -10℃ | 500mL | 冷凍 | 冷凍 | 要冷却 | "要冷却・小分け" |
| 5℃ | 1000mL | 冷蔵 | none | 適合 | "適合" |
| 30℃ | 2000mL | 冷蔵 | 冷蔵 | 廃棄 | "廃棄" |
| 15℃ | 500mL | 冷蔵 | none | 要冷却 | "要冷却" |
この例が見せていること
- 温度は比べるだけの型です。
℃は 0 が「無い」を意味しない目盛りなので、足し算も倍にすることもできません。書けるのは比較とrangeだけで、気温 - 気温は E048 で止まります。 区分?は、値がまだ無いことを持てる列です。 セルのnoneでだけ受けられて、式には出てきません。null を算術から締め出すために、表で場合分けさせる形になっています。- 出力は文字列でもかまいません。 貼る表示のように、そのまま人が読む値です。ただし文字列は表の入力の列にはできません（E110）——分岐を決める値は列挙にします。
面積と騒音と残業から、措置と負担を決める
事務所衛生基準規則と騒音障害防止のスケッチです。面積・音量・時間という三つの次元と、入力どうしの関係の宣言が出てきます。
rule 事務所の衛生基準(office_standard) v1
description "床面積と天井高から気積を、騒音と残業時間と合わせて、事業者が取る措置と負担額を決める（事務所衛生基準規則と騒音障害防止のスケッチ）"
enum 措置(action) = 適合(ok) | 要改善(improve) | 使用停止(stop)
inputs
在籍(people) : number range >=1 <=200
床面積(floor) : area[m2] range >=1m2 <=2000m2
占有面積(used) : area[m2] range >=1m2 <=2000m2
騒音(noise) : sound[dB] range >=0dB <=130dB
残業(overtime) : duration[h] range >=0h <=200h
# 占有している面積が床面積を超えることはない。検査はこの外側に行を求めない
constraint 占有面積 <= 床面積
outputs
判定(verdict) : 措置
負担額(cost) : money[円, incl_tax] round half_even(100円)
derive 余裕(spare) : area[m2] = 床面積 - 占有面積 range >=-1999m2 <=1999m2
table 広さ判定(space_of)
policy first
| 余裕 | -> 狭い(tight) : bool |
| <10m2 | true |
| - | false |
table 措置判定(action_of)
policy first
| 騒音 | 残業 | 狭い | 在籍 | -> 判定(verdict) : 措置 | 率(rate) : rate[step 10%] |
| >=90dB | - | - | - | 使用停止 | 100% |
| >=85dB | - | - | - | 要改善 | 50% |
| - | >45h | - | - | 要改善 | 50% |
| - | - | true | >=50 | 使用停止 | 100% |
| - | - | true | - | 要改善 | 30% |
| - | - | - | - | 適合 | 0% |
define 負担額(cost) : money[円, incl_tax] = 10000円 × 率
examples
| 在籍 | 床面積 | 占有面積 | 騒音 | 残業 | -> 判定 | 負担額 |
| 10 | 100m2 | 50m2 | 60dB | 10h | 適合 | 0円 |
| 10 | 100m2 | 95m2 | 60dB | 10h | 要改善 | 3000円 |
| 10 | 100m2 | 50m2 | 86dB | 10h | 要改善 | 5000円 |
| 10 | 100m2 | 50m2 | 95dB | 10h | 使用停止 | 10000円 |
| 10 | 100m2 | 50m2 | 60dB | 60h | 要改善 | 5000円 |
この例が見せていること
constraint 占有面積 <= 床面積は、呼び出し側が守ると約束した関係です。 検査はその外側に行を求めず、診断が返す入力は必ず実在しうる一件になり、生成コードは違反する入力を入口で受け付けません。- 面積は長さの積ではなく、独立した次元です。
縦 × 横は E103 で止まります——このツールは次元解析をしないので、積を入れる次元を黙って作ることはしません。 - 音量の dB も比べるだけです。 対数の目盛りなので、二つ足しても音が二つ分にはなりません。
round half_evenは五つの丸めのうちの一つです。 同点を偶数側へ寄せる、会計でよく使われる向きです。