|
2
|
1 \chapter{継続を中心としたプログラミングスタイル}
|
|
|
2
|
|
|
3 コンピューター上では様々なアプリケーションが常時動作している。
|
|
|
4 動作しているアプリケーションは信頼性が保証されていてほしい。
|
|
|
5 信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。
|
|
|
6 アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。
|
|
|
7
|
|
|
8 アプリケーションは通常特定のプログラミング言語で実装されている。
|
|
|
9 このプログラミング言語自身の信頼性は高く保証される必要がある。
|
|
|
10 また、実際にアプリケーションを動作させるOSも高い信頼性が保証される必要がある。
|
|
|
11 OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。
|
|
|
12
|
|
|
13
|
|
|
14 OSの信頼性の保証もテストコードを用いて証明することも可能ではあるが、 アプリケーションと比較するとOSのコード量、 処理の量は膨大である。
|
|
|
15 またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。
|
|
|
16 テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。
|
|
|
17 実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。
|
|
|
18 非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。
|
|
|
19
|
|
15
|
20
|
|
2
|
21 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
|
|
|
22 形式手法の具体的な検証方法の中で、 証明を用いる方法とモデル検査を用いる方法がある。
|
|
|
23 証明を用いる方法ではAgdaやCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
|
|
15
|
24 Curry-Howard同型対応則により、型と論理式の命題が対応する。
|
|
|
25 この型を導出するプログラムと実際の証明が対応する。
|
|
|
26 特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
|
|
|
27 証明そのものは記述した関数の内容の整合性を、定理証明支援系が検証する。
|
|
|
28 証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。
|
|
|
29 AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。
|
|
|
30 しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。
|
|
|
31 Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。
|
|
|
32 検証ができているソースコードそのものを使ってOSを動作させたい。
|
|
|
33
|
|
|
34
|
|
|
35 他の形式手法にモデル検査がある。
|
|
|
36 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。
|
|
|
37 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
|
|
|
38 実装するコードに対してモデル検査を行いたいが、モデル検査を行うモデル検査器は限られている。
|
|
|
39 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
|
