最近の検索
検索オプション
https://qiitadon.com/@momosetkn/104076507886887815
Coq で停止性証明の付いたプログラムを書けってことですよ (超適当)
qiitadon.com半額の人 (@momosetkn@qiitadon.com)
冗談はさておき、ループ書くとき事前条件と不変条件と事後条件を列挙して assert とかで確認しておけば、よほどアホなことしない限り確認はできる
もっと言うと、無限ループは大抵の場合そこまで致命的なバグではなくて、本当に全力で防ぐべきなのは dangling pointer とか arithmetic overflow からの UB とかそういうところなんですよ
瑣末なことに捉われている場合ではない