More than 5 years have passed since last update.
スタックコンパイラの証明
スタックコンパイラの証明
2014_04_30
RequireImportssreflectssrboolssrnatseqeqtypessrfun.算術式をスタック指向のプログラミング言語にコンパイルするコンパイラ（スタックコンパイラ）が正しく動作することの証明をする。証明は SSReflect を使っておこなう。
ソースコードは以下にあります。
https://github.com/suharahiromichi/coq/blob/master/ssr/ssr_stack_compiler.v
ソース言語（算術式）の定義
状態stateはプログラムの実行のある時点のすべての変数の現在値を表す。
Inductiveid:Type:=Idofnat.Definitionstate:=id->nat.ソース言語である算術式 aexp を定義する。
Inductiveaexp:Type:=|ANumofnat|AIdofid|APlusofaexp&aexp|AMinusofaexp&aexp|AMultofaexp&aexp.変数の略記法を以下に定義する。
DefinitionX:id:=Id0.DefinitionY:id:=Id1.DefinitionZ:id:=Id2.aexp を評価する関数を定義する。
Fixpointaeval(st:state)(e:aexp):nat:=matchewith|ANumn=>n|AIdX=>stX|APlusa1a2=>(aevalsta1)+(aevalsta2)|AMinusa1a2=>(aevalsta1)-(aevalsta2)|AMulta1a2=>(aevalsta1)*(aevalsta2)end.スタック指向のプログラミング言語（スタック言語）
スタック言語の命令セットsinstrは、以下の命令から構成される:
-
SPush n: 数nをスタックにプッシュする。 -
SLoad X: ストアから識別子Xに対応する値を読み込み、スタックにプッシュする。 -
SPlus: スタックの先頭の 2 つの数をポップし、それらを足して、結果をスタックにプッシュする。 -
SMinus: 上と同様。ただし引く。 -
SMult: 上と同様。ただし掛ける。
Inductivesinstr:Type:=|SPushofnat|SLoadofid|SPlus|SMinus|SMult.スタック言語のプログラムを評価するための関数を書く。
Fixpoints_exec(st:state)(ins:sinstr)(stack:seqnat):seqnat:=matchinswith|SPushn=>n::stack|SLoadidx=>(stidx)::stack|SPlus=>matchstackwith|b::a::stack'=>(a+b)::stack'|_=>stackend|SMinus=>matchstackwith|b::a::stack'=>(a-b)::stack'|_=>stackend|SMult=>matchstackwith|b::a::stack'=>(a*b)::stack'|_=>stackendend.補足：stack underflow の判定をまとめて前に出すと、証明がたいへんになるだろう。また、そのときの例外処理を行わないが、それによって、s_compile_correct_app の証明が簡単になっていると思う。
Fixpoints_execute(st:state)(stack:seqnat)(prog:seqsinstr):seqnat:=matchprogwith|[::]=>stack|ins::prog'=>s_executest(s_execstinsstack)prog'end.aexp をスタック言語の命令列にコンパイルする関数 s_compile を書く。
Fixpoints_compile(e:aexp):seqsinstr:=matchewith|ANumn=>[::SPushn]|AIdid=>[::SLoadid]|APlusab=>(s_compilea)++(s_compileb)++[::SPlus]|AMinusab=>(s_compilea)++(s_compileb)++[::SMinus]|AMultab=>(s_compilea)++(s_compileb)++[::SMult]end.コンパイルが正しいことの証明
以下で、s_compile 関数が正しく振る舞うことを述べる定理を証明する。
最初に補題として、スタック言語の命令列が append できることを証明する。
Lemmas_compile_correct_app:forall(st:state)(stack1stack2stack3:seqnat)(prog1prog2:seqsinstr),s_executeststack1prog1=stack2->s_executeststack2prog2=stack3->s_executeststack1(prog1++prog2)=stack3.Proof.move=>ststack1stack2stack3prog1.elim:prog1stack1stack2stack3.bymove=>stack1stack2stack3prog2;rewritecat0s;move=><-<-.move=>aprog1'IHprog1'stack1stack2stack3.elim:a;bymove=>?;applyIHprog1'with(stack2:=stack2).Qed.より一般的な、stackが任意の状態の場合について、
aexpをコンパイルしたスタック言語の命令列を実行した結果（左辺）と、
aexpを直接実行した結果（右辺）が一致することを証明する。
Lemmas_compile_correct_stack:forall(st:state)(stack:seqnat)(e:aexp),s_executeststack(s_compilee)=[::aevalste]++stack.Proof.move=>ststacke.elim:estack;(* 「stack」をpushするのが肝。 *)(* ANum, AId の場合 *)tryby[];(* APlus, AMinus, AMult の場合 *)trymove=>e1IHe1e2IHe2st0;applys_compile_correct_appwith(stack2:=aevalste1::st0);by[rewriteIHe1|applys_compile_correct_appwith(stack2:=aevalste2::aevalste1::st0);[rewrite(IHe2(aevalste1::st0))|]].Qed.最後に、stackが初期状態（空[]）の場合について、
aexpをコンパイルしたスタック言語の命令列を実行した結果（左辺）と、
aexpを直接実行した結果（右辺）が一致することを証明する。
Theorems_compile_correct:forall(st:state)(e:aexp),s_executest[::](s_compilee)=[::aevalste].Proof.move=>ste.applys_compile_correct_stack.Qed.Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme