Sho cu s: Abs ac Poin e s"
J. Ma co
[email p o ec ed] c.es
X. F anch
anc[email p o ec ed] c.es
Dep . Llengua ges i Sis emes In o ma ics (LSI)
Uni e si a Poli ecnica de Ca alunya (UPC)
Campus No d
Jo di Gi ona Salgado, 1-3
08034 BARCELONA
Abs ac
In his wo k we p esen he sp ecica ion and he implemen a ion o a new abs ac da a yp e
(ADT) called
STORE
. This new ADT allows he s o age o a gi en collec ion o elemen s oe ing
an abs ac mechanism ha supplies a di ec access o hem, al e na i e o he me ho d dened
by he s anda d op e a ions o usual ADTs. The in e es o he new mechanism s ems om he
eciency o p oin e s, while a oiding he loss o mo dula i y ha usually o ccu s when p oin e s a e
used. The implemen a ion o he op e a ions oe ed by he new ADT is done by de i a ion om
he equa ional sp ecica ion. The ep esen a ion chosen o he implemen a ion o he new ADT
makes he eciency p e iously men ioned p ossible, e en when he ep esen a ion s a egy equi es
he mo emen o he elemen s.
1
Con en s
1In o duc ion 3
2 The ADT
STORE
4
2.1 Op e a ions . ... ... .. ... ... ... ... ... .. ... ... ... ... ... . 5
2.1.1 Cons uc o Op e a ions . ... ... ... ... .. ... ... ... ... ... . 5
2.1.2 Obse e Op e a ions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.1.3 Mo die Op e a ions ... ... ... ... ... .. ... ... ... ... ... . 6
2.2 Equa ional sp ecica ion .. ... ... ... ... ... .. ... ... ... ... ... . 6
2.2.1 Equa ions b e ween Cons uc o Op e a ions .. .. ... ... ... ... ... . 6
2.2.2 Equa ions o he Obse e Op e a ions .. ... .. ... ... ... ... ... . 8
2.2.3 Equa ions o Mo die Op e a ions . . . . . . . . . . . . . . . . . . . . . . . . . . 10
3 Implemen a ion in Main Memo y 14
3.1 The Typ e Rep esen a ion . ... ... ... ... ... .. ... ... ... ... ... . 15
3.2 De i ing co de o he op e a ions ... ... ... ... .. ... ... ... ... ... . 19
3.2.1 De i a ion o
pu
.. ... ... ... ... ... .. ... ... ... ... ... . 19
3.3 Chosing implemen a ions o he comp onen s o he ep esen a ion . ... ... ... . 25
4 An Example: The Tennis Ladde 26
4.1 Aho, Hop c o & Ullman's Solu ions o he P oblem . .. ... ... ... ... ... . 26
4.2 The solu ion wi h he ADT
STORE
. ... ... ... .. ... ... ... ... ... . 28
5 Co dica ions 29
6 Conclusions 30
2
1 In o duc ion
The p esen wo k deals wi h he me ho dology o mo dula p og am de elopmen by means o abs ac
da a yp es (ADT). The mo dula me ho dology oe s many imp o an p op e ies such as unde s anding,
abs ac ion, eusabili y, e c., bu , o en, i implies a loss o eciency due o he imp ossibili yo
accessing implemen a ion o ADTs om o he mo dules.
O en, while designing a da a s uc u e, we ace he p oblem o educing he space cos (i.e.,
minimising edundan da a) o he emp o al cos (i.e., accessing mo e as e o da a). Too e come
hese p oblems wemay need an implemen a ion which p e mi s he access o he da a by means
o p oin e s (see, e.g, 1, pag. 149]). Recall ha he no ion o
poin e
co esp onds o he memo y
add ess o a gi en ob jec (wi h some high-le el acili ies, which a y among he die en p og amming
languages). Un o una ely, he use o p oin e s causes in gene al a comple e loss o mo dula i y b ecause:

I is necessa y o know he unde lying da a s uc u e used in he implemen a ion and he e o e,
in o ma ion hiding is no accomplished.

Co ec ness p o o s and so wa e main enance and eusabili y a e, in gene al, mo e complica ed.
Also, p og ams a e mo e dicul o unde s and.

An implemen a ion using p oin e s needs o gua an ee ha da a will no change hei p osi ion in
he s uc u e o he wise wewould no access he desi ed in o ma ion (unless all clien mo dules
keep acko changes and his may b e imp ossible).

