ループ構造の正しさを証明してやる！ [それはBooks]Code Readingを読んで、ループ性能(妥当性)に関しての議論を考えるときに、有効な手段があると書いてあった。「バリアント(variant)」と「インバリアント(invariant)」という概念を使う方法だ。「バリアント(variant)」とは、変わりやすいとか変更されるといった意味を持っている。 逆に「インバリアント(invariant)」は、変わらないとか不変なとかという意味を持っているらしい。 この「バリアント(variant)」と「インバリアント(invariant)」を使って、ループ構造が正しいかを証明する方法が、Code Readingの2章に載っていたので、忘れないうちに復習しておきたいと思います。 それにしても、Code Readingは面白いですね。技術者のツボをついた本だと思います。 概要と解説ループ処理の開始と終了の時点で共に成り立つ条件をループインバリアント
