たれぱんのびぼーろく

わたしの備忘録、生物学とプログラミングが多いかも

定義域と値域 in プログラミング

どうやって担保するか

f: X -> Y
関数fは入力/引数 x ∈ 定義域X を取り、出力/返り値 y ∈ 定義域Y を返す
関数fはcallerによって呼び出される.
引数を渡すのはcallerであるから、正しい引数xを渡す責務はcallerにある.
正しい引数を渡された関数は y ∈ Yを返す責務がある.
プログラムの検証をするなら、X -> Y (関数の内容、振る舞い) の検証 + 呼び出し時 x ∈ Xの検証 (関数の使われ方) が必要

ポイントは

  • 定義域と値域を担保できるか
  • 値域-定義域ミスマッチを実行前に担保できるか
function step1(arg:int) => int  
function step2(arg:int) => int & >0  
function step3(arg:int&>0) => int & >20  
function setp4(arg:int&>10) => int  

// pattern A
step1(1)  // int => int
|> step2  // int => >0
|> step3  // >0  => >20
|> step4  // >10 => int
// properly work  

// pattern B
step1(1)  // int => int
|> step2  // int => >0
|> step4  // >10 => int
|> step3  // >0  => >20
// 2to4 (e.g. output==5), 4to3 (e.g. output==-5) cause mismatch

patternBは、潜在的に異常な動作をしうるコード
動的な検証をしようとしたら、異常な動作を引き起こさなきゃいけない。異常な動作を引き起こす (おそらくエッジケースの) 引数がわかっていたら、最初から異常動作しないようにコード書く.

アサーション

あらゆる制約を書ける。なので定義域/値域の完全な担保が可能 (なはず).
Design by ContractのPre/Post conditionはこれにほぼ相当する.
おそらくエディタによる補完等は効かない。
pipeの安全性確保はこちら側ですることになる。

型システム

各引数に型がつくのであって、定義域の元 (引数のセット) には型がつかない (引数群をクラスにすればできなくはない)。
定義域の完全な担保は難しい
structural subtypingを採用しているものなら、pipeの安全性を確保できる。最高に魅力的
型でDbCを徹底したいなら、interfaceを実装したクラスを作ってConstruct内でValidationさせれば一応できる。かなりハイカロリー (クラスの用意、2関数に強く結合しているが故の変更コスト)なので、コア部分で使うのが妥当かな.

テスト

値域はある程度担保できるけど、定義域外が入ってくるのを防ぐ方法はない.

ドキュメンテーション運用

人間は不完全な生き物である、残念ながら。

目的

関数に定義域外の引数が入らないようにする. 関数が値域外の返り値を返さないようにする.
型定義ではじく。assertionではじく。どっちもそれ用のテストはあった方がbetter
型およびassertionが動くことが確約されれば、関数が定義域外をはじく能力が確約される。
その上で、プログラム内で関数が呼ばれる際に渡される引数が正しいとどうやって保証するのか。
定義域外の入力がくると、確約された能力によってType ErrorかAssertion Errorが発生しプログラムが停止する。だからプロダクション環境に入れる前に引数の正しさを保証する必要がある。
型を利用する場合は、引数の型を確認すればいいだけ。
Assertionを利用しようとした場合、「引数を生成した関数の返り値assertion条件 ⊂ 引数受け入れassertion条件」を目視 (あるいは自動検証) で確認しなければいけなくなる。あれ、目視あるいは自動検証って静的検査なのでは?もうほぼ静的型検査と変わらないのでは?
動的に検査するのであれば、引数生成関数にじゃんじゃかinputしてテストするしかない。さて2関数をまたぐテストケースはいくつどんなバリエーションで作ればいいのか…

検証方法

動的検証の場合、値に対する振る舞いを検査することになる.
具体的な値でなく変数の特性で検証すれば、関数呼び出しの正当性も検証できる.

動的な手法は具体的な値に関する何か (値の内容、値の型) を検査することになる?
定義域/値域は具体的な値というより変数の特性だから、型みたいな変数の特性を示すものでhandleしないと検証できない (総当たりが不可能なほとんどの場合で)

qiita.com

手法

アサーション/validation
静的型チェック 動的型チェック

Property-based testing