数理解析研究所講究録 1325 巻 2003 年 104-109

104

再帰型をもつオブジェクト指向計算モデルにおける例外処理の型付
堀江 美保子

酒井 正彦

坂部 俊樹

名古屋大学工学研究科〒 464-8603 名古屋市千種区不老町
mihoko@sakabe.nuie.nagoya-u.ac.jp {sakai,sakabe}@nuie.nagoya-u.ac.jp

Typing Exception in an Object Oriented Calculus
with Recursive Types
Mihoko HORIE Masahiko SAKAI Toshiki SAKABE
Graduate School of Engneering,Nagoya University
Furo-cho,Chikusa-ku,Nagoya,Japan,464-8603
概要

object calculus[1] はオブジェクト指向計算モデルであるが, 多くのプログラミング言語が持つ例外処理機能を表現することができない. そこで著者らはこれまでに object calculus のもつともシンプルなモデ
ルである$\mathrm{o}\mathrm{b}_{1<:}$を拡張し例外処理機能を追加するとともに操作意味論と型システムを与え, 型システムを拡張し再帰を扱えるようにしが操作意味論に対して健全であることを証明した [9]. 本稿では ,たに例外処理機能を追加し, 操作意味論と型システムを与え, 型システムが操作意味論に対しのプログラムの各部分で発生する例外のて健全であることを証明する. この型システムにより,型を静的に検査できる. キーワード
object calculus, オブジエクト指向言語, 例外処理, 型システム$\mathrm{O}\mathrm{b}_{1<:}$$\mathrm{O}\mathrm{b}_{1<:\mu}$$\mathrm{O}\mathrm{b}_{1<:\mu}$1

イプ判定式の決定可能性を示す. これによって, 計

はじめに

オブジェクト指向計算を形式化した object calculus [1] には, シンプノレなものから複雑なものまでいろいろな種類のがあり, Java などのオブジエクト

指向言語の多くの機能を表現することができる. しかし, 計算の途中で例外が発生したときに, 計算を止めて例外処理に移るような例外処理機能は表現で算結果が決定できることが保証される. 型システムの拡張で, 型は通常型と起こりうる例外の型を列挙

した例外型の組だと考える.

2object calculus
外処理機能の追加$\mathrm{O}\mathrm{b}_{<:1\mu}$

きない.

object calculus$\mathrm{O}\mathrm{b}_{<:1\mu}$への例に処理する例外を例外の

本稿では, object calculus の中で, 再帰型をもち型によって指定できる例外処理の機能を加えて拡張に, 例外を発生させるをと表記すする. この拡張した Ob ゆる. 拡張した部分には☆印を, 改良した部分には\star

簡単なモデルである$\mathrm{O}\mathrm{b}_{<:1\mu}$

throw 構文と, 処理する例外を型によって指定でき
る try catch 構文を追加し例外処理の機能を組み入$1\mu$$\mathrm{O}\mathrm{b}_{<:1\mu\langle\rangle}$

印を表記する.

れる. 構文の追加に伴い操作意味論, 型システムの2.1

拡張も行い, 型システムが操作意味論に対して健全-calculus の項は, 変数, オブジエクト, メ
ソッド実行, メソッド更新, fold, unfold からな
は,る (表 1). オブジエクトであることの証明を行う. この型システムで推論が完或すれば, どんな例外が発生するか実行前に知ることができる.

操作意味論の拡張では, 例外の型のサブタイプ関係を調べて処理するかどうか判断するため, サブタ$\mathrm{O}\mathrm{b}_{<:1\mu\langle\rangle}$の構文$\mathrm{O}\mathrm{b}_{<:1\mu}$$[1: =\sigma(x_{i} :$l_{\mathrm{i}}$がメソッド名,$b_{i}$

A_{i})b_{i}^{i\in 1..n}]$がメソツド本体,$\sigma(x_{i} :A_{i})$

はメの型がソッド本体に現れる変数 が self 変数,
であることを表す. fold ?よ再帰をするためにオ$x_{i}$$A_{i}$$x_{i}$

105 105
ブジェクトに再帰型を関連づける. また unfold は

fold されたオブジェクトから元のオブジェクトを取り出すものである. これに例外を発生と捕捉を表す
2 つの構文を追加する.

.
.

U)$

型 $U$ の項を例外として発生させる.

$[l_{i} :\sigma(x_{i} :通常の結果

A_{i})b_{i}^{i\in 1..n}]$

通常の結果$(U, v)$throw $(u : U)$catch(x : $U$ )項 を実行中に型 $U$ のサブタイプの例外が発生した場合, それを変数 に束縛して項 を

