PCCやTALって何?

PCC (Proof Carrying Code) やTAL (Typed Assembly Language)というのは一 言で言うと、アセンブリ言語(又は機械語)に付加情報をつけてプログラムの 正しさを検証できるようにしたものです。従来は、プログラムの正しさの検証 は、ML での型検査に代表されるように、高級言語のソースプログラムレベル で行なわれるのが普通でした(し、今でもそれは行なわれています)。 ところが、最近になって、バイトコード(Javaなど)や機械語など低レベル言語での検証も 重要視されてきています。それには次のような理由が挙げられます。 そこで、登場したのが、PCCやTAL, Java のbytecode verifier というわけです。 PCC ではHoare 論理に似た体系を利用して、プログラムの提供者は、 機械語にそのプログラムがどのような性質を満たすかとその証明を付加し、 使用する側はその証明が正しいことを検査してからプログラムを実行します。 そうすると、例えば「レジスタr0 に格納されたアドレスにはアクセスしない」というような 性質を保証することができます。 TAL は、普通のアセンブリ言語に型情報を加えたもので、「レジスタr1 には整数が入っている」 とか「レジスタr2にはレジスタr1に整数を格納してjumpすべきアドレスが入っている」 というような性質を保証することができ、型つきなので、当然型検査が通ったアセンブリ プログラムを実行したらcore dump することはありません。 興味のある人は課題6を選んでみて下さい。

課題のリスト

koba@is.s.u-tokyo.ac.jp