「全数検査」は検証ステップの時点で確定している値に限られる
値ベース検査の売りは「プログラムを完全評価してから、出てきた値を全数検査する」ことである。しかしこの「全数」性には時刻の指標が付く。検査されるのは、検証ステップの時点で値が確定しているものだけである。
「静的段階で確定する値」ではない。静的段階の内部でも、検証ステップより後に代入される値がある。
代入の時刻は二通りある
段階を跨ぐ値の篩所属は、最終的に誰も検査しない。検証はplanの早い段階で一度だけ走り、そのあとに二種類の代入が起きる。
- 上流stateの値は、plan時に代入される。ただし検証ステップの後である。
- リソース出力は、apply時に代入される。
どちらの代入点にも検証経路がなく、代入された値は検査器の視界に入らない。参照の宣言型検査が粗い型を通した場合(例えば宣言上はただのStringを、長さ・パターン付きの型が期待される場所へ渡した場合)、代入で解決された値が篩を満たすかを確かめる経路が存在しない。違反値はplanの表示に現れてさえ検査されず、最終判定はプロバイダAPIのエラーに委ねられる(carina#3448)。
なぜこの限定が重要か
値ベース検査の全域性は「値が手に入るなら検査できる」を保証するが、「検査の時点で値が手に入っている」ことは保証しない。この二つを混同すると、値ベース検査を採用しただけで全数検査が達成されたと読んでしまう。
実際に必要なのは、検査を一回のステップではなく値が到着した各時点に置くことである。篩の述語は値依存であり、値は代入されて初めて生まれるのだから、値が到着した時点で述語を走らせる以外にない。
根拠の確度
「全数」性の限定は探索中に二度精密化された。当初の「静的段階で確定する値」という言い方では、検証ステップより後にplan時代入される上流state値を取りこぼす。正しくは「検証ステップの時点で確定している値」である。