try

結果

$v::=$

fold$thr\sigma w(a :$a$

表 2: 操作意味論の記法 (結果の項)

例外発生する結果☆
ただし,は通常の結果.
$u$

$b$

$a$

$a$

$b$

$x$

(Red Throwl) ☆

実行する.
$\frac{\vdash a\sim u}{\vdash thr\alpha v(a\cdot U)\sim\nu thr\sigma w(u\cdot U)}.$.

本稿の例外処理では, 型によって例外を捕捉するかどうか判断する. try の中で発生した例外が指定された型のサブタイプならば, 処理を行うがそうでな

where $u\in$ {$a$

ければそのまま例外は発生したままである. 型の構

( :
の時,

$[l_{i}=\sigma$

の結果が

$u$

$x_{i}$$A_{\dot{\iota}}$)fold(U, $u)$ }$(a : U)$ の結果は,$b_{1}.:\in 1..n],$$thr\alpha w$

throw(u: $U$ ) なる. これは, 例外オブジエクトの結果として例外が発生していることを表す.

文は表 3 のように定められる. (2.3 節で詳しく述べる. )(Red ThrOw2) ☆

表 1: 項の構文.

$\frac{\vdash a\sim throw(u.U)}{\vdash throw(a.U)\sim throw(u.U)}.’.$$a,$$b::=$

項

変数$x$$[l_{i}=\sigma(x_{i} :オブジェクトA_{i})b_{i}^{i\in 1..n}]$$a.l$

メソッド実行$a.l_{-}^{arrow}\sigma(x:A)b$

メソッド更新すでに例外が発生しているので, その例外の結$(l_{i}\mathrm{B}|\rfloor)$fold $(U, a)$recursive foldun old(a)recursive unfold
例外発生☆
throw $(a:U)$
例外捕捉☆
try catch(x: )果 $thr\sigma w(u : U)$ をそのまま $thr\sigma w(a : U’)$ の

結果する.

(Red

$\vdash a\sim$

$f$

$U$

$a$

$\mathrm{T}1\mathrm{y}\mathfrak{y}$☆

throw(u : $U$ ) $\vdash b\{u\}’\cdot v$ $\vdash U<:U’$a catch(x : $U’$ ) $b\sim v$$\vdash try$

例外が発生し, 例外処理を行う場合である.

$b$

$a$

の結果が例外オブジェクトの結果 $thr\sigma w(u$ :

8121

$e$

$U)$

を温 $U()$ の recursive fold で表される式

fold(U, brint$\sigma(x_{2} :$=\sigma$A)thrm(e :(:$x_{1}$

U)]$

,

$e’$

$U)unfold(x_{3}).print$ とする.

$x_{1}]$

より型 $U$ の例外 が発生する. この例外 は, oetch$e$の後ろで変数$x_{3}$$e$$\mathrm{O}\mathrm{b}_{<:1\mu\langle)}$$a$に束縛され, unfold(e).print が実計算結果の項を表 2 のように定める.
操作意味論は, 項を結果に関連づける判定式: $a\sim$を推論するための規則で与えられる. 例外処理機
能を表現するために,に対して, 以下の推論規則を追加する.

$v$$\mathrm{O}\mathrm{b}_{<:1\mu}$

$b$

$b$

$\vdash a\sim*throw(u :$\vdash try$の操作意味論のサブタイプであるとき,
$U’$

$v$

(Red Try2) ☆

行される.

22

$U’$

則の中に含まれているのでこの決定可能性を
2.4 節で示す.

このとき $e’$ を実行すると, メソット呼出の式 $a.l$ の実行で throw $(e:U)$ にが$U$

catch(x :) の結果は の結果 とする. サブタイプ判定式 $\vdash U<:U’$ が評価規

try) ), $a\text{を式}[l=$を式 try $a.lcatch(x_{3}$ :$U’\{\rangle$

で

.

U)$

$\psi U<:U’$a catch(x : $U’$ ) $b\sim thrcnn(u : U)$

例外が発生しても, 例外処理を行わない場合で
ある. 項

$a$

thrm(u:ないとき,の結果が例外オプジエクトの結果

$U$

$a$

) で型 $U$ が型 $U’$ のサブタイプでの結果 thrm(u: $U$ ) がそのまま

catch(x : $U’$ ) の結果である. サブタイ
プ判定式 $\mu U<:U’$ が評価規則の中に含まれているのでこの決定可能性を 2.4 節で示す.

try

$a$

$b$

106
である. 項(Red Try3) ☆

a catch(x : $U’$ )$A_{i}$$x_{i}$$b_{i}^{i\in 1..n}]$

$a$

$b$

$a$

.

$\frac{\vdash a\prime\cdot thr\sigma w(u.U)}{\vdash a.l_{j}\sim thr\sigma w(u.U)}.$

メソッド実行の中の
ある.
$U)$

