|
10
|
1 \begin{abstract_eng}
|
|
73
|
2 Checking desirable specifications of software are important.
|
|
|
3 If it checks actual implementations, much better.
|
|
|
4
|
|
|
5 In this papaer, We propose two verification methods using meta computations which save original implementations.
|
|
|
6 On the hand method verify specification by enumerate possible states on programs.
|
|
|
7 We checked red-black tree specification using our meta computation library named Akasha, which override program executions exhaustively.
|
|
|
8
|
|
|
9 On the other hand method veriy programs with proofs.
|
|
|
10 Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
|
|
|
11 We define the CbC type system with subtype for proving CbC itself.
|
|
82
|
12 Dependent-typed language Agda proves properties of translated CbC programs using proposed subtype definition.
|
|
10
|
13 \end{abstract_eng}
|
