見出し画像

解けた！

りょうじ

５月１７日日曜日、晴れ

i を挟んで二つの部分ができること。このそれぞれが整列していることを不変条件としていた。だけれどもう一つ、 i を挟んだ前後の関係が必要だった。

ところでこれ、コードを見る限り配列 v の中身が保存されているように見える。しかし事後条件だけを意地悪くみると、例えば v の中身をすべて 0 で書き換えても成立する。

これを防ぐには事前条件は配列 v の 0 番目を除いて整列されていること、事後条件は配列 v 全体を整列したものであることを書けばよさそう。
Isabelle で「整列されていること」を示す述語は、まず間違いなくあるとおもう。これはどうやって探すのだろうかなあ？

＊　＊　＊

夕飯はナスの煮浸し、ポテトフライ、そして牛丼。

煮浸しと牛丼は『白ごはん.com』のレシピを利用。便利ですね、ここ。


この記事が気に入ったらサポートをしてみませんか？