操作的意味論

operational semantics

プログラムのある種の装置上での振る舞いを数学的に厳密に記述する

「コレが実行されたら、レジスタのここにこの値を追加して、」みたいなのを定義していく

プログラムの実行と、抽象機械の内部状態の対応付けとか

プログラムと、実行するVMの機械語にするコンパイラを定義するとか

対象のプログラムを解釈実行するインタプリタとか

完全に曖昧さを省いた言語の仕様のようなイメージ

一つの規則が変わるだけで、全体のプログラムの意味が変わってしまう

手続き型の言語と相性がいい？

機械の状態は項、機械の振る舞いは遷移関数で定義される

「項tの意味」はtを初期状態として動き始めた機械が到達する最終状態と考えられる

一つの言語に対して2つの操作的意味論を用いることもある

1. 一つはプログラマが書く項に似た機械状態を使う意味論

2. もう一つはその言語のインタプリタやコンパイラが操作する構造に近いもの

これらの異なる意味論で与えられた機械の振る舞いが、同じプログラムを実行したときに何らかの適切な意味で一致することが示せれば、言語の実装の正しさを証明したことに成る

例

2つの大別

参考