When he implemen a ion is done by means o p oin e s no only he ADT op e a ions can b e
used bu also we can access di ec ly o i s ep esen a ion and manipula e i . The e o e, i is
p ossible o manipula e ADTs wi hou esp ec ing he p olicy dened by hei equa ions.
Wi h he aim o a oiding hese d awbacks, we p op ose he design o a new ADT, which no only
p e mi s o s o e da a and o access hem bymeans o akey, bu also allows o di ec access o da a
wi hou knowing how hey a e s o ed. We should men ion ha he addi ion o his mechanism will
b e done by dening i s o mal seman ics. Ce ainly, he idea o s udy his new ADT comes om he
necessi y o a comp omise b e ween mo dula i y and eciency.
The goal o he p esen wo k is o p esen he design o his new ADT which oe s, in he one hand,
unc ions o da a s o age and access bykey o da a s uc u es, indep enden ly o hei o ganiza ion
3
and o he key yp e and, on he o he hand, he p ossibili y o a di ec access o da a by means o
an add ess we call he
sho cu
. Essen ially,we ob ain an abs ac mechanism inside he ADT which
co esp onds o he p oin e s in b o h concep and eciency.
The es o he pap e is o ganized as ollows. In sec ion 2, we p esen he algeb aic sp ecica ion
o he new ADT showing he so s and he op e a ions oe ed as well as he equa ions ha dene
he b eha iou o each o hem. In sec ion 3, wecho ose  s he ep esen a ion o he new da a yp e,
hen we show he comple e de i a ion o one o he op e a ions and nally we indica e he cos o
each op e a ion, dep ending on he de ailed implemen a ion o he ep esen a ion used. In sec ion 4, we
conside a classic example ha equi es he use o p oin e s o eciency easons, and whe e we can see
ha he use o he new ADT assu es he same eciency wi hou losing mo dula i y a all. In sec ion
5, we include se e al conclusions ega ding he co dica ion o he new ADT in ADA, Mo dula-2 and
C++. Finally, in sec ion 6, we summa ise he ad an ages o he new ADT and we p esen some op en
ques ions o u he esea ch. This pap e is based on 11], whe e all he emaining discussions can b e
ound, ega ding he de i a ion o all he op e a ions and de ails o he h ee implemen a ions.
2 The ADT
STORE
Since wewan o ob ain an ADT which p e mi s o s o e any kind o in o ma ion, weha e designed an
ADT ha is gene ic" ( pa ame e ized"). The new ADT, called
STORE
, has he da a o b e s o ed
as a pa ame e , decomp osed in o
key
and
in o ma ion
. The pa ame e
key
is used o access he da a.
The e a e no op e a ions equi ed on
in o ma ion
 he so
key
mus ha e compa ison op e a ions
1
.
The ADT
STORE
oe s wo so s:

s o e:
whe e he da a is s o ed.

sho cu :
which supplies he di ec access o he s o ed da a.
1
F om now on, we use he op e a ion symbol
cmp
o e e o he equali y op e a ion.
4
2.1 Op e a ions
2.1.1 Cons uc o Op e a ions
c ea e:
;!
s o e
c ea es an emp y s o e.
pu : s o e, key, in o ma ion
;!h
s o e, sho cu
i
e u ns a pai o med by he esul ing s o e a e adding he pai o key and in o ma ion,
and he sho cu whichgi es di ec access o his pai .
Al e na i ely,we could decomp ose
pu
in o wo op e a ions, one o each comp onen o he esul .
Howe e , weha e p e e ed he ab o e men ioned s uc u e o he sake o clea ness o algeb aic
sp ecica ion p esen ed in Subsec ion 2.2.
2.1.2 Obse e Op e a ions
ge In Key: s o e, key
;!
in o ma ion
e u ns he in o ma ion asso cia ed o he key. P econdi ion: he key is in he s o e.
ge In Sho: s o e, sho cu
;!
in o ma ion
e u ns he in o ma ion asso cia ed o he sho cu . P econdi ion: he sho cu has da a
asso cia ed inside he s o e.
ge Key: s o e, sho cu
;!
key
e u ns he key asso cia ed o he sho cu . P econdi ion: he sho cu has da a asso cia ed
inside he s o e.
isIn?: s o e, key
;!
bool
e u ns a b o olean alue indica ing whe he he key is in he s o e.
ge Sho cu : s o e, key
;!
sho cu
e u ns he sho cu asso cia ed o he key. P econdi ion: he key is in he s o e.
isEmp y?: s o e
;!
bool
e u ns a b o olean alue indica ing whe he he s o e is emp y.
5

2.1.3 Mo die Op e a ions
emo e: s o e, sho cu
;!
s o e
e u ns he esul ing s o e a e emo ing he da a asso cia ed o he sho cu . P econdi-
ion: he sho cu has da a asso cia ed inside he s o e.
modi y: s o e, sho cu , in o ma ion
;!
s o e
e u ns he esul ing s o e a e subs i u ing he in o ma ion asso cia ed o he sho cu ,
by he new in o ma ion. P econdi ion: he sho cu has da a asso cia ed inside he s o e.
2.2 Equa ional sp ecica ion
Following he gene al me ho d o algeb aic sp ecica ion wi h ini ial seman ics, wegi e  s he equa-
ions b e ween cons uc o op e a ions 4, 5, 6].
2.2.1 Equa ions b e ween Cons uc o Op e a ions
I seems ha we could assume ha he
s o es
b eha e as se s, in ha he o de ing in which he da a
a e s o ed is no imp o an . Ac ually his happ ens in able" like ADT's 6]. In o de o assu e his
p op e ywe should ha e o gua an ee ha , o a gi en
key
,we ob ain always he same
sho cu
,
ega dless o he momen in which he
key
and i s
in o ma ion
a e s o ed. This would imply ha
die en keys could no ha e he same
sho cu
 o he wise, s o ing an
