著者

坂口 和彦

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.7, no.5, pp.10-10, 2014-12-05

---

本発表では,スタック指向プログラミング言語PS0と定理証明支援系Coq上に実装したPS0の対話的プログラミング環境を紹介する.この対話的プログラミング環境では,ユーザはまず目的のプログラムがスタックの状態をどう変化させるかを表す形でプログラムの仕様を与え,次にプログラムの断片や証明を順番に与えていくことでプログラムを完成させる.このとき,記述するべき残りのプログラムの仕様は今までに入力したプログラムでどのような状態のスタックに遷移するかを表しているため,一般化されたスタックの状態を見ながらプログラムを記述できる.また,PS0のプログラムをPostScriptのプログラムに変換し,GhostScript等のPostScriptインタプリタの上で実行できることを確認した.We introduce a stack-oriented programming language PS0 and its interactive programming environment implemented in the Coq proof assistant. In this programming environment, first, a user writes the specification of a program as to how the program mutates the stack. Next, the user interactively fills unspecified part of the program. Finally, the user obtains the complete program that proved satisfying the specification. At each step, the environment shows the specification of the program that we should fill. The specification describes the property of the initial and final state of the stacks. Therefore, we can write the program with the generalized state of the stack given. We also implemented a translator from PS0 programs to PostScript programs. It was confirmed that PostScript programs generated by the translator can be executed on PostScript interpreters (e.g., Ghostscript) properly.