$a$

$a$

$Ue)$ であること $(a:U(Ue\rangle$

れかであることを意味する. 例外の型は,
しくは,

$a$

$u$

$U\langle$と例外が発生するとすればその型は $Ue$ 中の型のいず$b\sim\rangle v$, fold(U, $u)$ }where $v\in$ {( : )例外が発生しない場合である. 項 の結果がの結果
通常のオブジェクトの結果であれば,を try oetch(x: $U’$ ) の結果とする.
(Red Select2) ☆
$[l_{i}=\sigma$の型書く) は, 例外が発生していなければ $U$ の型であり,$\vdash a\sim v$$\vdash try$$a$で例外が発生した場合での例外オブジェクトの結果 throw(u:を a.lj の結果とする.

$\epsilon$$U_{m}$$U_{1},$ $U_{2},$$\ldots,$

$Ue$

, も

というリストで表す. または, 必ず例外が発生し, 通常の型がないことを表す. 型の構文を表 3 のように定める. オブジェクト
がメソッド
がメソッド名,型
は,$[l_{i} :A_{i}^{i\in 1..n}]$$A_{i}$$l_{i}$の返り値の型を表す. 再帰型 $\mu(X)U\{X\}$ は, 再帰を行う際 $U\{X\}$ を $X$ に束縛することを表す. 再帰
型を $\mu(X)A$ とせず $\mu(X)U$ としたのは, 例外まで束縛して再帰しなくても十分であると考えたこと,ならび, 計算モデルをなるべく簡単にしたかったことによる.

(Red Update2) ☆

.

$\frac{\vdash a\sim>throw(u.U)}{\vdash a.l_{j}-arrow\sigma(x\cdot A)b\sim throw(u.U)}.\cdot$

メソッド更新の中の
ある.
$U)$

$a$

$a$

で例外が発生した場合での例外オブジェクトの結果 throw(u :を $a.l_{j}\Leftarrow\sigma(x:A)b$ の結果とする.

(Red FOld2) ☆
throw(u : $U’$ )old(U, )throw $(u : U’)$$\vdash a$$\vdash f$

へ$\sim$$a$

再帰を含む fold の で例外が発生した場合である. 再帰を抜け出し,の例外オブジェクト$a$$a$の結果 throw(u:$U’$) を fold(U, ) の結果と$a$する.
(Red UnfOld2) ☆

$\vdash un$

unfold の$a$型システムは次の 4 つの判定式の型推論規則に..
..

よって構或される.

throw(u : $U$ )fold(a) ’. thrcrw(u : $U$ )$\vdash a$へ

で例外が発生した場合である.

$a$の例外オブジェクトの結果 throw $(u :U)$ を
unfold(a) の結果とする.

◇
Well-formed environment 判定式:
$E\vdashA$
判定式:
Well-formed type
Subtyping 判定式: $E\vdash A<:B,$ $E\vdash U<:V$
Term typing 判定式: $E\vdash a:A$
$E\vdash$

例 22 例 2.1 の式 $e’$ をが次のようになることがこ

追加した型の操作意味論で判定できる.

$A<:B,$ $E\vdash U<:V$ の規則を次のように定義する.

$\vdash trya.l$catch$(x_{3} :$\mathrm{O}\mathrm{b}_{<:1\mu\{)}$$\mathrm{O}\mathrm{b}<:1\mu$$\mathrm{a}$$int=\sigma(x_{1}$:$U’(\rangle)x_{1}]$の型システムにおける型は通常型と呼び,$\mathrm{O}\mathrm{b}_{<:1\mu\langle\rangle}$$\epsilon$

について判定式 $E\vdash A,$$E\vdash$(Type Excep) ☆
$\frac{E\vdash UE\vdash V\forall j\in 1..m}{E\vdash U(V_{j}^{j\in 1..m}\rangle}$$U,$ $V$と表記$U\langle V^{j\in 1..m}j\rangle$

する.

),

U)unfold(x_{3}).print$へ

2.3$U\langle Ue$の型は, 通常型と例外聖の組 $U(Ue\rangle$

で定義する. ここに, 例外型 $Ue$ は, 通常型のリストを構或するすべての型が Wellも Well-formed でformed ならば,ある.

$U\langle V^{\mathrm{j}\in 1..m}j\rangle$

107 107(Val Object)(Sub Excep) ☆
$E\vdash U\langle V_{l}^{i\in 1..m})E\vdash U’\langle V_{j}^{\prime j\in 1..n}\rangle\forall i\in 1..m$$\star$$. \frac{E,x_{i}\cdot U\langle\rangle\vdash b_{i}\cdot B_{i}\forall i\in 1..n}{E\vdash[l_{i}=\sigma(x_{i}.U\langle\rangle)b_{i}^{i\in 1n}]\cdot U(\rangle}.\cdot..$.

$k_{i}\in 1..n$$E\vdash U<:U’E\vdash V_{i}<:V_{k_{i}}’$where$E\vdash U\langle V_{i}^{i\in 1..m}\rangle<:U’\langle V_{j}^{\prime j\in 1..n})$型$U(V_{i}^{i\in 1..n}’\rangle$

が, 型$U’\langle V_{j^{j\in 1..n}}’\rangle$のサブタイプであるということは, 型 $U$ が $U’$ のサブタイプであり,$V_{\mathrm{j}}^{\prime j\in 1..n}$$V_{i}^{i\in 1..m}$のそれぞれについて,のどれか一つのサブタイプになっていることである. 例外の型では, サブタイプで発Select) , (Val Update)
規則の変更を行う.
($\star$例 23 例 2.1 において,$\triangle$$U’=$

bwint:$U$$\star$$U=\triangle$] としたとき,$U\equiv[l_{i} :$e’$についても同様に\mu (X 冷\pi int: $X$ ],の型は $U$ ( になる$\rangle$

ことが聖システムで判定できる. このことは式 $e’$ の生する例外は, スーパータイプでも発生できる

例外が外部に波及しないことを意味する.

ことを意味する.

2.4

次に ,

構文について項の型付け判定
式 $E\vdash a:A$ の規則を追加する.

サブタイプ判定式:E\vdash U $<:V$ の決
定可能性$\mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w},\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{c}\mathrm{h}$(Val Throw) ☆

B_{i^{i\in 1..n}}]$操作意味論 (2.2 節) の推論規則 (Red Tryl), (Red
Try2) において $\vdash U<:V,$ }$fU<:V$ が評価規則に含まれている. そこで環境 $E$ が空のときの$U<:V$ の決定可能性を示す. $\phi\vdash U<:V$ が決定$\phi\vdash$$\frac{E\vdash a.U\langle Ue)}{E\vdash throw(a\cdot U).\epsilon(U,Ue\rangle}..\cdot$

throw(a: $U$ ) は, 必ず例外を発生するので通常の型は空という意味で となる. で例外が発生していなければ, throw(a: $U$ ) は, 型 $U$の例外を発生させ,となる. 例外が発生していれば, それが伝わるので,の例外の型
を throw $(a : U)$ の例外の型に加える.
Try) ☆
$a$$\epsilon$$\epsilon\langle U\rangle$$a$($\mathrm{V}\mathrm{a}1$

可能性であることは, その否定の $\phi\psi U<:V$ が決定可能であることを含意する.
$\phi\vdash U<:V$ の決定可能性を示すためにイプであることを判定する項書換え系$E\vdash try$:a catch(x: $U’$ )$b$とにより, 定理 23 を得た.

補題 21 $U,$ $V$ を型とし, それらをコード化した項

$b$

$a$

$b$

$a$

$b$

$a$

使うことは,$a$との値を同じように扱うこと$b$である. そこで try
型は ,

$a$

と

$b$

$a$

catch(x : $U’$ ) の通常の$b$の共通な型 $U$ とする.

その他 (Type ), (Sub ) の規則を定義し, 例外の$\epsilon$$\epsilon$型を外側に伝えるために以下の規則の変更を行う.
($\mathrm{V}\mathrm{a}1$

Fold)とする. このとき,サブタイプ判定式 $\phi\vdash U<:V$ が推論可能

iff

で true に到達可能.
subtype?(u, ) が
ステップ数に関する帰納法により証明される.
$R_{\epsilon t}$$(\Leftarrow)$

または が実行さ
oetch(x : $U’$ ) は,れるものである. try catch(x : $U’$ ) の値を

try

$v$

$v$

$U\langle V_{j}^{j\in\{k|k\in 1..m,E\vdash V_{k}\wedge:U’\}}, Ve’\rangle$

を作或

し, 付録に示す. そして以下の 2 つの補題を示すこを $u,$$\underline{E\vdash a.\cdot U(V^{j\in 1..m}\mathrm{j})E,x.\cdot U’\vdash b\cdot.U(Ve’\rangle}$, サブタ$R_{\epsilon t}$$\star$.

$\frac{E\vdash b.U\{A\}(Ve\rangle}{E\vdash fold(A,b).A}.$

where $A\equiv\mu(X)U\{X\}\langle Ve\rangle$(Val Unfold)$\star$$(\Rightarrow)$

導出木の深さに関する帰納法により証明される.

口

補題 22 サブタイプ判定項書換え系が停止性を持つ.

辞書式経路順序により証明される.

口

定理 23 $\phi\vdash U<:V$ は, 決定可能である.
補題 2.1, B. による.

口$B$

項書換え系の停止性証明ツールを利用することにより, 補題 22 の証明を簡単に行うことができた. 項

書換え系を使わなくてもサブタイプ判定式の導出木
に対して, 葉に向かつて判定式のサイズが小さくな
るかまたは 2 つの型がサブタイプとして近づくことを用いて, 決定可能性は証明できると考えられる.
$\frac{E\vdash a.A}{E\vdash unfold(a).U\{A\mathrm{B}(Ve\rangle}.\cdot$

where $A\equiv\mu(X)U\{X\}\{Ve\rangle$

しかしながら, 項書換え系へのコーデイングにより証明を容易にすることができた.

108
25

型システムに対する操作意味論の健
全性

表 4: 例外処理機構の比較
木稿$\mathrm{O}\mathrm{b}_{1<:\mu(\rangle}$,$\frac{\mathrm{C}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{o}\mathrm{n}\mathrm{L}\mathrm{i}\mathrm{s}\mathrm{p}}{(throwu,b)}$$\mathrm{O}\mathrm{b}_{<:1\mu\langle)}$throw $(a : U)$
try catch(x:において, 次の補題が成り立つ.

$a$

補題 2.4$E,$ $X<:U,$ $E’\vdash\Im,$ $E\vdash U’<:U$$E,X<:U’,E’\vdash\triangleright s$

:

$E,x$

.

.

ならば,

$E,x$

の構造に関する帰納法で証明される.

$\Im$

:

ならば,

$E,$ $x$$E,$ $E’\mathrm{f}U’$}$\vdash\Im\{U\}$.

$\Im\{d\}$

$)$

throw
try a $catch(U_{1}x_{1})b_{1}..catch(U_{n}x_{n})b_{n}$catch $(u, a)$l よタグ変数.

を記述した形での定式化を行った. また Java では,
Throwable のサブクラスの値を例外として発生させ$U$

口るが*Oblでは投げられる例外値の型に制限はのない. Java の try catch... catch は,

これらの補題を利用して, 次の定理が成り立つ.

定理 $2.6\vdash a\sim v$ のとき,
$v$

:

$C$

$?u.a$$E’\vdash$の構造に関する帰納法で証明される.

$s^{\triangleright}\{x\}$

Java

$u$

: $U$ , $E’\vdash\Im\{x\}E\vdash d$ : $U()$ ならば, $E,$$\langle$$(catch\prime u, a)$$b$

口

補題 25 $E,$ $X<:U,$ $E’\{X\}\vdash\Im\{X\},$ $E\vdash U’<$ :
$U$

)

$a$

$U\langle\rangle,E’\vdash\Im,E\vdash U’<:U$$U’(\rangle,E’\vdash\Im$

ならば,

$U$

$\phi\vdash a:C$ならば,$\mathrm{O}\mathrm{b}_{1<:\mu\langle)}$$\phi\vdash$

try oetch をネストすることで表現することができる
が, try-catch-finmlly は, 残念ながら.

判定式 $\vdash a\sim*v$ の証明木の深さに関する帰納法によって証明される.

$<:\mu\langle$ $)$口$\mathrm{O}\mathrm{b}_{1<:\mu(\rangle}$で管理して捕捉している.

である力 , もしくはサブタイプの型になることがわ

4

かる.

では

に逐次
表現することはできない. ただし,実行の機能を追加すれば表現可能である. Common
Lisp, SML, [4], [5] は例外を例外名あるいはタグ

この定理から, 計算結果の型は計算する前と同じ$\mathrm{a}$$\mathrm{O}\mathrm{b}_{1<:\mu(\rangle}$

まとめを拡張して, 例外処理機
object calculus
を形式化し, 構文, 型システ
能を追加したム, 操作意味論を与えた. 操作意味論の評価規則に含まれているサブタイプ判定式に対して, その決定$\mathrm{O}\mathrm{b}_{<:1\mu}$

3

関連研究

$\mathrm{O}\mathrm{b}_{<:1\mu()}$

本稿は Java の例外処理を基に , オプジエクト指向計算モデル上で例外処理機能のモデル化を行った.
例外処理機能については, 多くの研究がなされている [2],[3], $[4],[5],[8]$ . Java, Nakano[5], Kameyama
and SatO[4], Common Lisp における例外処理機構の構文を表 4 にまとめる.
本稿と Java はサブタイプ関係を用いて例外捕捉することは, 同じである. しかし, 本稿では throwに対し型情報 $U$ を記述しなければならないのに対して, Java ではその必要はない. 型情報をはずし型の型推推論を行うことが考えられるが,論アルゴリズムはまだ与えられていない. ただし,$\mathrm{O}\mathrm{b}_{1<:\mu\langle\rangle}$の型推論アルゴリズムはすでに与えられている [6]. また,は簡単な Object calculus$\mathrm{O}\mathrm{b}_{1<:\mu}$

可能性を示した. また, 操作意味論の型に関する健全性の証明を行った. さらに複雑な object calculus
への例外処理機能の追加は今後の課題である.

謝辞
本研究を進めるに際して, 熱心にご討論頂いた坂部研の皆様に感謝致します. 本研究は一部, 日本学術振興会科学研究基盤 $(\mathrm{C})11680352$ , 柏森情報科学振興財団の補助を受けています.

参考文献
[1]

$\mathrm{A}\mathrm{b}\mathrm{a}\mathrm{d}\mathrm{i},\mathrm{M}.$,$\mathrm{C}\mathrm{a}\mathrm{r}\mathrm{d}\mathrm{e}\mathrm{l}\mathrm{l}\mathrm{i},\mathrm{L}$. : A THEORY OF OB-JECTS, Springer, 1998.

$\mathrm{O}\mathrm{b}_{1<:\mu\langle\}}$に例外処理機能を追加したものであるが, 複雑な完全であるこObject calculus では, 型推論がともすでに示されている [7]. このことから, 型情報$\mathrm{N}\mathrm{P}$[2]$\mathrm{D}\mathrm{r}\mathrm{o}\mathrm{s}\mathrm{s}\mathrm{o}\mathrm{p}\mathrm{o}\mathrm{u}\mathrm{l}\mathrm{o}\mathrm{u},\mathrm{S},$$\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{k}\mathrm{e}\mathrm{v}\mathrm{y}\mathrm{c}\mathrm{h},\mathrm{T}$:Java

ceptions Throw no Surprises

Ex-$\mathrm{h}\mathrm{t}\mathrm{t}\mathrm{p}://\mathrm{W}\mathrm{W}\mathrm{W}^{}$

108 109doc[3]$.\mathrm{i}\mathrm{c}.\mathrm{u}\mathrm{k}/\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{j}\mathrm{e}\mathrm{c}\mathrm{t}/\mathrm{s}\mathrm{l}\mathrm{u}\mathrm{r}\mathrm{p}/,2000$$\mathrm{J}\mathrm{a}\mathrm{c}\mathrm{o}\mathrm{b}\mathrm{s},\mathrm{B}$.

: AFormalization of Java’s Ex-.

ception Machanism, ESOP2001, LNCS2028,
2001,$\mathrm{P}\mathrm{P}$.284-301.

[4] Kameyama,Y.,. : Non-deterministic

Calculi, Theoretical Computer
Science, Vol. 272, 2002, pp. 223-245.

$\mathrm{C}\mathrm{a}\mathrm{t}\mathrm{c}\mathrm{h}/\mathrm{T}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}$[5]$\mathrm{N}\mathrm{a}\mathrm{k}\mathrm{a}\mathrm{n}\mathrm{o},\mathrm{H}$// sub$arrow$. : Logical Structure of the Catch andThrow Mechanism,, ph.D thesis, Universityof Tpkyo, 1995.

same?

(

$\mathrm{P}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{b}\mathrm{e}\mathrm{r}\mathrm{g},\mathrm{J}$. : Efficient

Inference of Object
Computation,
andTyPes, Infomation
Vol. 123, No. 2,
1994, pp. 198-209.

$\mathrm{O}\mathrm{B}$(CONS$(\mathrm{f}\mathrm{s}1$$\mathrm{O}\mathrm{B}(\mathrm{x}),$fssl)),’

and$(\mathrm{f}\mathrm{s}\mathrm{l},\mathrm{f}\mathrm{s}2)$$\mathrm{O}\mathrm{B}$$\mathrm{O}\mathrm{E}$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}^{7}$(NIL))(CONS($\mathrm{O}\mathrm{B}$$(\mathrm{f}\mathrm{s}2$, fss2)))(fssl),$\mathrm{O}\mathrm{B}$(fss2))

true$arrow$$//\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{R}\mathrm{e}\mathrm{c}$subtype?

$(\mathrm{M}\mathrm{U}(\mathrm{X}.\mathrm{n}\mathrm{t}1).\mathrm{N}\mathrm{U}(\mathrm{Y}.\mathrm{n}\mathrm{t}2))$$arrow \mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+(\mathrm{n}\mathrm{t}\mathrm{l} \prime \mathrm{n}\mathrm{t}2)$

このノレーノレを呼ぶたびに subtype?
を追力 兇靴を作る。

$\star$$(\mathrm{N}\mathrm{T}1,\mathrm{N}\mathrm{T}2)$

ノレに$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+?(\mathrm{X},\mathrm{Y})arrow \mathrm{t}\mathrm{u}\mathrm{r}\mathrm{e}$の) レー$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}y\mathrm{p}\mathrm{e}+$?

