正当性の検証を意識してコードを書く

今日C言語でバッファのサイズを拡大するコードを書いていた。こんな感じの。

if (element_number(buffer) >=capacity(buffer)) {
  さらに大きいバッファの領域を確保する
}

しかし、別にこのコードは正しく動作するのだけどifではなくwhileで書いた方がいいのではと思った。なぜかというとwhileを使った方がプログラムの検証が簡単になるからだ。
プログラムの検証ではwhile文に関して次のような規則を用いる。

while (P) {
ここでは P は成り立つ
...
}
ここでは P は成り立たない(Pの否定が成り立つ)

while文を抜けたところでは条件式の式は(breakが中の文になければ)偽にになるわけだ。whileを知っている人にとっては当たり前の話だ。でも、こういう規則を使ってプログラムの正当性を検証しやすいようにコードを書いておくとバグが少なくなったり，構造がすっきりするのではないかと思った。

今回の場合ではwhileを抜けたところで

element_number(buffer) < capacity(buffer)

という条件がが成り立つようになる。element_numberやcapacityが正しく実装されているなら、バッファのサイズを拡張する処理にバグがあると無限ループになる。もしかしたら、デバッグがやりやすくなる効用もあるかもしれない。

プログラムの検証って講義を聞いていたときは正直あまり実用的でないと思ったけど、これを知っておくとプログラムの信頼性が上がる気がする。