実践プロパティベーステストをさっと読んでみた。
『実践プロパティベーステスト ― PropErとErlang/Elixirではじめよう』www.lambdanote.com
この感想を読んでみて、実際のテストのイメージがわかない（だけどテスト全般には興味がある）人は対象読者です。買いましょう。
最初の方を読んでの感想
結局流し読みになってしまったのですが、せっかくなので感想を書きます。
流し読みになった理由の一つはWindowsでのErlangの動かし方が分からなかった事。Eralng自体はインストールできたのだけど、最初に出てくるコマンドrebar3から見つからなくて諦めてしまった。もう一つは、意外にも知ってることが多かったから。
プロパティベーステストとは、特定の処理に対して絶対守られるルールをプロパティとして記述し、それに違反しないかどうかをテストする手法です。本書によると「どのような入力値を与えても常に同じであるような振る舞い」をコードとして書くとプロパティになります。ここだけ読むと、静的なテストのように感じますが中身はランダム検証です。
最初の方を読んだ感想。
「おつりの合計額は、常に払った金額から請求額を引いた額に等しくなる」というプロパティについて、intで表せるようなプロパティは普通にassert入れれば十分な気がする。Erlangもそうだけど、型に厳しい言語であればコンパイラの型チェック通った時点である程度のチェックは通ってる。少なくともお釣りの金額を期待するところで顧客名のリストが返ってくるようなことはない。そういうのも期待して型も設計しているはず。
もうちょっと抽象的なリストのソートみたいな奴はどうテストするんだろうと思って読んでいくと、同じ関数を別の人が実装すると書いてあって、この辺で半導体の検証手法を思い出しました。
半導体の検証手法
検証手法に関しては、半導体の検証はロジカルな部分だけでもお金が突っ込まれていて実践投入されてます。例えば、Fomalityといった静的検証ツールがあって、大元のソースコードの修正と、別のフェーズで入れるパッチを入れた結果が、論理的に等価ですよねみたいな静的なチェックをやってくれます。
SystemCとかSVA(SystemVerilog Assertion)等、本番の半導体で動く記述よりも抽象度の高い（開発効率が高い）記述で、同じ挙動を別々に書くこと＋ランダム検証で本書のプロパティチェックと同等の事が実施されています。ある条件を満たしてから、2CLK以内にこの状態にならないとエラーのような記述も普通に使います。これはステートに対するプロパティに相当します。ステートのassertionもand, orで簡単に組み合わせて複雑なシーケンスも記述可能になっています。
複雑なステートが入ってくるとそのプロパティが正しいのかどうかも問題になってきて、PCIとかUSB等の規格物については規格にあっているかどうかをチェックする専門家が作ったライブラリ（assertionの塊）が有償で売られてます。これも普通に使われていると思います。
本書でも取り上げられてますが、普通にランダム検証を使うと乱数が偏らないのでエッジケースをつきにくく、制約付きランダムで乱数を偏らせてエッジを狙ったり実動作に近づけたりします。例えばメモリアクセスに必要な時間を正確に見積もることができないので、アクセスのタイミングをランダムにしてシミュレーションするというのはどこでもやってると思います。
プログラマーのためのCPU入門 ― CPUは如何にしてソフトウェアを高速に実行するかwww.lambdanote.com
ラムダノートさんのプログラマーのためのCPU入門にを読むと、最近のCPUがどのタイミングでメモリにアクセスするかを事前に予測する難しさが分かります。
Encode->Decodeの対称プロパティは、僕が関係した画像系のプロジェクトでは非可逆の事が多く使えるケースは無かった気がします。
こう書くと半導体検証は恵まれているような気がしますが辛い話もいっぱいあります・・・
プロパティベースの検証に興味を持ったら、半導体の検証手法を調べてみると面白いです。普通に探すとデバイス（半導体そのもの）の検証やテストが出てくるので、Logic検証とかSystem検証で調べてみると良いです。
プロパティベースの使い道
本を読んでみて、C++で自分のプロジェクトに使えないかなと思ったところです。
Design Patternの実装のチェック
Strategyパターンのような複数の実装を同じように扱うようなライブラリを作ったとき、どの実装が来ても共通の振る舞いをプロパティにしたい。
移植ライブラリの等価チェック
今風の課題ですが、PyTorchの関数と同じ動きを関数をC++で作らないといけないとき、正解値をPyTorchで作って自作の関数を検証する。ただのランダム検証といわれたらそれまでか。
やはり、今の僕には文法や検証の概念よりは上手い使い方が知りたい。特に小さいプロジェクトでも、上手く使ってコスパ良い検証ができる手法を知りたいですね。
この後読みたいのは、n月刊ラムダノートの検証特集かな。大規模検証事例から個人プロジェクトまで。もしくは半導体で使われる検証手法（でソフトウェア設計にも応用が利きそうな物）の特集を、現役引退した半導体検証エンジニアの方々が書いてくれないかなと期待しています。