//例$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}y\mathrm{p}\mathrm{e}+?(\mathrm{X},Y)arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+7$[6]$(\mathrm{n}\mathrm{s}\mathrm{l}.\mathrm{n}\mathrm{s}2)$

Object$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}^{7}$

subtype? ($\mathrm{S}\mathrm{a}\mathrm{t}\mathrm{o},\mathrm{M}$and subtypel?

$arrow \mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}?(\mathrm{n}1,\mathrm{n}2)$(X.TOP)

使いたい変数に対して$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}//$作る// 使いたい変数に対して$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+?(\mathrm{E}.\mathrm{X})$作る$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}y\mathrm{p}\mathrm{e}+$

?(

?

.TOP)

$\mathrm{M}\mathrm{U}(_{-\prime-})$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$(\mathrm{E},\mathrm{M}\mathrm{U}(_{-\prime}-))arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+?(\mathrm{E},\mathrm{E})arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+?(\mathrm{E}.\mathrm{T}0\mathrm{P})arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$[7]:Type inferr.ence with Simple Selftypes is-complete, Nordic Journalof Computing, Vol. 4, No. 3, 1997, pp. 259286.
$\mathrm{J}\mathrm{i}\mathrm{m},\mathrm{T}.$$\mathrm{P}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{b}\mathrm{e}\mathrm{r}\mathrm{g},\mathrm{J}.,$$\mathrm{N}\mathrm{P}$[8] 寺澤啓司, 酒井正彦, 坂部俊樹 : オブジェクト
指向計算モデルにおける例外処理の形式化, 修$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+?(\mathrm{E},0\mathrm{B}(_{-}))arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}y\mathrm{p}\mathrm{e}+$?(TOP,TOP)
?(
.TOP)

