2023/03/13
形式検証すごい
やったこと
- TIER IV Computing System Workshop 2023.03 を見た
- タイガーブック、型検査を書いた
- 本を読んだ
昼から TIER IV のワークショップを見てたけど、特に OS の知識が皆無だったから 8 割くらい内容が分からなかった。
形式検証の話は少しは掴めておもしろい内容だった。
そもそも形式検証を使った開発というのがあること自体知らなかった。
今のところの認識では、仕様を自然言語より厳密に定義できるが、結局は仕様 → 実装は人間が地道にやるしかなくてバグが含まれる可能性はもちろんある。
(形式手法の中の何かに分類される一部のことだと思うけど) 手順としてはオートマトンでシステムのモデル (Model) を記述してから、論理式で仕様 (Specification) を記述することで検証するらしい。
型推論があったりする強い型システムでは、型がモデルと同じ役割があって、例えば ML の型推論は数学的な裏付けがある (らしい) から、実際のプログラムを書いた時にモデルに反した式になっていないかが検証されていることを考えると形式手法と言えるのかな？
ここのへんの話、全然分からないけど、すごくおもしろそう。
構造や記述言語が異なるものの変換とその界面はバグの原因になる一方で、やりがいがあって楽しいと思う。
仕様 → プログラムもそうだけど、高級言語 → 機械語や DB → アプリケーション、クライアント → サーバなどもある。
抽象化してレイヤーに分けることは複雑なものを理解するために必要な思考なんだろうな。
タイガーブックには字句解析器・構文解析器・意味解析器でのエラーの扱いについての記述が少ないが、2023/03/04 の日報で引用したサイトに書いてある方法を参考にして実装することを前提に、以下のような戦略を現時点で考えている。
字句解析器：エラーがあれば例外を投げてプログラムが終了 (ここでのエラーは読み捨てるか置き換えるかの判断ができない)
構文解析器：修復できるエラーは修復 → エラーメッセージを出力して error ノードを生成、修復できなければ例外 (exception Parsing.Parse_error) を投げてプログラム終了
意味解析器：宣言でのエラーや error ノードは例外を投げてプログラム終了、それ以外の場所でのエラーや error ノードはエラー用の型を生成 (エラーの種類とエラーの内容を持つ)
意味解析から持ち越したエラーは、中間表現木のところで検査すると思っているけど、まだ内容が分からないから後になって意味解析フェーズでエラーは全てプログラムを止めるようにした方が良い可能性はある。
エラーを見つけた時点で例外を投げず、いくつかは次のフェーズに伝播させると一度のコンパイルで複数のエラーが報告できるが、特に型検査をする時の場合分けがとてもややこしくなることに気づいた。
思ったこと
TIER IV のワークショップを視聴して、自分が知らない領域とやりたいこと・知りたいことは無限にあると思った。 逆に自分のやってきたことや知っていることは、世の中にあるコンピュータサイエンスの知識とその土台となる哲学や数学、論理学などの蓄積された知識を前にすると、本当にちっぽけなんじゃないかとすら思えてくる。
今日の英会話
ウーパールーパーが絶滅の危機のため、保護団体に寄付をして食い止めようという話。 トカゲは黒っぽい色で尻尾が青っぽいイメージだったけど、国によってトカゲの種類が違うみたい。フィリピンだと水色の体に赤の斑点がある変なトカゲが野生でいて、トイレの壁とかによく出るらしい。