仕様の定義を行なう。両親を表現するため、parentsとして両親の姓・父親の名・母親の 名の3 引数から両親の名前を格納した項を返す演算の定義を行なった。
NAME X :: TRIV
BASE-SET
X :: TRIV
eq MKparents({nilF},{nilM}) = {nil} .
eq MKparents({nilF},{Mname(Mfa,Mfi),Sm}) =
{parents(Mfa,nilFNam,Mfi) } U MKparents({nilF},{Sm}) .
eq MKparents({Fname(Ffa,Ffi),Sf},{nilM}) =
{parents(Ffa,Ffi,nilMNam) } U MKparents({Sf},{nilM}) .
eq MKparents({Fname(Ffa,Ffi),Sf},{ Sm }) =
{ parents(Ffa,Ffi,getMfi(Ffa,{ Sm })) } U
MKparents({Sf},{Sm}
Mdef {Mname(getMfa(Ffa,{Sm}),getMfi(Ffa,{Sm}))}) .
eq getMfi(Ffa,{ nilM }) = nilMNam .
eq getMfi(Ffa,{Mname(Mfa,Mfi),Sm}) =
if Ffa == Mfa then Mfi else getMfi(Ffa,{Sm}) fi .
eq getMfa(Ffa,{ nilM }) = nilMNam .
eq getMfa(Ffa,{Mname(Mfa,Mfi),Sm}) =
if Ffa == Mfa then Mfa else getMfa(Ffa,{Sm}) fi .
}
}
モジュールグラフ(図5.12)からも明らかであるが、このモジュールでは父親集合と母親 集合とから両親集合を作り出すために、これらに用いる集合をそれぞれ輸入により用意し ている。このとき集合の演算名をそのまま用いたのでは3者で同名の演算を参照すること になり定義が曖昧なものとなる。そこで輸入を行なう際に名前替えを利用してこの曖昧性 を排除する。
モジュールグラフでは名前替えを伴った輸入を行なう際には、同一のモジュールをそれ ぞれ実線で記入することでこの意味を表明することにしていた。ゆえに図5.12ではSETな どのモジュールが実線で3度描かれているのである。
父親集合と母親集合とは名前の集合であるため、SETモジュールの仮パラメータにパラ メータ付きモジュールNAMEを特定化している。モジュールNAME内の演算も名前替えにより 曖昧性排除がされる。コード上でこの作業はデータ構造の輸入を行なうprotecting(...)
の括弧内で一度に記述されているため名無しのビューが用いられている。図中でビューの 菱形の内部にビュー名が記述されていないのはそのためである。
次に仮パラメータを全て文字列に特定化する宣言をおこなう。
module MAKE-Str-PARENTS-SET {
protecting (MAKE-PARENTS-SET
[ FATHER <= view to STRING { sort Elt -> String },
MOTHER <= view to STRING { sort Elt -> String },
PARENTS <= view to STRING { sort Elt -> String}])
}
ここではデータ構造として集合を用いたが、この仕様からの二分木を用いた仕様の導出 を考える。一旦モジュールグラフへ変換して二分木を用いたモデル作成時の変更箇所の特 定を行なう。
モジュールグラフ(図5.13)の(0)がMAKE-PARENTS-SETのモジュールグラフによる表現 である。この図から二分木による実現(5)に至るまでの変更について説明する。
(0)(1):データ構造を二分木に変更するためモジュールグラフ上のデータ構造部分を
書き換える。集合の基本構造を示したモジュールBASE-SETを用いていることから二 分木も基本構造を記述したモジュールBASE-TREEを用意する。
(1)(2):データ構造部分の二分木化を終了。仮パラメータへの制約は全順序関係を記
述したセオリTOSETとなる。
(2)(3):二分木に格納される要素は全順序関係を持つデータ集合となる。このため、
ビューで用いられるセオリもTRIVよりもきつい制約のTOSETとなる。
(3)(4):モジュールNAMEの仮パラメータへの制約も同様に変更が必要になる。
(4)(5):MAKE-PARENTS-SET をMAKE-PARENTS-TREE と改名し、仮パラメータへの制 約を変更する。
上記で終えたモジュールの構造の変更を元にMAKE-PARENTS-SET内の等式を二分木構造 へ対応させる。これでMAKE-PARENTS-TREEの実体を得る。
二分木の定義は BINARY-TREE で行なう。仕様の定義上、列のモジュールを利用する。
BASE-SEQに対する多重のパラメータ化を行なう。
module BINARY-TREE[ELT :: TOSET] {
extending (BASE-SEQ[X <= view to ELT { sort Elt -> Elt }])
[ BinaryTree ]
signature {
op makeBinTree_ : Seq -> BinaryTree
op flatten_ : BinaryTree -> Seq
op nilTree : -> BinaryTree
op binTree : Elt BinaryTree BinaryTree -> BinaryTree
op insert_to_ : Elt BinaryTree -> BinaryTree
op delete_from_ : Elt BinaryTree -> BinaryTree
}
axioms {
var L : Seq
vars E E' : Elt
vars T T' : BinaryTree
eq makeBinTree(nilSeq) = nilTree .
eq makeBinTree(E L) = insert E to (makeBinTree L) .
eq insert E to nilTree = binTree(E, nilTree, nilTree) .
eq insert E to binTree(E', T, T') =
if E < E' or E == E'
then binTree(E', (insert E to T), T')
else binTree(E', T, (insert E to T')) fi .
eq delete E from T = makeBinTree(drop(E,flatten T)) .
eq flatten nilTree = nilSeq .
eq flatten(binTree(E, T, T')) =
((flatten T) $ (E (flatten T'))) .
}
}
集合で仕様化を行なった上記プログラムからデータ構造を二分木に挿替えたことにより、
仮パラメータへの制約であるセオリがただ一つのソート宣言を要求するTRIVから、全順 序関係を定義したTOSETへ変更になった。BINARY-TREEの内部モジュールとして参照して
いるBASE-SEQのセオリを示していないが、内部モジュールのセオリは外部のセオリと等
しいか緩い制約であることが要求される。きつい制約を持つモジュールを内部構造として 参照するモジュール定義は、ビュー宣言の定義から不可能となっている。実際にBASE-SEQ のセオリはTRIVである。
BINARY-TREE の利用によるMAKE-PARENTS-SET のモジュール構造の変化をモジュール グラフで示すことができた。このモジュール構造を元にMAKE-PARENTS-TREEの構築を行 なった。
protecting(BINARY-TREE[ ELT <= view to
NAME [ X <= view to FATHER { sort Elt -> Elt , op _<_ -> _<_ }]
* { sort Name -> FatherName , op name -> Fname }
{ sort Elt -> FatherName , op _<_ -> name< }]
* { sort BinaryTree -> FatherTree , sort Seq -> FatherSeq
op nilTree -> nilFather , op binTree -> binFTree })
protecting(BINARY-TREE[ ELT <= view to
NAME [ X <= view to MOTHER { sort Elt -> Elt , op _<_ -> _<_ }]
* { Renaming to define Mother-SET same as Father . }
protecting(BINARY-TREE[ ELT <= view to PARENTS
{ sort Elt -> Elt , op _<_ -> _<_ }])
signature {
[ Parents < Elt.PARENTS ]
op nilName : -> Elt.PARENTS
op parents : Elt.FATHER Elt.FATHER Elt.MOTHER -> Parents
op parents : Elt.MOTHER Elt.FATHER Elt.MOTHER -> Parents
op MKparents : FatherTree MotherTree -> BinaryTree
op MKparentsSeq : FatherTree MotherTree -> Seq
op getMfi : Elt.FATHER MotherTree -> Elt.MOTHER
op getMfa : Elt.FATHER MotherTree -> Elt.MOTHER
}
axioms {
vars Ffa Ffi : Elt.FATHER ; vars Mfa Mfi : Elt.MOTHER
vars Fr Fl Ftree : FatherTree ; vars Mr Ml Mtree : MotherTree
eq MKparents(Ftree , Mtree) =
makeBinTree(MKparentsSeq(Ftree , Mtree)) .
eq MKparentsSeq(nilFather,nilMother) = nilSeq .
eq MKparentsSeq(nilFather,binMTree(Mname(Mfa,Mfi),Ml,Mr)) =
parents(Mfa, nilName, Mfi)
( MKparentsSeq(nilFather, Ml) $
MKparentsSeq(nilFather, Mr)) .
eq MKparentsSeq(binFTree(Fname(Ffa,Ffi),Fl,Fr),nilMother) =
parents(Ffa, Ffi, nilName)
( MKparentsSeq(Fl, nilMother) $
MKparentsSeq(Fr, nilMother)) .
eq MKparentsSeq(binFTree(Fname(Ffa,Ffi), Fl, Fr),
binMTree(Mname(Mfa,Mfi), Ml, Mr)) =
parents(Ffa, Ffi, getMfi(Fname(Ffa, Ffi),Mtree))
( MKparentsSeq(Fl, getTree(Fname(Ffa,Ffi),
delete Mname(Ffa,getMfi(Fname(Ffa,Ffi),Mtree))
from Mtree))
$ MKparentsSeq(Fr, getTree(Mname(Ffa,Ffi),
delete Mname(Ffa,getMfi(Fname(Ffa,Ffi),Mtree))
from Mtree))) .
}
}