$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$0\mathrm{B}(_{-})$(CONS$(\mathrm{f}\mathrm{s}\mathrm{l}$$arrow \mathrm{s}\mathrm{a}\mathrm{m}\mathrm{e}?(\mathrm{f}\mathrm{s}\mathrm{l},\mathrm{f}\mathrm{s}2)$and$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+?$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+$($0\mathrm{B}$?($0\mathrm{B}(\mathrm{x}),0\mathrm{B}$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$,fssl)),)$0\mathrm{B}(\mathrm{C}0\mathrm{N}\mathrm{S}(\mathrm{f}\mathrm{s}2_{*}\mathrm{f}\mathrm{s}\mathrm{s}2))$$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}+?$(NIL))($0\mathrm{B}$(fssl).

$0\mathrm{B}$(fss2))$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$); 例外の型// subtypel?(as.
: $[]$ \prec bs>の時 true.

as,bs$\mathrm{b}\mathrm{s}$において,$[]<\mathrm{a}\mathrm{s}><$士論文, 名古屋大学大学院工学研究科情報工学専攻, 2000.

subtypel?(NIL,
subtypel?(CONS$\mathrm{n}\mathrm{s}2$)$arrow \mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}2?(\mathrm{n}1,\mathrm{n}\mathrm{s}2)$[9]

