解けず

５月８日金曜日、晴れ

昼は冷凍の坦々麺、夜は昨晩の肉豆腐の残りとバターチキンカレー。カレー粉があるとおもって油断していたところ、これが無く。ターメリック、コリアンダー、クミン、ガラムマサラを適当にまぜて味つけをしたけれど、これだという味が決まらずとても残念。
鳥もも肉は３時間、たっぷりのヨーグルトとスパイスでマリネしたんだけれどねえ。バターもしっかり入れたんだけれどねえ。残念。トマトの味が勝ちすぎたのか、はたまた。

＊　＊　＊

昨晩遅くまで働いたので、今日はだまし騙し流す感じで……　などという甘い考えはコードを前にして四散霧消。ガッツリ取り組む。

開発者オプションでアクティビティが裏に回ると同時に消えるというものが選べると知り、対策コードがうまく動いていることを確認する。

しかるに予想外のところでクラッシュ。見れば onCreate で API を非同期呼び出しし、その結果を受けて View を生成するという遅延コード。対して onActivityResult で（これよりはるか前に onDestroy まで行って新たに onCreate されているが遅延があるため）存在しない View に値を設定しようとしている。ああ、そりゃあダメだわ。

結局 Activity ひとつ、そのライフサイクルを叩き直すことになる。

夜までかかって、なんとか形にまとめる。各バージョンでの動作確認が終わらなかったので PR のレビューは来週にまわすことにして切り上げる。

＊　＊　＊

連休はいってすぐのセミナーでのチャレンジ課題。ループ不変条件を穴埋めした上で、自作のプログラム検証器にかけて正当性を確かめようというもの。

自作検証器までの道のりが遠すぎるのと、サンプル実装を動かす環境が手元にないこと。これを考えあわせて Isabelle で確かめたらよいだろうと対応を後回しにしていた。

腰を上げてチャレンジ。してみたけれど、とにかく難しい。

そもそも Isabelle は v[i] = v[i + 1]; 的な代入文を受け付けてくれない。これを乗り越えるために数時間が過ぎた。しかし、そのおかげで検証対象のコード内で「変更」（つまり代入）する対象の変数を VARS で宣言する必要があるともわかったし、添字での代入の代わりにリストの置き換えを使えばいいこともわかった。

v:= list_update v i v!(i+1);

こう書いてやればいい。あるいはこう。

v:= v[i:= v!(i+1)];

後者の記法のほうが教科書的で好ましいのだけれど、 Isabelle に言わせると２通りの解釈ができる曖昧さがあるとのことで無念。（型解釈的に正しいのは一方だけだから通してやるけれど、と恩着せがましい）

コードは移せたけれど。そして多分これ、というループ不変条件も書いてみたけれど、証明が通らない。難しい。