in o ma ion
and a
key
implies a
isk o mo di ying he
in o ma ion
o ano he key (o he same
sho cu
) whichwas s o ed p e iously.
The e o e, he e should b e a unique
sho cu
co esp onding o a
key
, and his, in u n, equi es he
numbe o keys and he keys hemsel es o b e known b e o e hand. Al e na i ely,we can do i byan
injec i e unc ion om he se o keys o he se o sho cu s. The las equi emen is e y es ic i e,
i wewan he
s o e
o b e indep enden om he
key
.
Weo e come his es ic ion, by le ing he
sho cu
o dep end also on he
s o e
, and in his way
die en keys can ha e he same
sho cu
, i hey a e s o ed in die en s o es. The e o e, he o de
in which da a a e s o ed is imp o an , and hus
s o es
will no b eha e as se s.
Now, le us conside he ela ions b e ween he wo consecu i e
pu
op e a ions, when we s o e
some
in o ma ion
wi h a
key
whichwas p e iously in he
s o e
. Since we can ha e only a unique
in o ma ion
asso cia ed o each
key
, he esul will b e ha o eplacing he
in o ma ion
asso cia ed o
he
key
by he new
in o ma ion
. The ques ion ha a ises he e is: whichis he
sho cu
ob ained?
6
Since he e was a
sho cu
asso cia ed o he
key
( i.e., he
sho cu
ob ained when s o ed he p e ious
in o ma ion
) and since wewan a unique
sho cu
co esp onding o he
key
, hen i is p ecisely he
o me
sho cu
he one we will ob ain.
Le us see he equa ions which exp ess hese ela ions. Le us s a by hose ela ed o s o es we
will use he op e a ion
isIn?
which ell us whe he he key is in he s o e. This op e a ion is used only
when he s o e is no emp y, b ecause o he wise he s o e would no ha e his ela ion.
In he case when he
key
is he ein, we conside he ollowing wo cases:
1. The key is he las one added o he s o e.
2. The key exis s bu i is no he las one.
In he  s case, he equa ion is simple i jus exp esses he ac ha he ob ained s o e will b e
he same as i he las ime we had s o ed he new in o ma ion.
h
isIn?(pu (s ,k
1
,i
1
).s o e,k
2
)
^
cmp(k
1
,k
2
)
i
)
pu (pu (s ,k
1
,i
1
).s o e,k
2
,i
2
).s o e = pu (s ,k
2
,i
2
).s o e
In he second case, he equa ion exp esses he swap b e ween he wo las keys ob aining his:
h
isIn?(pu (s ,k
1
,i
1
).s o e,k
2
)
^:
cmp(k
1
,k
2
)
i
)
pu (pu (s ,k
1
,i
1
).s o e,k
2
,i
2
).s o e = pu (pu (s ,k
2
,i
2
).s o e,k
1
,i
1
).s o e
No ice ha in his case he e is no a subs i u ion o he in o ma ion asso cia ed o he key, bu
applying his equa ion successi ely,we will a i e o he  s case since he key is he ein. The e o e,
we can apply he  s equa ion and in his way o subs i u e he in o ma ion asso cia ed o he key.
Le us see now he equa ions o sho cu s. As b e o e, we dis inguish wo cases:
1. The key is he las one added o he s o e.
2. The key exis s, bu i is no he las one.
In he  s case, we only ha e o exp ess ha he ob ained
sho cu
will b e he one ob ained
p e iously.
h
isIn?(pu (s ,k
1
,i
1
).s o e,k
2
)
^
cmp(k
1
,k
2
)
i
)
pu (pu (s ,k
1
,i
1
).s o e,k
2
,i
2
).sho cu = pu (s ,k
1
,i
1
).sho cu
7
In he second case weha e o jus exp ess ha he ob ained
sho cu
will b e he same as he one
ha wewould ha e ob ained, i he new key and he new in o ma ion had b een s o ed in he p e ious
s o e.
h
isIn?(pu (s ,k
1
,i
1
).s o e,k
2
)
^:
cmp(k
1
,k
2
)
i
)
pu (pu (s ,k
1
,i
1
).s o e,k
2
,i
2
).sho cu = pu (s ,k
2
,i
2
).sho cu
This do es no sp eci y ye comple ely he b eha iou o sho cu s, b ecause weha e no conside ed
he case in which he key is no he ein in ac , in his case,
pu
may e u n any alue as sho cu
bu he access o he sho cu should supply he app op ia e esul s. The equa ions o he op e a ion
ge In Sho
will desc ib e his b eha iou , as gi en nex .
2.2.2 Equa ions o he Obse e Op e a ions
Le us s udy now he b eha iou o he obse e op e a ions.