堀江美保子, 酒井正彦, 坂部俊樹: オブジェクト

指向計算モデルにおける例外処理の型付, 日本
ソフトウエア科学会第 19 回大会論文集, 2002.

// subtype2?( ,CONS
supertype が CONS
subtype2? ( .CONS$(\mathrm{b}.\mathrm{b}\mathrm{s})$$/\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}$?(a, )$\mathrm{b}$$:\mathrm{a}<:\mathrm{b}$かを判定する. /sub topsubtype?(E.E))
subtype? (E.
)
subtype? (E.
subtype? ( ,TOP)作る
subtype?

の時 true. subtype かどう$//\mathrm{s}\mathrm{a}\mathrm{m}\mathrm{e}?(\mathrm{x}.\mathrm{y}):\mathrm{x}$same?(0B(C0NS$arrow$$arrow$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$0\mathrm{B}(_{-})$$\mathrm{X}$$arrow$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$使いたい変数に対して$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}//$$(\mathrm{E},\mathrm{X})arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$//使いたい変数に対して作とが等しい時, tme)fss1)).0B(C0NS’) and same?(0B(fss1),0B (fss2))$\mathrm{f}\mathrm{s}2$$(\mathrm{f}\mathrm{s}2.\mathrm{f}\mathrm{s}\mathrm{s}2))$$\mathrm{n}2$$(\mathrm{X}.\mathrm{X})arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$//使いたい変数に対して作

same?(xl,)

and same?

$(\mathrm{n}\mathrm{s}\mathrm{l}.\mathrm{n}\mathrm{s}2)$),xsl).CONS(x2,) and same?(xsl,$\mathrm{x}\mathrm{s}2$$\mathrm{x}2$)$(\mathrm{M}\mathrm{U}(\mathrm{x}1.\mathrm{n}\mathrm{t}1).\mathrm{M}\mathrm{U}(\mathrm{x}2,\mathrm{n}\mathrm{t}2))$$\mathrm{s}\mathrm{a}\mathrm{n}\mathrm{e}+’(\mathrm{n}\mathrm{t}1.\mathrm{n}\mathrm{t}2)$☆このノレー) を呼ぶたびに?を作る。
sue に追カ I した$\mathrm{s}\mathrm{a}\mathrm{m}\mathrm{e}+?(\mathrm{x}\mathrm{l},\mathrm{x}.

2)arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$を$\mathrm{s}\mathrm{a}\mathrm{n}\mathrm{e}+$るsubtype?
subtype?
$\epsilon \mathrm{u}\mathrm{b}\mathrm{t}\mathrm{y}\mathrm{p}\mathrm{e}$)$\mathrm{x}\mathrm{s}2)$$(\mathrm{x}1$$\triangleright$

subtype?

$\mathrm{t}\mathrm{y}2$$(\mathrm{T}Y(\mathrm{n}1,\mathrm{n}\mathrm{s}\mathrm{l}).\mathrm{T}\mathrm{V}(\mathrm{n}2.\mathrm{n}\mathrm{s}2))$

same?(nl.

same?
$arrow$る$(\mathrm{n}1,\mathrm{n}\mathrm{s}2)$$(\mathrm{F}\mathrm{S}(11.\mathrm{t}\mathrm{y}\mathrm{l}).\mathrm{F}\mathrm{S}(12.\mathrm{t}\mathrm{y}2))$

same?(C0NS$arrow$)

subtype2?

same?( $11.12\rangle$ and same?(tyl.

same?

$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$)$\mathrm{y}$$(\mathrm{f}\mathrm{s}\mathrm{l}$same?(fsl,same?

$//\epsilon \mathrm{u}\mathrm{b}\mathrm{e}$$\mathrm{T}0\mathrm{P}$$(\mathrm{n}1,\mathrm{n}2)\mathrm{o}\mathrm{r}$$R_{st}$$\mathrm{n}\mathrm{s}2$): 通常の型 a のに存在する時, true.

$(\mathrm{n}2,\mathrm{n}\mathrm{s}2)$$\mathrm{n}1$subtype?

)and subtypel?(nsl,$(\mathrm{b},\mathrm{b}\mathrm{s})$$\mathrm{a}$$arrow$

付録: サブタイプ判定項書換え系

true$arrow$$(\mathrm{n}1.\mathrm{n}\mathrm{s}\mathrm{l}),\mathrm{n}\mathrm{s}2$$(\mathrm{M}\mathrm{U}(_{-},-)\prime \mathrm{T}0\mathrm{P})arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$(\mathrm{E},\mathrm{H}\mathrm{U}(_{\sim},-))arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$?(TOP,TOP)
.TOP)

same?

$(\mathrm{E},\mathrm{E})$same?(ll,11)
same?(NIL,NIL)$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$sane? ($\mathrm{T}0\mathrm{P},$TOP)

same?(12.12)$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$subtype? ($0\mathrm{B}(_{-})$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$//\mathrm{a}\mathrm{n}\mathrm{d}\text{と}$// sub Excep

subtype?

$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$orture and tureor ture$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$(\mathrm{T}\mathrm{Y}(\mathrm{n}1.\mathrm{n}\mathrm{s}1),\mathrm{T}\mathrm{Y}(\mathrm{n}2,\mathrm{n}\mathrm{s}2))$ture or$-arrow \mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$