Structural operational semantics

Presentation on theme: "Structural operational semantics"— Presentation transcript:

1 Structural operational semantics
Transition relation の形は、　　　　　　　　　　　　　　　　＜S, s＞ ⇒ r　と表す。　　　　　　　(1)rが＜S’, s’＞の形　　　　　　　　　　　状態sにおけるSの実行が終わらなかっ　　た。結果ではなく、中間の形。　　　　　　(2)rがs’の形　　　　　　　　　　　　　　　　　　　　　　状態sにおけるSは終了して、最終状態はs’。 rが存在しなければ、stuck(行き詰まった？)と　呼ぶ。

2 finite と infinite 状態sからステートメントSを実行したとき、derivation sequence は以下の２つのどちらかになる。　　　　　　　　　　　　　　　　　　　　(1) finiteなシーケンス　　　　　　　　　　　　　　r0, r1, r2, ‥ rk rkはterminalかstuck　　の形　　　　　　　　　　　　　　　　　　　　　　　(2)infiniteなシーケンス　　　　　　　　　　　　　r0, r1, r2, ‥

3 ステップ数の表し方 r0 ⇒i ri ‥ r0からriまで実行するのにiステップあることを示す。
r0 ⇒* ri ‥ r0からriまで実行するのに、有限回のステップがあることを示す。 上の２つは、derivation sequence でなくてもよい。riがterminal もしくは、stuckの形であればよい。

4 terminateとloop ＜S, s＞から始めて、有限のderivation sequenceになるとき、状態sにおけるステートメントSの実行はterminateするという。 ＜S, s＞から始めて、無限に続くderivation sequenceになるとき、状態sにおけるステートメントSの実行はloopするという。

5 定義 状態sにおけるステートメントSの実行は、＜S, s＞ ⇒* s’になるとき、成功した(terminate successfully)という。 また、Sがすべてのsにおいて終了するとき、Sはいつでも終了するという。 また、Sがすべてのsにおいてloopするとき、Sはいつでもloopするという。

6 Property of the semantics
Structural operational semantics では、derivation sequence の長さにおける帰納法で証明するのが好都合である。 実際証明するときは、この帰納法のステップは以下のどちらかを調べることでなされる。(1)syntaxの要素の構造　　　　　　　　　(2)derivation sequenceの最初の　　transitionの正当性を証明する導出木

7 Induvction on the Length of Derivation Sequence(derivation sequenceの長さにおける帰納法)
1, まず示したい性質が全ての長さが0のderiation sequenceにて成立することを示す。 2, 次に他の全てのderivation sequence にて成立することを示す。長さが最大でkの全てのderivation sequenceを満たすことを仮定する（induction hypothesis）。そして、長さがk+1のderivation sequenceでも成立することを示す。

8 定理２．１９ ＜S1; S2, s＞ ⇒k s”　ならば、　 ＜S1, s＞ ⇒k1 s’かつ＜S2, s’＞ ⇒k2 s”である。（ただしk = k1 + k2）　　　　　　　　　となるような状態sと自然数k1とk2が存在する。

9 deterministic テーブル2.2が、全てのS, s, r, r’において、＜S, s＞ ⇒ r かつ＜S, s＞ ⇒ r’ならば　r = r’であるとき、テーブル2.2はdeterministicであるという。

10