The equa ions o
ge In Sho
:
{
The  s one will b e an e o equa ion, indica ing ha he op e a ion is no dened o an
emp y
s o e
. Recall ha his op e a ion is pa ial.
ge In Sho(c ea e,sc) = e o
{
We also include an equa ion o exp ess, he b eha iou when he
sho cu
whose
in o ma ion
wewan o consul is he same as he one e u ned in he las op e a ion o
s o e
.The
in o ma ion
ha we will ob ain will b e he one o his las op e a ion. In o de o compa e
he
sho cu s
we will use a p i a e op e a ion, deno ed
cmp
.
h
cmp(sc,pu (s ,k,i).sho cu )
i
)
ge In Sho(pu (s ,k,i).s o e,sc) = i
{
The nex equa ion indica es ha , i he
sho cu
is no he same as he one ob ained in
he las op e a ion o
pu
, hen he esul o consul ing he in o ma ion asso cia ed o he
sho cu
will b e he same as consul ing he p e ious
s o e
.
h
:
cmp(sc,pu (s ,k,i).sho cu )
i
)
ge In Sho(pu (s ,k,i).s o e,sc) = ge In Sho(s ,sc)
8
No ice ha , i he e was no
in o ma ion
asso cia ed o he
sho cu
,by applying successi ely
his equa ion, wewould ob ain
s =c ea e
, and he e o e om he  s equa ion his is an
e o .

Equa ions o
ge Key
, simila o hose o
ge In Sho
:
ge Key(c ea e,sc) = e o
h
cmp(sc,pu (s ,k,i).sho cu )
i
)
ge Key(pu (s ,k,i).s o e,sc) = k
h
:
cmp(sc,pu (s ,k,i).sho cu )
i
)
ge Key(pu (s ,k,i).s o e,sc) = ge Key(s ,sc)

The Equa ions o
ge In Key
:
{
The  s equa ion s a es ha , i he
key
o b e consul ed is he las one s o ed hen we will
ob ain he las he
in o ma ion
s o ed.
h
cmp(k
1
,k
2
)
i
)
ge In Key(pu (s ,k
1
,i).s o e,k
2
)= i
{
I he condi ion o he  s equa ion do es no hold hen weha e a second equa ion, and
he co esp onding esul will b e ha o applying
ge In Key
on he p e ious
s o e
.
h
:
cmp(k
1
,k
2
)
i
)
ge In Key(pu (s ,k
1
,i).s o e,k
2
)=ge In Key(s ,k
2
)
{
Since he op e a ion in ques ion is a pa ial one (b ecause i is no dened when he
key
is no in he
s o e
)wemus also add a las equa ion which indica es ha consul ing he
in o ma ion
asso cia ed o a
key
in an emp y
s o e
will b e an e o .
ge In Key(c ea e,k) = e o

Equa ions o
isIn?
:
{
The  s equa ion is in ui i ely clea . I we apply
isIn?
o a
key
and o an emp y
s o e
,
hen he esul will b e alse.
isIn?(c ea e,k) = alse
{
In he same way, he second equa ion comes na u ally. I he
key
o whichwe apply he
op e a ion
isIn?
is he las one added o he
s o e
, hen he esul will b e ue i he
key
is no he las one added, hen he esul will b e ha o applying
isIn?
o he p e ious
s o e
.
9
Using his ep esen a ion o he yp e
s o e
we s ill ha e an op e a ion o high cos , namely he
pu
op e a ion. When we s o e he da a by means o a
key
which is al eady in he
s o e
,weha e only o
ob ain he
sho cu
asso cia ed o he
key
and hen using i o access o he a ay, assigning he alue
o he new da a. In his case, he cos is ha o consul ing he able. Howe e , when he
key
is no
in he
s o e
,weha e o sea ch o ee p osi ion in he a ay, and his, in he wo s case, has linea
cos . Toa oid his cos we add ano he s uc u e o nd quickly a ee p osi ion. This s uc u e is a
queue whe e he ee p osi ions o he a ay a e s o ed (see Fig. 3). Wi h his mo dica ion, he cos
o nding a ee p osi ion is cons an (p o ided ha he implemen a ion o he queue is go o d enough,
i co esp onds jus o ob aining he  s elemen o he queue). The cos o pu ing a p osi ion as a
ee one, while emo ing, could b e made also cons an i i jus co esp onds o he cos o pu ing an
elemen o he queue.
k
1
k
6
k
5
k
3
k
2
k
4
     
1 2 3 4 5 6 7 8 9 10 11 12 13
k
5
k
1
k
3
k
6
k
4
k
2
in
5
in
1
in
3
in
6
in
4
in
2
j
q


q)
-
      
-
666I 66
Figu e 3: a ay, able and queue
16

The ep esen a ion o he new so s o da a is:

s o e
is implemen ed by a eco d consis ing o h ee elds:
1.
a
: a ayo
n
comp onen s, whe e he alid indices a e he na u al numbe s be ween 1 and
n
, o a ce ain na u al
n
 he comp onen s o he a ay a e pai s consis ing o wo elds:
in
(o yp e
in o ma ion
)and
key
(o yp e
key
).
2.
: a queue o
sho cu s
i.e., a queue con aining he indices co esp onding o he ee p osi-
ions o he a ay.
3.
: is a able o pai s
h
k ey  sho cu
i
.

The
sho cu
is implemen ed by a na u al in he ange 0
:::n
. The alue 0 is used as an undened
alue. The es o he alues will co esp ond o he indices o he a ay.
To e i y ha he implemen a ion o he new ADT is co ec wi h esp ec o i s sp ecica ion we
ollow he me ho d p esen ed in 8]. I consis s o dening he abs ac ion unc ion, which ans o ms a
alue o he implemen a ion o a alue o i s mo del, deno ed by a e m which b elongs o i s asso cia ed
equi alence class in he quo ien - e m algeb a 4]. Since his unc ion is pa ially dened, wemus
also dene he in a ian o he ep esen a ion which es ablishes he condi ion ha he alues o he
implemen a ion mus sa is y so o ep esen alid alues o he ADT. Also, we need o indica e when
wo die en alues o he implemen a ion co esp ond o he same alue o ADT unde implemen a ion,
in o he wo ds, weha e o sp eci y he edeni ion o he equali y.
He e is a sho desc ip ion o he a ay, queue and able op e a ions, esp ec i ely, ha we a e going
o use.
cons
(
a p
) e u ns he alue in he p osi ion
p
o he a ay
a

