
解けた!
5月17日日曜日、晴れ
やった!
— いけべ (@ikb) May 17, 2020
ついに「チャレンジ問題:バブルアップ」が証明できたっ!!
そうか〜、そこが足りなかったのか〜!
納得。 pic.twitter.com/YObjPJ2nyk
やった!
— いけべ (@ikb) May 17, 2020
ついに「チャレンジ問題:バブルアップ」が証明できたっ!!
そうか〜、そこが足りなかったのか〜!
納得。 pic.twitter.com/YObjPJ2nyk
i を挟んで二つの部分ができること。このそれぞれが整列していることを不変条件としていた。だけれどもう一つ、 i を挟んだ前後の関係が必要だった。
ところでこれ、コードを見る限り配列 v の中身が保存されているように見える。しかし事後条件だけを意地悪くみると、例えば v の中身をすべて 0 で書き換えても成立する。
これを防ぐには事前条件は配列 v の 0 番目を除いて整列されていること、事後条件は配列 v 全体を整列したものであることを書けばよさそう。
Isabelle で「整列されていること」を示す述語は、まず間違いなくあるとおもう。これはどうやって探すのだろうかなあ?
* * *
夕飯はナスの煮浸し、ポテトフライ、そして牛丼。
煮浸しと牛丼は『白ごはん.com』のレシピを利用。便利ですね、ここ。