仕様書がコードの後から書かれると、それは実装の説明になります。先に書かれ、別の場所で管理され、実装とは独立に実行できるのであれば、それは判定器になります。
ALSは後者を狙って、Almideの言語仕様を実装とは別のリポジトリに置いたものです。コンパイラは一行も入っていません。
中身
振る舞いの約束が301件あります。標準出力、標準エラー、終了コードを、すべての実行ターゲットで同一に定めたものです。加えて、ターゲットをまたぐ実行フィクスチャが591件、診断のケースが752件あります。診断のケースでは、壊れたコードが決まったコードとヒントで拒否されることと、直した版がコンパイルできることを両方確かめます。
構成としては、Ferroceneに対する仕様リポジトリ、seL4に対する検証リポジトリ、WASMエンジンに対する仕様と同じ位置づけになります。
要求が先に着地する
新しい振る舞いは、まず仕様側に入ります。仕様文を引用した契約と、それを宣言するフィクスチャを、仕様リポジトリへの一つの変更として出します。実装側は次に、そのタグを指して判定を通します。別にレビューされる二つ目の変更です。
二つのリポジトリの履歴が、要求がコードに先行したことの証拠になります。そして契約ごとに、それが実際に先行していたのか、同時だったのか、後追いだったのかを測って記録します。後追いの件数は、減る方向にしか動かせません。
基準線を、こっそり動かせないようにする
基準を緩める変更は、日付つきの理由を添えた独立した変更でなければ通りません。ある機能を通すために基準を下げたのであれば、その事実が別の記録として残ります。
レビューの記録も、対象となる文章のハッシュに結びつけてあります。一度レビューされた節の文言を書き換えると、その行は自動的に古い扱いになります。
判定は、走らせた範囲までしか広くない
適合性の検査は、仕様のコミット、バイナリの版、プラットフォーム、走らせた区分、件数、そしてすべての失敗を逐語で書いた報告を出力します。
一行、はっきり書かれている決まりがあります。判定は、その報告が「走らせた」と言っている範囲までしか広くありません。全部通ったという主張ではなく、どこを通したかという記述になります。
足りない部分も同じ場所に書く
仕様の意味を独立に確かめるため、依存ゼロの参照実装が別に置かれています。中核のコーパスは49件中49件を再現し、より広いコーパスでは比較できた172件のうち171件が実装と一致しました。残る429件は「この実装では判定を控える」として、152の分類つきで記録されています。
そしてREADMEには、Almideのソースに対する機械化された評価関係はまだ存在しない、と書かれています。何ができていないかを同じ場所に書いておくことが、判定器として信用されるための条件になります。
外部に開発を委託している場合
生成されたコードが通るかどうかを外から測るのが修正生存率で、生成されたコードが正しい意味で動くかを外から測るのがこちらです。
同じ構図は受託開発にも当てはまります。受け入れ条件が納品物の中にしかないと、それは実装の説明になります。発注側が持ち、実装とは独立に走らせられる形にしておくと、判定の材料になります。書く速さが上がるほど、この分離の価値が上がります。