ass
(
a p
) assigns he alue
in
he p osi ion
p
o he a ay
a

pu F i s
(
q
) pu s he alue
in he on o he queue
q

assig n
(
 k 
)
asso cia es he alue
o he key
k
in he able

deassig n
(
 k
) asso cia es an undened alue o he
key
k
in he able
 and
l ook up
(
 k
) e u ns he alue asso cia ed o he key
k
in he able
.
The Abs ac ion Func ion
con e
(
h
a 
i
)=
8
>
>
>
>
<
>
>
>
>
:
c ea e
i
=TABLE.c ea e
pu
(
con e
(
h
a pu F i s
(
 sc
)
 deassig n
(
 k
)
i
)
 k  cons
(
a sc
)
:in
)
:s o e
i
=assign( ',k,sc)
17
The Rep esen a ion In a ian
The ep esen a ion in a ian mus assu e ha e e y p osi ion o he a ay is ee o o ccupied bu no
b o h o hem a he same ime. The e o e, i indica es ha any p osi ion o he a ay, i.e., any na u al
be ween 1 and
n
mus b e ei he in he queue o ee p osi ions (only once) o as a alue asso cia ed o
a
key
in he able. In his las case, he
key
canno b e wha e e : i mus coincide wi h he alue o
he eld o he a ay in his p osi ion. Since a
sho cu
canno b e asso cia ed o mo e han a
key
,a a
ce ain momen , wemus assu e also ha , gi en a p osi ion he e is only one
key
in he able whichi
is asso cia ed o.
Bu he
sho cu
dep ends on he
s o e
, he e o e he ep esen a ion in a ian mus indica e which
is he
sho cu
ha will assign ou ep esen a ion when we s o e an in o ma ion by means o a
key
ha is no ound in he
s o e
. Since he only condi ion ha mus sa is y he
sho cu
, is no o b e
asso cia ed o ano he
key
,any o he queue p osi ions can b e used, o ins ance i s head.
We can now w i e down he in a ian .
Fi s we will dene a p edica e ha indica es whe he a
sho cu
b elongs only once o he queue.
8
2
q ueue

8
sc sc
1
sc
2
2
sho cu
uniq ue
(
c ea e sc
)=
alse sc
2
c ea e
=
alse
uniq ue
(
enq ueue
(
 sc
)
sc
)=
:
(
sc
2
)
sc
2
enq ueue
(
 sc
)=
ue

:
ig
(
sc
1
sc
2
)]
)

:
ig
(
sc
1
sc
2
)]
)
uniq ue
(
enq ueue
(
 sc
1
)
sc
2
)=
uniq ue
(
 sc
2
)
sc
2
2
enq ueue
(
 sc
1
)=
sc
2
2
In Rep(
h
a 
i
)

8
j
:1

j

n
:


uniq ue
(
 j
)
^:9
k
:
l ook up
(
 k
)=
j

_

:
(
j
2
)
^9
!
k
:
lookup
(
 k
)=
j


^
8
k
:
l ook up
(
 k
)
6
=
unde ined
:
cons
(
a l ook up
(
 k
))
:key
=
k
^
8
k
:
:
isI n
?(
con e
(
h
a 
i
)
k
):
pu
(
con e
(
h
a 
i
)
ki
)
:sho cu
=
head
(
)
The Equali y Redeni ion
The equali y edeni ion exp esses ha he alues o he a ay in i s ee p osi ions ( hose ound in
he queue) a e no ele an o he abs ac alue. This means ha he same
s o e
is ob ained i any
ee p osi ion o he a aywe e mo died. Also, i should exp ess ha wo
s o es
a e equal when wo
ables, cons uc ed in die en ways, con ain he same se o pai s. Bu his has b een con empla ed in
he equa ions o he yp e able, and he e o e he e is no need o include i in he equali y edeni ion.
18
8
j
:1

j

n
^
(
j
2
):
con e
(
h
a 
i
)=
con e
(
h
ass
(
a j al
)
 
i
)
3.2 De i ing co de o he op e a ions
In his subsec ion, we p esen he de i a ion o he implemen a ion a pa icula op e a ion,
pu
,asa
case s udy o he whole de i a ion p o cess
2
. In o de o simpli y he demons a ions wewo k unde
he hyp o hesis ha
n
is big enough o assu e ha he queue is ne e emp y. La e , a he nal
implemen a ion, weha e conside ed his p ossible case o e o .
3.2.1 De i a ion o
pu
Acco ding o 8] he op e a ion
pu
mus b e implemen ed by a unc ion sa is ying he ollowing p e-p os
sp ecica ion:
unc ion
impl pu (
h
a:a ay :queue : able
i
 k:keyi:in o ma ion)
