ヒープ メモリにおけるオブジェクト指向演算子の表現

得，更新する関数である．Mはクラス集合Cの要素数であり，iはクラスcに対 応するサブヒープの，ヒープ メモリにおける位置である．N はクラスcに対応す るサブヒープに格納されるタプルの要素数であり，jはそのタプルにおけるuの位 置である．getElem^p_q,setElem^p_qは，p, qに依存して次のように定義される．

getElem^p_q t =

⎧⎪

⎪⎪

⎪⎪

⎪⎪

⎪⎨

⎪⎪

⎪⎪

⎪⎪

⎪⎪

⎩

t (p= 1, q= 1のとき)

F st t (p= 1,1< qのとき)

F st (Snd₍₁₎ (...(Snd_(p−1) t))) (1< p < qのとき) Snd₍₁₎ (...(Snd_(q−1) t)) (p=q,1< qのとき)

setElem^p_q x t=

⎧⎪

⎪⎪

⎪⎪

⎨

⎪⎪

⎪⎪

⎪⎩

x (q = 1のとき)

(getElem¹_q t, ..., getElem^p−1_q t,

x, getElem^p+1_q t, ..., getElem^q_q t) (1< qのとき)

空のストアは，空のサブヒープをタプルにまとめたものとして表現される．

ExRep^cは次のように定義される．

ExRep^c :c→Heap→bool ExRep^c o H ≡V alid^c o H

これはV alid^cそのものである．つまり，クラスcのオブジェクトがストアに存在

することはその参照がクラスcに対応するサブヒープにおいて有効であること同 値である．

GetRep^c,SetRep^cはそれぞれ次のように定義される．

GetRep^c :c→H →attr_c GetRep^c o H ≡Read^c_a o H

SetRep^c :c→attr_c →H →H SetRep^c o x H ≡W rite^c_a o x H

クラスcのオブジェクトの属性の取得，更新は，そのオブジェクト参照が指すタプ ルの属性領域の取得，更新と同値である．

CastRep^c_dは次のように定義される．

CastRep^c_d:c→Heap→d CastRep⎧ ^c_d o H ≡

⎪⎨

⎪⎩

if ExRep^c o H then Read^c_d o H else N ull^d (cd ordc) CastRep^e_d (CastRep^c_e o H) H ((ce, e ⁺ d) or (d⁺ e, ec))

CastRep^c_dはクラスcとdの継承関係の位置について2つの場合に分けて定義され

る．変換元のクラスcと変換先のクラスdが直接の親子関係にある場合は，Read^c_d により，オブジェクト参照が指すブロックに格納されるクラスdのオブジェクト参 照を読み出せばよい．変換を行うオブジェクトが存在しない場合は変換先のクラ スのNULLオブジェクトN ull^dに変換したこととする．cとdが直接の親子関係で はない継承関係にある場合は，型変換を推移的に適用すればよい．つまり，まずc と直接親子関係にあるクラスeに変換してから次にそれをdに変換する．

N ewRep^cは次のように定義される．

N ewRep^cH ≡

⎧⎪

⎪⎪

⎪⎪

⎪⎪

⎪⎨

⎪⎪

⎪⎪

⎪⎪

⎪⎪

⎩

Add^c def ault_c H (cがルートのとき)

let (o₁, H₁) =N ewRep^d H in

let (o₂, H₂) =Add^c def ault_c H₁ in

let H₃ =Link_c^d o₁ o₂ H₂ in (o₂, H₃) (dc) where

Link^d_c o₁ o₂ H ≡W rite^c_d o₂ o₁ (W rite^d_c o₁ o₂ H)

def ault_c ≡((V(c, a₁), ...,V(c, a_n)), N ull^d, N ull^e1, ..., N ull^em) (a_i ∈ Mattr(c), dc, ce_j)

N ewRep^cはクラスcのオブジェクトを，ルートクラスからクラスcに至るまでの

継承関係に関して再帰的に構築する．生成されたオブジェクトは複数のタプルが連 結した構造となる．まず，初期段階としてルートクラスのインスタンスを生成する 場合，Add_cにより，クラスcのサブヒープに新たなタプルを追加する．次に，帰納 段階としてルート以外のクラスのインスタンスを生成する場合，まず，N ewRep^d により親クラスdのインスタンスを生成する．次に，Add^cにより，クラスcのサ ブヒープに新たなタプルを追加し，最後に，得られた二つのオブジェクト参照o₁, o₂をLink_d^cによりリンクする．Link^c_dは，W rite^d_c,W rite^c_dによって，o₁,o₂それぞ れが指すタプルのオブジェクト参照の要素にo₂, o₁を書き込む関数として定義さ れる．なお，クラスcのサブヒープに追加するタプルdef ault_cの各要素は，属性 aの場合はそのデフォルト値のタプル(V(c, a₁), ...,V(c, a_n))，親クラスd，子クラ スe_jのオブジェクト参照の場合はそのクラスのNULLオブジェクトN ull^d,N ull^ej とする．

IsRep^c_dは次のように定義される．

IsRep⎧ ^c_d o H ≡

⎪⎨

⎪⎩

ExRep^c o H∧

j¬ExRep^ej (CastRep^c_ej o H) H (c=d, ce_j) ExRep^c o H∧IsRep^e_d (CastRep^c_e o H) H (ce, e^∗ d)

IsRep^c_dは見かけの型cを持つオブジェクトがクラスdのインスタンスであるかど

うかを判定する述語であるが，これを判定するには，型cのオブジェクト参照が指 すタプルから祖先クラスの方向にクラスdのサブヒープに格納されるタプルまで リンクしていることを調べればよい．子クラスのタプルとリンクしているかど う かは，子クラスに型変換した結果のオブジェクトがストアに存在するかで判別す ることができる．この述語はc= dとc ⁺ dの 2 つの場合に分けて定義される．

c=dである場合，cオブジェクトからどの子クラスe_jのタプルにもリンクしてい なければよい．つまり，cオブジェクトを子クラスe_jに型変換した結果のオブジェ クトがストアに存在しなければよい．c ⁺ dである場合，cオブジェクト参照を dを子孫とする子クラスeに型変換し，それがdのインスタンスであればよい．い ずれの場合もcオブジェクトがストアに存在していなければならない．