e u n
hh
a
1
:a ay
1
:queue
1
: able
i
 sc:sho cu
i
P e: In Rep(
h
a, ,
i
)
g
P
Pos : In Rep(
h
a
1
,
1
,
1
i
)
^
con e (
h
a
1
,
1
,
1
i
)=pu (con e (
h
a, ,
i
),k,i).s o e
^
sc=pu (con e (
h
a, ,
i
),k,i).sho cu
g
e u n
hh
a
1
,
1
,
1
i
,sc
i
The de i a ion o his unc ion is c ucial o he e ica ion p o cess no only b ecause o i s dicul y
bu also due o he ac ha weha e o p o e, p e iously, a se ie o lemmas necessa y also o he
de i a ion o he es o he unc ions.
The Lemmas ega ding he ables
Lemma 1

lookup(assign( ,k,sc),k
1
)=undened
]
):
ig(k,k
1
)
Lemma 2

lookup( ,k)=undened
]
)
deassign( ,k)=
Lemma 3

lookup( ,k)=undened
]
)
deassign(assign( ,k,sc),k)=
Lemma 4

lookup( ,k)
6
=
undened
]
)
6
=
TABLE.c ea e
2
See 11] o he comple e de i a ion.
19
Lemma 5

lookup( ,k)
6
=
undened
]
)
=assign(
1
,k,lookup( ,k))
Lemma 6
lookup(deassign( ,k),k)=undened
Lemma 7

=assign(
1
,k
1
,sc
1
)
]
)
=assign(
2
,k
1
,sc
1
)
^
lookup(
2
,k
1
)=undened
Lemma 8
isIn?(con e (
h
a, ,
i
),k)=(lookup( ,k)
6
=
undened)
The Lemmas ega ding he queues
Lemma 9
pu Fi s (dequeue(q),head(q))=q
Lemma 10
head(pu Fi s (q, ))=
Using hese lemmas le us see he de i a ion o he unc ion
pu
.
The esul o he op e a ion will dep end on whe he he
key
o b e s o ed is ound in he
s o e
o
no . The e o e, we conside an al e na i e o he design o he unc ion. Since, om Lemma 8, he
esul o
isIn?(con e (
h
a, ,
i
),k)
is equi alen o
lookup( ,k)
6
=
undened
we will pu his las one as a
condi ion o he al e na i e.
unc ion
impl pu (
h
a:a ay :queue : able
i
 k:keyi:in o ma ion)
e u n
hh
a
1
:a ay
1
:queue
1
: able
i
 sc:sho cu
i
P e: In Rep(
h
a, ,
i
)
g
i
lo okup( ,k)=undened
hen
A
1
:In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
g
P
1
else
A
2
:In Rep(
h
a, ,
i
)
^
lo okup( ,k)
6
=undened
g
P
2
end i
Pos : In Rep(
h
a
1
,
1
,
1
i
)
^
con e (
h
a
1
,
1
,
1
i
)=pu (con e (
h
a, ,
i
),k,i).s o e
^
sc=pu (con e (
h
a, ,
i
),k,i).sho cu
g
e u n
hh
a
1
,
1
,
1
i
,sc
i
20
Le 's see wha asse ion we can deduce om A
1
.
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
)
( Lemma 8 )
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^:
isIn?(con e (
h
a, ,
i
),k)
)
( Deni ion o In Rep )
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
)
( Equali y Redeni ion and head( )
2
)
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
^
con e (
h
a, ,
i
)= con e (
h
ass(a,head( ),
h
k,i
i
), ,
i
)
)
( The in o duc ion o he op e a ion pu in b o h sides o he equali y)
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,head( ),
h
k,i
i
), ,
i
),k,i).s o e
)
( Lemma 3 )
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,head( ),
h
k,i
i
), ,deassign(assi gn ( ,k,head( )),k)
i
),k,i).s o e
)
( Lemma 9 )
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
^
pu (con e (
h
a, ,
i
),k,i).s o e=
pu (con e (
h
ass(a,head( ),
h
k,i
i
),pu Fi s (d equeu e( ),head( )),deassi gn(ass ign ( ,k,head( )),k)
i
),k,i).s o e
)
( Eq. o a ay cons(ass(A,i, ),i)= )
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,head( ),
h
k,i
i
),pu Fi s (deq ueue( ),head( )),
deassign(assign ( ,k,head( )),k)
i
),k,cons(ass(a,hea d( ),
h
k,i
i
), head( )).in ).s o e
)
( Abs ac ion Func ion )
In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
^
pu (con e (
h
a, ,
i
),k,i).s o e= con e (
h
ass(a,head( ),
h
k,i
i
),dequeue( ), assign( ,k,head( ))
i
)
)
( In Rep(
h
a, ,
i
)
^
lo okup( ,k)=unden ed]
)
In Rep(
h
ass(a,head( ),
h
k,i
i
),dequeue( ), assign( ,k,head( ))
i
))
In Rep(
h
ass(a,head( ),
h
k,i
i
),dequeue( ), assign( ,k,head( ))
i
)
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head( )
^
pu (con e (
h
a, ,
i
),k,i).s o e= con e (
h
ass(a,head( ),
h
k,i
i
),dequeue( ), assign( ,k,head( ))
i
)
The e o e, om A
1
we can deduce his las asse ion, deno ed A
3
.
Le 's see wha asse ion we can deduce om A
2
.
In Rep(
h
a, ,
i
)
^
lo okup( ,k)
6
=undened
)
( Lemma 5 )
In Rep(
h
a, ,
i
)
^
=assign(
1
,k,lo okup( ,k)) )
21

)
( Abs ac ion Func ion )
In Rep(
h
a, ,
i
)
^
con e (
h
a, ,
i
)= pu (con e (
h
a,pu Fi s ( ,lo oku p( ,k)),deassi gn( ,k)
i
),k, cons(a,lo okup( ,k)).in ).s o e
)
( Equali y Redeni ion and
8
k:k
2
pu Fi s ( ,k) )
In Rep(
h
a, ,
i
)
^
con e (
h
a, ,
i
)= pu (con e (
h
ass(a,lo okup ( ,k),
h
cons(a,lo o kup ( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassig n( ,k)
i
),k,cons(a,lo okup ( ,k)).in ).s o e
)
( The in o duc ion o he op e a ion pu in b o h sides o he equali y)
In Rep(
h
a, ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (pu (con e (
h
ass(a,lo oku p( ,k),
h
cons(a, lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
),k,cons(a,l o oku p( ,k)).in ).s o e,k,i).s o e
^
pu (con e (
h
a, ,
i
),k,i).sho cu = pu (pu (con e (
h
ass(a,lo o kup( ,k),
h
cons (a, lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
),k,cons(a,lo oku p( ,k)).in ).s o e,k,i).sho cu
)
( Eq. o s o e pu (pu (s ,k,i
1
).s o e,k,i
2
).s o e= pu (s ,k,i
2
).s o e, and
pu (pu (s ,k,i
1
).s o e,k,i
2
).sho cu =pu (s ,k,i
1
).sho cu )
In Rep(
h
a, ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,lo okup( ,k),
h
cons(a , lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
),k,i).s o e
^
pu (con e (
h
a, ,
i
),k,i).sho cu = pu (con e (
h
ass(a,lo oku p( ,k),
h
cons(a, lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
),k,cons(a,l o ok up( ,k)).in ).sho cu
)
( Eq. o a ay cons(ass(A,i, ),i)= )
In Rep(
h
a, ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,lo okup( ,k),
h
cons(a , lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn ( ,k)
i
),k,cons(ass(a,lo okup ( ,k),
h
cons(a,lo okup( ,k)).key,i
i
),lo ok up( ,k)).in ).s o e
^
pu (con e (
h
a, ,
i
),k,i).sho cu = pu (con e (
h
ass(a,lo oku p( ,k),
h
cons(a, lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
),k,cons(a,l o oku p( ,k)).in ).sho cu
)
( Lemma 6 )
In Rep(
h
a, ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,lo okup( ,k),
h
cons(a , lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn ( ,k)
i
),k,cons(ass(a,lo okup ( ,k),
h
cons(a,lo okup( ,k)).key,i
i
),lo ok up( ,k)).in ).s o e
^
pu (con e (
h
a, ,
i
),k,i).sho cu = pu (con e (
h
ass(a,lo oku p( ,k),
h
cons(a, lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassig n( ,k)
i
),k,cons(a,lo okup ( ,k)).in ).sho cu
^
lo okup(deassig n( ,k),k)=unde ned
)
( Lemma 8 )
In Rep(
h
a, ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,lo okup( ,k),
h
cons(a , lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn ( ,k)
i
),k,cons(ass(a,lo okup ( ,k),
h
cons(a,lo okup( ,k)).key,i
i
),lo ok up( ,k)).in ).s o e
^
22
pu (con e (
h
a, ,
i
),k,i).sho cu = pu (con e (
h
ass(a,lo oku p( ,k),
h
cons(a, lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassig n( ,k)
i
),k,cons(a,lo okup ( ,k)).in ).sho cu
^
:
isIn?(con e (
h
ass(a,lo ok up( ,k),
h
cons(a, lo okup( ,k)).key,i
i
), pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
),k)
)
(In Rep(
h
a, ,
i
)
^
lo okup( ,k)
6
=undened ]
)
In Rep(
h
ass(a,lo okup( ,k),
h
cons(a,l o oku p( ,k)) .key,i
i
), pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
))
In Rep(
h
a, ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).sho cu =head(pu Fi s ( , lo okup( ,k))
^
pu (con e (
h
a, ,
i
),k,i).s o e= pu (con e (
h
ass(a,lo okup( ,k),
h
cons(a , lo okup( ,k)).key,i
i
),
pu Fi s ( ,lo okup( ,k)),deassi gn( ,k)
i
),k,cons(as s(a,lo o kup ( ,k),
h
cons(a,lo okup( ,k)).key,i
i
),lo okup ( ,k)).in ).s o e
)
( Abs ac ion Func ion and Lemma 10 )
In Rep(
h
a, ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).s o e= con e (
h
ass(a,lo okup( ,k),
h
cons(a,lo okup ( ,k)).key,i
i
), ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).sho cu =lo okup( ,k)
)
( In Rep(
h
a, ,
i
)
^
lo okup( ,k)
6
=undened ]
)
In Rep(
h
ass(a,lo okup( ,k),
h
cons(a,lo okup( ,k)).key,i
i
), ,
i
))
In Rep(
h
ass(a,lo okup( ,k),
h
cons(a,lo okup ( ,k)).key,i
i
), ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).s o e= con e (
h
ass(a,lo okup( ,k),
h
cons(a,lo okup ( ,k)).key,i
i
), ,
i
)
^
pu (con e (
h
a, ,
i
),k,i).sho cu =lo okup( ,k)
The e o e, om A
2
we can deduce his las asse ion, deno ed A
4
.
By in o ducing hese new asse ions weha e:
unc ion
impl pu (
h
a:a ay :queue : able
i
 k:keyi:in o ma ion)
e u n
hh
a
1
:a ay
1
:queue
1
: able
i
 sc:sho cu
i
P e: In Rep(
h
a, ,
i
)
g
i
lo okup( ,k)=undened
hen
A
1
:In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
g
A
3
g
P
1
else
A
2
:In Rep(
h
a, ,
i
)
^
lo okup( ,k)
6
=undened
g
A
4
g
P
2
end i
Pos : In Rep(
h
a
1
,
1
,
1
i
)
^
con e (
h
a
1
,
1
,
1
i
)=pu (con e (
h
a, ,
i
),k,i).s o e
^
sc=pu (con e (
h
a, ,
i
),k,i).sho cu
g
e u n
hh
a
1
,
1
,
1
i
,sc
i
23
Ha ing hese wo new asse ions i is easy o iden i y,by means o he assignmen ule, which
exp essions should b e assigned o
a
1

1

1
, and
sc
in each case. By doing hese assignmen s we ob ain
he ollowing implemen a ion o he
pu
unc ion:
unc ion
impl pu (
h
a:a ay :queue : able
i
 k:keyi:in o ma ion)
e u n
hh
a
1
:a ay
1
:queue
1
: able
i
 sc:sho cu
i
P e: In Rep(
h
a, ,
i
)
g
i
lo okup( ,k)=undened
hen
A
1
:In Rep(
h
a, ,
i
)
^
lo okup( ,k)=undened
g
A
3
g
a
1
:= ass(a,head( ),
h
k,i
i
)
1
:= dequeue( )
1
:= assign( ,k,head( ))
sc:= head( )
else
A
2
:In Rep(
h
a, ,
i
)
^
lo okup( ,k)
6
=undened
g
A
4
g
a
1
:= ass(a,lo okup( ,k),
h
cons(a,lo okup( ,k)).key,i
i
)
1
:=
1
:=
sc:= lo okup( ,k)
end i
Pos : In Rep(
h
a
1
,
1
,
1
i
)
^
con e (
h
a
1
,
1
,
1
i
)=pu (con e (
h
a, ,
i
),k,i).s o e
^
sc=pu (con e (
h
a, ,
i
),k,i).sho cu
g
e u n
hh
a
1
,
1
,
1
i
,sc
i
24
3.3 Chosing implemen a ions o he comp onen s o he ep esen a ion
Once weha e de i ed he co de o he op e a ions, we s udy wo pa icula implemen a ions o he new
ADT
3
. In b o h o hem we use he dynamic memo y zone as an a ay and he queue o he sys em as
ha o he ee sho cu s. These wo implemen a ions die in he implemen a ion o he able. In he
 s one, weha e used a hashing able wi h chaining. Using a hashing able equi es he pa ame e
KEY
o include also a hashing unc ion. In he second implemen a ion weha e implemen ed he
able wi h an AVL
4
1].
We gi e nex he cos o he op e a ions o he ADT dep ending on he implemen a ion used o
able (see Table 1).
Table 1: The cos o he unc ions
COST
FUNTIONS AVL HASHING
TABLE
c ea e
O
(1)
O
(
)
pu
O
(log
n
)
O
(1)
ge In Key
O
(log
n
)
O
(1)
ge In Sho
O
(1)
O
(1)
ge Key
O
(1)
O
(1)
isIn?
O
(log
n
)
O
(1)
ge Sho cu
O
(log
n
)
O
(1)
isEmp y?
O
(1)
O
(1)
emo e
O
(log
n
)
O
(1)
mo di y
O
(1)
O
(1)
As i can b e seen, he cos o he op e a ions
ge Key
,
ge In Sho
and
modi y
is cons an in b o h
implemen a ions b ecause he able is no accessed, in his case. The cos o he emaining op e a ions
3
See 11] o mo e de ails.
4
An AVL is a bina y sea ch ee whe e he di e ence b e ween he heigh o i s sub ees is less o equal han 1 and he
sub ees a e AVL in u n.
25
14]
Wi h, N.
P og amminginModula-2.
Sp inge -Ve lag, 3 d. edi ion, 1988.
32