Es udio y desa ollo de ´ecnicas pa a
el es ing de p og amas concu en es
Uni e sidad Complu ense de Mad id
Facul ad de In o m´
a ica
T abajo de in de g ado del Doble G ado en
Ma em´
a icas e Ingenie
´
ıa In o m´
a ica
Ma co An onio Ga ido Rojo
Di igido po :
Miguel G´omez-Zamalloa Gil
Cu so 2017-2018
Copy igh c
Ma co An onio Ga ido Rojo
Es e abajo puede encon a se en
h ps://gi hub.com/MaS e e/CABS-Memo ia
bajo licencia MIT.
Resumen
El a ance de los o denado es en las ´ul imas d´ecadas ha b indado la opo unidad a los
desa ollado es de p og amas de ap o echa las en ajas de los p ocesado es mode nos
que pe mi en la ejecuci´on simul ´anea de a ios hilos de ejecuci´on al mismo iempo. Es
po es e mo i o po el que cada ez es m´as com´un el desa ollo de p og amas concu en es
en odos los ´ambi os, desde el so wa e cien ´ı ico has a las aplicaciones m´o iles.
No obs an e, el desa ollo de p og amas concu en es conlle a iesgos adicionales como
deadlocks o condiciones de ca e a no p esen es en los p og amas secuenciales. Es po
ello necesa io el uso de ´ecnicas de alidaci´on como el es ing pa a pode comp oba el
compo amien o de los p og amas y e i ica que cumplen con los equisi os adecuados.
Sin emba go, las ´ecnicas de es ing habi uales no son e ec i as debido al inde e minis-
mo en la ejecuci´on de los p ocesos y una explo aci´on exhaus i a de odos los posibles
en elazamien os suele se in a able po su cos e exponencial. No obs an e, en los sis e-
mas basados en ac o es, debido a la ausencia de memo ia compa ida y la ejecuci´on sin
in e upciones de los p ocesos, el n´ume o de pun os en los que hace al a conside a el
inde e minismo de es os p og amas es mucho meno .
Una de las mejo es ´ecnicas pa a mi iga la explosi´on de es ados es el algo i mo POR
(Pa ial O de Reduc ion), que pe mi e ag upa en clases de equi alencia de i aciones
edundan es, y sob e el que, hoy en d´ıa, se sigue in es igando. Sob e es as l´ıneas en es e
abajo nos cen a emos en el uso de SYCO pa a el es ing de p og amas concu en es.
SYCO es una he amien a pa a ABS, un lenguaje de modelado pa a p og amas concu-
en es basado en el modelo de ac o es, que pe mi e ob ene los posibles es ados inales de
un p og ama concu en e usando el es ado del a e del algo i mo DPOR (Dynamic Pa ial
O de Reduc ion). No obs an e, el p oblema que p esen a ABS es que, como odo lenguaje
de modelado, la implemen aci´on eal de un p og ama dis a mucho de la implemen aci´on
que se pueda hace en es e lenguaje. Adem´as, el modelo de concu encia basado en ac-
o es, pese a es a cob ando cada ez m´as impo ancia, no es el modelo de los lenguajes
m´as popula es como son Ja a y C/C++.
La idea de es e abajo consis e en acili a el uso de las he amien as de es ing implemen-
adas pa a ABS con los p og amas esc i os en C. Pa a ello desa olla emos un lenguaje
con una sin axis simila a C, llamado CABS, que pe mi i ´a la ejecuci´on concu en e de
hilos, usando pa a ello una concu encia de g ano ino.
Abs ac
The ad ance in compu e s du ing he las decades has b ough he oppo uni y o ake
ad an age o he new p ocesso s which a e able o execu e se e al h eads a he same
ime. Tha is he eason why concu en p og ams a e ge ing mo e and mo e common in
a wide a ie y o si ua ions, including, o example, scien i ic so wa e and mobile apps.
Ne e heless, concu en so wa e de elopmen has addi ional isks, such as deadlocks and
da a aces, which a e no p esen in sequen ial p og ams. Tha is why i is necessa y o
use alida ion echniques, such as so wa e es ing, in o de o check he beha io o hese
p og ams and hei equi emen s.
Howe e , he usual echniques a e no e ec i e due o he nonde e minis ic beha io o
hese p og ams and ying o sea ch all he possible in e lea ings is an in ac able p oblem
due o i s exponen ial cos . Howe e , in he ac o model pa adigm, due o he absence o
sha e memo y and he non-p eemp i e scheduling, he numbe o in e lea ings is much
lowe .
One o he bes echniques o a oiding he s a e explosion is he Pa ial O de Reduc ion
(POR) algo i hm. This algo i hm can me ge se e al edundan de i a ion in o he same
equi alence class. Nowadays, some esea che s a e s ill wo king on his. In his hesis, we
will use a speci ic implemen a ion o his echnique, called SYCO.
SYCO is a so wa e ool de eloped o ABS, a modeling language o concu en p og am-
ming based on he ac o model. Using his ool, we can ob ain he possible inal s a es o
a concu en p og am using he s a e o he a in he Dynamic Pa ial O de Reduc ion
(DPOR) algo i hm. Howe e , ABS implemen a ions a e a away om a eal implemen-
a ion o he inal p og am in one o he main languages, such as Ja a o C/C++. In
addi ion, ac o model concu ency is no he pa adigm used in hose languages.
The idea o his hesis is o de elop a p og amming language, simila o C, wi h a ine-
g ain concu ency suppo and o make easie he use o he ools de eloped o ABS in
C p og ams. The name o his language is CABS. (Did you ca ch he joke?)

Palab as cla e
ABS
SYCO
P og amas concu en es
Sem´an icas
Lenguaje de p og amaci´on
In e lea ings
Tes ing de p og amas
Modelo de concu encia basado en ac o es
CUP
JLEX
Keywo ds
ABS
SYCO
Concu en p og amming
Seman ics
P og amming languages
In e lea ings
So wa e es ing
Ac o model concu ency
CUP
JLEX
16 CAP´
ITULO 1. INTRODUCCI ´
ON
algo m´as in e esan e. Es e concep o es conocido como paso de mensajes.
Cada hilo de ejecuci´on aho a pod ´a en un momen o dado escucha el canal o esc ibi
en ´el y modi ica su compo amien o seg´un los mensajes que eciba. Seguimos po an o
con ando con los mismos p oblemas de la concu encia educiendo eso s´ı el n´ume o de
in e lea ings a ene en cuen a.
Imaginemos aho a que los mensajes mandados en e obje os son los que p o ocan la eje-
cuci´on de los m´e odos que es os con ienen. Es a es la idea en los modelos de concu encia
basados en ac o es.
En es os modelos, cada obje o ejecu a sus a eas de o ma concu en e con espec o a las
del es o de obje os con la ´unica es icci´on de que cada obje o solo puede ejecu a una
´unica a ea a la ez. El es o de a eas espe an en una cola cuyo o den en p incipio no es
de e minable. El paso de mensajes indica qu´e m´e odo desea ejecu a un obje o (pudiendo
se uno p opio o pe enecien e a o o obje o) y, dependiendo del ipo de llamada, una
a ea puede deja paso a o a si a´un no cuen a con los alo es necesa ios pa a p osegui .
Se a a de una concu encia donde el schedule o plani icado no puede desasigna a una
a ea den o de un obje o si es a no ha e minado o si no ha llegado a un pun o de espe a,
uncionando cada obje o como una especie de moni o . Es o es lo que se conoce como un
modelo non-p eemp i e.
Al igual que como hemos comen ado an e io men e, al in oduci los modelos de paso de
mensajes, el modelo de ac o es ambi´en educe no ablemen e el n´ume o de in e lea ings
a ene en cuen a. Es o es de i al impo ancia cuando se in en an aplica ´ecnicas de
es ing sis em´a ico en las que se deben de ene en cuen a odos los en elazamien os
posibles y donde hay que ene muy en cuen a la explosi´on de es ados, que hace que sean
in a ables en los casos gene ales. Pa a es os m´e odos de explo aci´on sis em´a ica se puede
supone que odas las ins ucciones de una a ea se ejecu an una de ´as de o a sin ning´un
en elazamien o has a que no se llega al inal de la unci´on en un e u n.
En es e ipo de concu encia se basan muchos lenguajes de p og amaci´on como po ejem-
plo E lang y Scala, adem´as de ABS, el que a a se nues o compa˜ne o de iaje en es e
abajo.
La mo i aci´on de es e abajo es la c eaci´on de un lenguaje de p og amaci´on b´asico, lla-
mado CABS, que pe mi a ec ea una concu encia en e p ocesos a ni el de g ano ino y
sob e el que podamos emplea las po en es he amien as ya elabo adas pa a el lenguaje
ABS en la ma e ia del an´alisis de p og amas concu en es. CABS se ´a un lenguaje de p o-
g amaci´on con una sin axis pa ecida a la de C con ipado es ic o y es ´a ico, que incluye la
posibilidad de usa unciones y a ays y que se mue e en el pa adigma de la p og amaci´on
impe a i a.
Sob e es a em´a ica se han hecho ya abajos simila es de c eaci´on de lenguajes o compi-
lado es como en [1]. En dicho abajo, se abo d´o la de ecci´on de deadlocks en un lenguaje
b´asico que con aba con p imi i as pa a decla a p ocesos y ce ojos y que empleaba la

17
he amien a SACO desa ollada pa a ABS sob e una aducci´on o mal. De un modo
simila , en nues o abajo emplea emos las mismas ´ecnicas o males sob e sem´an icas
pa a demos a que la aducci´on que se p opond ´a pa a CABS en e ec o cumple con la
p ese aci´on de odos los in e lea ings posibles y que, po an o, los es ados inales alcan-
zables ejecu ando CABS con su sem´an ica son los mismos que ob end ´ıamos con ABS. A
di e encia de [1], nues o abajo p e ende llega a desa olla un lenguaje de p og ama-
ci´on Tu ing comple o sob e el que se puedan implemen a algo i mos y no es ingi nos a
c ea una demos aci´on me amen e acad´emica sob e la posibilidad de ob ene los en e-
lazamien os en un lenguaje de p ueba.
De un modo simila al que se p e ende hace con CABS, en los a˜nos 80 se c eo SPIN 1.
SPIN es una he amien a de e i icaci´on de sis emas dis ibuidos desa ollada po Ge a d
J. Holzmann que abajaba sob e modelos esc i os en P omela 2, un lenguaje de modela-
do, que e a aducido a C. E a sob e el c´odigo en C donde se empleaban dis in as ´ecnicas
de e i icaci´on, en e las que se inclu´ıa el uso de Pa ial O de Reduc ion (POR). En es e
aspec o, noso os pod emos ap o echa la he amien a SYCO, disponible pa a ABS y que
implemen a ´ecnicas a anzadas de Dynamic Pa ial O de Reduc ion (DPOR). Sob e es-
a he amien a dedica emos un cap´ı ulo comple o al inal de es e abajo. El obje i o de
DPOR es consegui educi el n´ume o de es ados de explo aci´on necesa ios pa a conoce
los posibles esul ados inales de un p og ama. Como hemos is o en los ejemplos an e io-
es, exis en ocasiones en que el o den en la ejecuci´on de dos ins ucciones pe enecien es a
p ocesos dis in os no in luye en el esul ado inal del p og ama y es en es e aspec o donde
DPOR consigue de e mina que o denes son edundan es pa a in en a sal a la explosi´on
exponencial de es ados in e medios.
En un ´ambi o m´as gene al podemos encon a in es igaciones como en [2], donde el uso
de es as ´ecnicas se emplea pa a el an´alisis de Redes de inidas po so wa e o SDN po
sus siglas en ingl´es. SDN es un pa adigma sob e la a qui ec u a de edes que pe mi e un
con ol sob e el compo amien o de las mismas. En [2] se es ablece una elaci´on o mal
en e las SDN y el modelo de ac o es pa a la e i icaci´on de so wa e dis ibuido, eali-
zando una especi icaci´on en ABS.
Como hemos podido e , el e eno de la e i icaci´on o mal de p og amas concu en es
p esen a ejemplos simila es a los que in en a emos acome e en es e abajo que di i-
di emos en a ios cap´ı ulos, cada uno de ellos cen ado en un aspec o conc e o. En los
siguien es cap´ı ulos desc ibi emos la sin axis y sem´an ica de nues o lenguaje as´ı como
la del lenguaje ABS sob e el que ealiza emos la aducci´on de CABS. Pos e io men e se
demos a ´a la idea de la co ecci´on de la aducci´on, lo que nos pe mi i ´a ex apola las
p opiedades del c´odigo ABS aducido al c´odigo o iginal en CABS. En e es as p opie-
dades pueden encon a se las esul an es del uso de he amien as o males desa olladas
sob e ABS. T as oda la o malizaci´on, habla emos de la implemen aci´on de la aduc-
ci´on p opues a en un compilado de CABS a ABS, que desa olla emos en Ja a usando
JLex y CUP, he amien as empleadas en la asigna u a de P ocesado es de Lenguaje. Po
´ul imo, habla emos de la aplicaci´on p incipal del compilado de CABS que es el uso de la
1h ps://en.wikipedia.o g/wiki/SPIN_model_checke
2h ps://en.wikipedia.o g/wiki/P omela
18 CAP´
ITULO 1. INTRODUCCI ´
ON
he amien a SYCO pa a ob ene odos los posibles esul ados inales de la ejecuci´on de
un p og ama concu en e ap o echando el s a e o he a en DPOR.
¡Comencemos!
Cap´ı ulo 2
Sin axis y sem´an ica
2.1. Sin axis de CABS
La mayo ´ıa de lenguajes de p og amaci´on del me cado siguen una sin axis com´un simila
a la que iene el lenguaje o iginal en el que se suelen basa que es C. A la ho a de de ini
la sin axis de CABS oma emos como e e encia de nue o la de ese lenguaje.
Pa a sen a las bases de la no aci´on que se usa ´a de aho a en adelan e pa a de ini la
sem´an ica de nues o lenguaje, di emos que Pes un p og ama en CABS o mado po ins-
ucciones globales como lo son las decla aciones de a iables globales y las decla aciones
de unciones.
La decla aci´on de a iables cons a ´a de un ipo y de un nomb e de a iable seguido de
un pun o y coma. Las unciones es a ´an o madas po un ipo de e o no, un nomb e de
unci´on, una lis a de a gumen os (es posible que sea ac´ıa), un cue po con ins ucciones
S∈S m y una exp esi´on de e o no. A modo de ilus aci´on podemos e el siguien e
c´odigo
1 ype global_ a 1 ;
2 ype global_ a 2 ;
3
4 ype nomb e_de_ uncion (a gs ...) {
5...
6codigo
7...
8 e u n exp
9}
donde se mues a la decla aci´on de dos a iables globales y de una unci´on.
Los ipos que maneja emos en nues o lenguaje se ´an en e os y booleanos, cuyos iden i-
icado es se ´an in ybool espec i amen e. Pe mi i emos adem´as la decla aci´on y el uso
de a ays de en e os y booleanos en asignaciones y exp esiones a i m´e ico-l´ogicas y como
a gumen os de unciones. No se pod ´an usa como ipo de e o no. Un ejemplo del uso de
a ays es el siguien e:
19
20 CAP´
ITULO 2. SINTAXIS Y SEM ´
ANTICA
1in a ay [10]; # A ay global con 10 en e os
2in global_ a ; # A en u amos que ald a 27, pe o eso
depende a de la seman ica :)
3
4in (in es , in a [10]) {
5in a ;
6 a = 2 * es + a [1];
7 e u n a ;
8}
9
10 in main () {
11 a ay [0] = 10;
12 a ay [1] = 5;
13 in es;
14 es = a ay [0] + 1;
15 global_ a = ( es , a ay);
16 e u n 0;
17 }
Las ins ucciones Sdel cue po de una unci´on de un p og ama son las ´ıpicas de un len-
guaje impe a i o, en e las que se encuen an las asignaciones, las ope aciones a i m´e ico-
l´ogicas, las ins ucciones de con ol, como los condicionales y los bucles y, la cla e de un
lenguaje con concu encia, un h ead pa a la ejecuci´on de unciones en pa alelo imi ando
el compo amien o de la lib e ´ıa p h ead en C. Veamos un ejemplo que use es a ´ul ima
cons ucci´on:
1in a ;
2
3in main () {
4 h ead (1);
5 h ead (2);
6 e u n 0;
7}
8
9 oid (in alue ) {
10 a = alue ;
11 }
Como podemos e , las llamadas concu en es son simila es a las llamadas a p ocedimien-
os habi uales p ecedidas po la palab a ese ada h ead.
2.2. Sem´an ica de CABS
A con inuaci´on pasamos a habla de la sem´an ica del lenguaje CABS. La idea es da
un signi icado al c´odigo CABS de modo que quede de inido el compo amien o de cada
una de las cons ucciones p esen es en el lenguaje. Pa a es e p op´osi o escoge emos una
sem´an ica de paso co o en la que la de i aci´on se puede in e p e a como una secuencia
2.2. SEM ´
ANTICA DE CABS 21
de pasos que simulan las ansiciones que gene a ´ıa un c´odigo ejecu ado en un o denado
eal, es deci , los cambios en memo ia y en la ins ucci´on ac ual ma cada po un con ado
de p og ama.
En una p ime a secci´on da emos las de iniciones b´asicas de lo que se ´an los es ados de
nues o p og ama pa a, pos e io men e, especi ica cuales se ´an las eglas que ma ca ´an
las ansiciones en e ellos. Po ´ul imo, mos a emos algunos ejemplos de de i aci´on a
pa i de unos p og amas b´asicos.
2.2.1. P e´ambulo sem´an ico
Los p og amas en CABS se pueden en ende , de o ma simpli icada, como unas secuencias
de pasos que an a maneja unos alo es en e os y l´ogicos posiblemen e almacenados en
una memo ia donde ambi´en se gua da ´an los esul ados desp endidos de las ope aciones
que se ealicen. Es po es o que en p ime luga enemos que de ini un conjun o de alo es
V=Z∪Bque sea la uni´on de los en e os y de los booleanos, los elemen os b´asicos de
odo p og ama.
Una p ime a pa e de la ep esen aci´on del es ado es a ´a o mada po las a iables glo-
bales de nues o p og ama. De inimos G=Va ,→Vel conjun o de unciones pa ciales
del conjun o de a iables al conjun o de alo es. El es ado ac ual de nues as a iables
globales se ´a una unci´on de es e conjun o y po lo gene al nos e e i emos a ella con
la le a G. Pos e io men e cuando hablemos de a iables locales ambi´en las de ini emos
como un conjun o de unciones simila es pe o que a a emos po sepa ado po comodi-
dad. El conjun o Va con iene odos los nomb e de a iable posibles y usa emos G a
pa a e e i nos al alo almacenado po la a iable global a . Po se una unci´on pa -
cial quedan e lejadas en G´unicamen e las a iables que han sido p e iamen e decla adas.
Po o o lado nos encon amos en nues o lenguaje con la necesidad de de ini un con-
jun o que ecoja la in o maci´on b´asica de las unciones y p ocedimien os. De inimos
F=Func ,→(T×S m ×A gs ×(Exp ∪ {ε})) el conjun o de unciones pa ciales
que asocia un nomb e de unci´on a su de inici´on. Una unci´on queda ´a de inida po su
ipo de e o no ∈T, su c´odigo S∈S m, sus a gumen os de en ada a g ∈A gs y
su exp esi´on de e o no e∈Exp ∪ {ε}. Seg´un las necesidades, la exp esi´on de e o no
se ´a una exp esi´on booleana, una exp esi´on a i m´e ica o simplemen e se ´a la exp esi´on
ac´ıa, empleada pa a los p ocedimien os. De nue o enemos un conjun o de nomb es de
unciones Func. En p incipio los nomb es de a iable y de unci´on son los mismos en
los lenguajes de p og amaci´on habi uales y es ambi´en el caso de CABS, no obs an e,
po simplicidad, conside a emos en la sem´an ica que son conjun os sepa ados. A su ez,
con amos ambi´en con la en aja de las unciones pa ciales en Fque solo end ´an la in o -
maci´on de aquellas unciones que en e dad hayan sido de inidas en el p og ama. Fse ´a
la me a a iable que usa emos pa a e e i nos a una unci´on de Fconc e a.
Pa a da un signi icado a nues os p og amas enemos que de ini qu´e a a ep esen a pa-
a noso os su es ado de ejecuci´on. De inimos el conjun o de es ados S a e =G×F×RP
como una upla que ecoja la in o maci´on de las a iables globales y de las unciones

22 CAP´
ITULO 2. SINTAXIS Y SEM ´
ANTICA
de inidas en nues o p og ama P, as´ı como, una lis a de ma cos de ejecuci´on o un ime
p ocesses que con end ´a la in o maci´on local de los p ocesos. Es o ´ul imo queda ´a ecogido
en los elemen os de RP = ((Loc)+×S m)∗donde Loc =Va ,→Vse ´a el conjun o de
´ambi os locales. Po lo gene al usa emos la no aci´on local :s∈(Loc)+pa a e e i nos a la
pila de llamadas de un p oceso, donde local ∈Loc ys∈(Loc)∗, emulando la no aci´on de
lis a de un lenguaje uncional como Haskell. Usa emos adem´as la me a a iable RP pa a
e e i nos a una lis a de ma cos de ejecuci´on conc e a y el ope ado ;pa a e e i nos a
un elemen o de la lis a cualquie a, de modo que, RP ;(local :s, S) indica que la lis a de
ma cos RP con iene en conc e o el ma co (local :s, S) donde Ses el c´odigo del p oceso
y (local :s) su pila de ´ambi os locales.
La idea a segui pa a de ini nues a sem´an ica se ´a apoya nos en dos unciones auxilia es
ini ys a que espec i amen e inicializa ´an el es ado global del p og ama y lanza ´an a
ejecuci´on la unci´on inicial main, bas´andonos en la de inici´on que hemos dado de es ado.
La unci´on ini .
De inimos la unci´on ini :P og ,→S a e de o ma ecu si a del siguien e modo.
ini (ε)=(nil,nil,[])
ini (in a ; P)=(G[ a 7→ 0] ,F,RP) donde ini (P) = (G,F,RP)
ini (bool a ; P)=(G[ a 7→ FALSE],F,RP) donde ini (P) = (G,F,RP)
ini (in unc(a g){S; e u n a}P)=(G,F[ unc 7→ (in , S, a g, a)] ,RP)
donde ini (P) = (G,F,RP)
ini (bool unc(a g){S; e u n b}P)=(G,F[ unc 7→ (bool, S, a g, b)] ,RP)
donde ini (P) = (G,F,RP)
ini ( oid unc(a g){S}P)=(G,F[ unc 7→ ( oid, S, a g, ε)] ,RP)
donde ini (P) = (G,F,RP)
Con es a unci´on conseguimos c ea el ´ambi o global de a iables y de unciones de nues os
p og amas en CABS. Hemos usado la no aci´on [x7→ alue] pa a indica que el alo de
una unci´on en xes sus i uido po el nue o alo alue. Es a no aci´on se segui ´a usando
m´as adelan e.
La unci´on ( egla) s a .
De inimos la unci´on s a :S a e ,→S a e como
s a ((G,F,RP)) = (G,F,[(nil : [], S)]) donde F(main)=(in , S, a g,0)
Con es o conseguimos c ea un nue o ma co de ejecuci´on con el c´odigo inicial de main.
N´o ese que la unci´on inicializa la pila de ´ambi os de a iables locales con el ´ambi o nil
que no con iene ninguna a iable inicializada.
2.2. SEM ´
ANTICA DE CABS 23
Sem´an ica (Exp esiones a i m´e ico-l´ogicas).
Las p ime as eglas que que emos de ini se ´an las de las exp esiones a i m´e ico-l´ogicas.
Nues o lenguaje pe mi e la llamada a unciones con alo de e o no, lo que hace que
engamos que, desde un p incipio, maneja unas eglas que ga an icen la no e minaci´on
de la e aluaci´on de las exp esiones. Se ´a po ello que engamos que da una de inici´on de
una unci´on pa cial que dada una exp esi´on nos de uel a o a exp esi´on m´as simpli icada,
pudiendo emplea el es ado del p og ama pa a ello y pe mi iendo modi icaciones del mis-
mo, has a e en ualmen e queda nos con un alo ∈V, lo que conside amos la exp esi´on
m´as simpli icada.
Empecemos po da una de inici´on en el caso de las exp esiones en e as. De aho a en ade-
lan e nos e e imos po el conjun o Aexp a la uni´on de exp esiones a i m´e icas y alo es
en e os.
Buscamos de ini la unci´on sem´an ica A: (Aexp×S a e),→(Aexp ×S a e) median e
las siguien es eglas:
24 CAP´
ITULO 2. SINTAXIS Y SEM ´
ANTICA
[numA]hn, (G,F,RP ;(s, S))i →Aexp hN JnK,(G,F,RP ;(s, S))i
local(x) =
 a L
Ahx, (G,F,RP ;(local :s, S))i →Aexp h , (G,F,RP ;(local :s, S))i
G(x) = local(x) = unde
 a G
Ahx, (G,F,RP ;(local :s, S))i →Aexp h , (G,F,RP ;(local :s, S))i
donde xes a iable en e a.
ha1,(G,F,RP ;(s, S))i →Aexp ha0
1,(G,F,RP ;(s0, S0))i
J1
Aha1Ja2,(G,F,RP ;(s, S))i →Aexp ha0
1Ja2,(G,F,RP ;(s0, S0))i
ha2,(G,F,RP ;(s, S)))i →Aexp ha0
2,(G,F,RP ;(s0, S0)))i
J2
Ah Ja2,(G,F,RP ;(s, S)))i →Aexp h Ja0
2,(G,F,RP ;(s0, S0)))i
J3
Ah 1J 2,(G,F,RP ;(s, S))i →Aexp h 1JN 2,(G,F,RP ;(s, S))i
donde Jes alguno de los ope ado es del lenguaje que ienen su hom´ologo sem´an ico JN.
ha, (G,F,RP ;(s, S))i →Aexp ha0,(G,F,RP ;(s0, S0))i
uns ack1
AhUNSTACK (a),(G,F,RP ;(s, S))i →Aexp hUNSTACK (a0),(G,F,RP ;(s0, S0))i
uns ack2
AhUNSTACK ( ),(G,F,RP ;(local :s, S))i →Aexp h , (G,F,RP ;(s, S))i
F( unc) = (in , SF, a gsF, a)check a gs(a gsF, a gs)e al(a gs) = a gs0
call1
Ah unc(a gs),(G,F,RP ;(local :s, S))i →Aexp h unc(a gs0),(G,F,RP ;(local :s, S))i
2.2. SEM ´
ANTICA DE CABS 25
F( unc) = (in , SF, a gsF, a)check a gs(a gsF, a gs)e al(a gs) = 1:· · · : n
call2
Ah unc(a gs),(G,F,RP ;(local :s, S))i →Aexp hUNSTACK (a),(G,F,RP ;(nil [a gs 7→ 1:· · · : n] : local :s, SF;S))i
donde check a gs es una unci´on auxilia que comp ueba la co ecci´on de ipos y el n´ume o de a gumen os y donde e al indica que
los a gumen os de la unci´on son e aluados has a consegui los alo es de V inales, haciendo uso de las eglas de la sem´an ica de
exp esiones. De es e modo se jus i ica que pa a ejecu a una unci´on sea necesa io e alua uno a uno los a gumen os de la unci´on.
De hecho, e al puede hace uso de las eglas pa a exp esiones booleanas en el caso de las unciones con pa ´ame os mix os. Dichas
eglas son las que de inen B: (Bexp ×S a e),→(Bexp ×S a e).
[T ueB]h ue, (G,F,RP ;(s, S))i →Bexp h ue,(G,F,RP ;(s, S))i
[FalseB]h alse, (G,F,RP ;(s, S))i →Bexp h alse,(G,F,RP ;(s, S))i
local(x) =
 a L
Bhx, (G,F,RP ;(local :s, S))i →Bexp h , (G,F,RP ;(local :s, S))i
G(x) = local(x) = unde
 a G
Bhx, (G,F,RP ;(local :s, S))i →Aexp h , (G,F,RP ;(local :s, S))i
donde xes una a iable booleana.
hb1,(G,F,RP ;(s, S))i →Bexp hb0
1,(G,F,RP ;(s0, S0))i
J1
Bhb1Jb2,(G,F,RP ;(s, S))i →Bexp hb0
1Jb2,(G,F,RP ;(s0, S0))i
hb2,(G,F,RP ;(s, S)))i →Bexp hb0
2,(G,F,RP ;(s0, S0)))i
J2
Bh Jb2,(G,F,RP ;(s, S)))i →Bexp h Jb0
2,(G,F,RP ;(s0, S0)))i
J3
Bh 1J 2,(G,F,RP ;(s, S))i →Bexp h 1JB 2,(G,F,RP ;(s, S))i
32 CAP´
ITULO 3. ABS: SINTAXIS Y SEM ´
ANTICA
donde los a gumen os son una lis a sepa ada po comas de ce o o m´as nomb es de a ia-
bles p ecedidos de su ipo (al es ilo de Ja a).
De los ipos p ede inidos en ABS solo usa emos los en e os (In ) y los booleanos (Bool).
Tambi´en emplea emos el ipo gen´e ico Lis pa a la cons ucci´on de A ays.
La decla aci´on de clases en ABS es simila a la de Ja a con la peculia idad de que odas
las clases de inidas po el usua io deben implemen a una in e az. La sin axis pa a la
de inici´on de clases en ABS es
1class nomb e_de_clase ( a gs) implemen s nomb e_de_in e az {
2...
3decla aciones de a ibu os p i ados
4...
5...
6implemen aciones
7...
8}
La decla aci´on de a ibu os de una clase es id´en ica a la de Ja a, con la ausencia de las
palab as ese adas p i a e,public op o ec ed. La isibilidad de odos los a ibu os es
p i ada. Del mismo modo, las implemen aciones de m´e odos siguen el mismo es ilo. Un
m´e odo es po an o p´ublico si es ´a de inido en la in e az que implemen a la clase, en
caso con a io es p i ado.
Una ca ac e ´ıs ica especial de las clases de ABS es la posibilidad de de ini las con una lis a
de a gumen os accesibles desde cualquie pun o de la clase. Es a p opiedad se ´a amplia-
men e explo ada con pos e io idad pa a la implemen aci´on del concep o de a iable global.
Po ´ul imo, nos queda discu i las llamadas a m´e odos de una clase. En ABS, las llamadas
a m´e odos son un paso de mensaje, es deci , cuando un obje o llama a un m´e odo de o o
obje o o de s´ı mismo, dicha llamada se me e en una cola a la espe a de pode se eje-
cu ada po el obje o ecep o . Un obje o (o ac o ) solo puede ejecu a un mensaje a la ez.
De los ope ado es de llamada a m´e odos de ABS, noso os solo nos p eocupa emos del
ope ado ‘!’, cuya sin axis es
1Fu < _ e > e = o! (a gs );
La idea de es a llamada es manda un mensaje al obje o opa a que ejecu e su m´e odo
. Es a llamada de uel e un ipo u u o. El ipo u u o pe mi e en e o as cosas sabe
cuando se ha concluido la ejecuci´on del mensaje y en es e caso ecupe a el alo de e-
o no del m´e odo.
Cuando que amos ealiza una llamada s´ınc ona, es deci , una llamada pa a la que no
deseamos con inua la ejecuci´on de un mensaje an es de conoce el alo de e o no del
m´e odo llamado, emplea emos un awai . La idea del awai es pa aliza la ejecuci´on del
mensaje ac ual, pe mi iendo a o os mensajes del obje o se ejecu ados, y espe a a que

3.2. SEM ´
ANTICA 33
la a iable u u a de la llamada enga un alo , es deci , que la llamada haya concluido.
La cons ucci´on awai iene la siguien e sin axis
1awai o! ( a gs);
y su ipo de e o no es el mismo que el del m´e odo de la llamada.
El es o de la sin axis de ABS empleada en es e abajo se educe al uso de los i /else y
del while, as´ı como de la decla aci´on de a iables locales en los m´e odos y de asignaciones
a a iables de los esul ados de la e aluaci´on de exp esiones a i m´e ico-l´ogicas. La sin axis
e e en e a es as cons ucciones del lenguaje son p ´ac icamen e simila es a las de Ja a.
El concep o de unci´on main en ABS lo cumple un conjun o de ins ucciones ABS esc i as
en e lla es y si uadas al inal del a chi o del c´odigo.
3.2. Sem´an ica
De o ma simila al desa ollo expues o pa a CABS, en es a secci´on segui emos unos pasos
simila es pa a de ini la sem´an ica del lenguaje ABS.
Un es ado de un p og ama en ABS end ´a ep esen ado po los obje os c eados en ejecu-
ci´on y po la in o maci´on es ´a ica apo ada po las clases e in e aces, es deci , el c´odigo
de la implemen aci´on de los m´e odos, an o p´ublicos como p i ados, y la inicializaci´on
de los a ibu os. Po an o de inimos S a eABS como uplas (O,C) donde el elemen o O
se ´a una lis a de obje os ins anciados y Ccon end ´a la de inici´on de las clases e in e aces.
Es e ´ul imo elemen o se ´a una lis a de de iniciones indexada po un iden i icado de clase.
Con end ´a elemen os de la o ma (In e , a c, me , a gsc) donde, en o den de izquie da a
de echa, se iene el nomb e de in e az que implemen a una clase, los a ibu os o ields de
la clase, los m´e odos que implemen a jun o con su de inici´on (es deci , c´odigo y a gumen-
os) y los a gumen os de clase.
Un obje o end ´a dado a su ez po un iden i icado ´unico o, su nomb e de clase, una
cola de mensajes a la que llama emos RT (Run ime asks), un iden i icado de a ea que
indique que mensaje es ´a p ocesando el obje o en ese ins an e y la in o maci´on del es ado
de los a ibu os median e a :Va ,→VABS, una unci´on que asigne a un nomb e de
a iable un alo de ABS. Pues o que los iden i icado es de obje os pueden eni dados
po un n´ume o en Z, se puede e que VABS es en esencia el mismo conjun o de alo es
que hemos de inido pa a CABS. Po comodidad escoge emos es a opci´on. Es impo an e
ene es o en cuen a pues o que, si us´a amos o o ipo de iden i icado pa a los obje os,
se ´ıa necesa io de ini el conjun o de alo es de ABS de o o modo y hab ´ıa de ene se
en cuen a en el es o de a gumen os o males que lle a emos a cabo que los alo es en
CABS no se ´ıan los mismos que en ABS. El papel de a se ´a el mismo que en´ıan los
elemen os de Loc en la sem´an ica de CABS, pe mi iendo aho a ene obje os a los que
se puede accede usando un nomb e de a iable de Va .
El concep o de a ea ecoge la in o maci´on del ´ambi o local loc :Va ,→VABS, el c´odigo
del m´e odo S∈S mABS y un iden i icado ´unico de a ea. Con es o quedan de inidos
34 CAP´
ITULO 3. ABS: SINTAXIS Y SEM ´
ANTICA
los elemen os RT. No hay que con undi las a iables de ´ambi o local loc, decla adas
den o de un m´e odo, con los a ibu os del obje o a que son un a˜nadido al con a con
o ien aci´on a obje os.
Con es as de iniciones b´asicas p ocedemos a da una de inici´on o mal de la sem´an ica de
ABS.
3.2. SEM ´
ANTICA 35
3.2.1. Reglas de de i aci´on en ABS
is local(x)is In (x)
[ass1
ABS]
(O;(id, c, RT ;(loc, x =a;S, ), , a ),C)→(O;(id, c, RT ;(loc hx7→ A JaKloc,a i, S, ), , a ),C)
is a (x)is In (x)
[ass2
ABS]
(O;(id, c, RT ;(loc, x =a;S, ), , a ),C)→(O;(id, c, RT ;(loc, S, ), , a hx7→ A JaKloc,a i),C)
Declin
ABS(O;(id, c, RT ;(loc, In x =a;S, ), , a ),C)→(O;(id, c, RT ;(loc hx7→ A JaKloc,a i, S, ), , a ),C)
is local(x)is Bool(x)
[ass3
ABS]
(O;(id, c, RT ;(loc, x =b;S, ), , a ),C)→(O;(id, c, RT ;(loc hx7→ B JbKloc,a i, S, ), , a ),C)
is a (x)is Bool(x)
[ass4
ABS]
(O;(id, c, RT ;(loc, x =b;S, ), , a ),C)→(O;(id, c, RT ;(loc, S, ), , a hx7→ B JbKloc,a i),C)
Declbool
ABS(O;(id, c, RT ;(loc, Bool x =b;S, ), , a ),C)→(O;(id, c, RT ;(loc hx7→ B JbKloc,a i, S, ), , a ),C)
BJbKloc,a =TRUE
i TRUE
ABS (O;(id, c, RT ;(loc, i (b){S1}else{S2}S, ), , a ),C)→(O;(id, c, RT ;(loc, S1S, ), , a ),C)
BJbKloc,a =FALSE
i FALSE
ABS (O;(id, c, RT ;(loc, i (b){S1}else{S2}S, ), , a ),C)→(O;(id, c, RT ;(loc, S2S, ), , a ),C)
36 CAP´
ITULO 3. ABS: SINTAXIS Y SEM ´
ANTICA
[whileABS](O;(id, c, RT ;(loc, while(b){S1}S, ), , a ),C)→(O;(id, c, RT ;(loc, i (b){S1while(b){S1}}S, ), , a ),C)
CJc0K= (In e , a c, me , a gsc)check a gs(a gsc, a gs)
[objABS](O;(id, c, RT ;(loc, In e in e =new c0(a gs); S, ), , a ),C)→(O:o;(id, c, RT ;(loc [in e 7→ id0], S, ), , a ),C)
donde o= (id0, c0,[],⊥,a 0) con id0un nue o iden i icado de obje o no u ilizado y a 0=a cha gsc7→ E Ja gsKloc,a ilos
a ibu os del nue o obje o c eado. La unci´on Ee al´ua los a gumen os escogiendo en e AyBseg´un sea un en e o o un booleano.
loc ∪a Jin e K=id0CJc0K= (In e , a c, me , a gsc)con ains(me , m)check a gs(a gsm, a gs)
 skASYNC
ABS (O;(id0, c0,RT0, 0,a 0)(id, c, RT ;(loc, in e !m(a gs); S, ), , a ),C)→s
donde sk = (loc0, S0, 00) con 00 un iden i icado de a ea nue o, loc0=nil [a gsm7→ a gs] y me JmK= (S0, a gsm) y el nue o
es ado s = (O;(id0, c0,RT0: sk, 0,a 0)(id, c, RT ;(loc, S, ), , a ),C)
loc ∪a Jin K=id0CJc0K= (In e , a c, me , a gsc)con ains(me , m)check a gs(a gsm, a gs)
 skSYNC
ABS1(O;(id0, c0,RT0, 0,a 0)(id, c, RT ;(loc, In x =awai in !m(a gs); S, ), , a ),C)→s
donde o0= (id0, c0,RT0: sk, 0,a 0), sk = (loc0, S0, 00) con 00 un iden i icado de a ea nue o y loc0=nil [a gsm7→ a gs],
me JmK= (S0, a gsm) y s = (O;o0(id, c, RT ;(loc, In x =awai 0;S, ), , a ),C)
loc ∪a Jin K=id0CJc0K= (In e , a c, me , a gsc)con ains(me , m)check a gs(a gsm, a gs)
 skSYNC
ABS2(O;(id0, c0,RT0, 0,a 0)(id, c, RT ;(loc, awai in !m(a gs); S, ), , a ),C)→s
donde o0= (id0, c0,RT0: sk, 0,a 0), sk = (loc0, S0, 00) con 00 un iden i icado de a ea nue o y loc0=nil [a gsm7→ a gs],
me JmK= (S0, a gsm) y s = (O;o0(id, c, RT ;(loc, awai 0;S, ), , a ),C)
sk = (loc0, ε(ν), 00)
[ e 1
ABS](O;(id0, c0,RT0; sk, 0,a 0)(id, c, RT ;(loc, In x =awai 0;S, ), , a ),C)→s
donde o0= (id0, c0,RT0, 0,a 0) y s = (O;o0(id, c, RT ;(loc [x7→ ν], S, ), , a ),C)
3.2. SEM ´
ANTICA 37
sk = (loc0, ε(ν), 00)
[ e 2
ABS](O;(id0, c0,RT0; sk, 0,a 0)(id, c, RT ;(loc, awai 0;S, ), , a ),C)→(O;o0(id, c, RT ;(loc, S, ), , a ),C)
donde o0= (id0, c0,RT0, 0,a 0)
sk = (loc0, S, 00)S6=ε(ν)
[wai ABS](O;(id0, c0,RT0; sk, 0,a 0)(id, c, RT ;(loc, In x =awai 0;S, ), , a ),C)→s
donde o0= (id0, c0,RT0, 0,a 0) y s = (O;o0(id, c, RT ;(loc, In x =awai 0;S, ),⊥,a ),C)
[selecABS](O;(id, c, RT ;(loc, S, ),⊥,a ),C)→(O;(id, c, RT ;(loc, S, ), , a ),C)
[endABS](O;(id, c, RT ;(loc, e u n a;S, ), , a ),C)→(O;(id, c, RT ;(loc, ε(AJaKloc,a ), ),⊥,a ),C)
[deselecABS](O;(id, c, RT ;(loc, ε(ν), ), , a ),C)→(O;(id, c, RT ;(loc, ε(ν), ),⊥,a ),C)

38 CAP´
ITULO 3. ABS: SINTAXIS Y SEM ´
ANTICA
3.3. Ex ensi´on sem´an ica y sin ´ac ica
Adem´as de las de iniciones an e io es asociadas al lenguaje ABS, puede esul a in e e-
san e a˜nadi una se ie de es uc u as auxilia es a modo de az´uca sin ´ac ico que puedan
acili a nos el camino en los siguien es cap´ı ulos de es e abajo. Es po ello po lo que
hemos in oducido en la sem´an ica la no aci´on awai pa a indica que espe amos a que
e mine la a ea con iden i icado y que ecupe amos su alo de e o no. Es e ipo de
cons ucci´on y o as m´as pueden no exis i en el lenguaje o iginal ABS, pe o noso os
ha emos uso de ellas como me a no aci´on pa a exp esa el signi icado del es o de cons-
ucciones s´ı p esen es en el lenguaje.
3.4. Ejemplos
Sea el c´odigo en ABS
1module Cabs;
2impo * om ABS . S dLib ;
3
4in e ace GLOBAL {
5In ge a ();
6Uni se a (In al );
7}
8class GlobalVa iables () implemen s GLOBAL {
9In a = 0;
10
11 In ge a () {
12 e u n a ;
13 }
14
15 Uni se a (In al ) {
16 a = al ;
17 }
18 }
19
20 in e ace In {
21 Uni (In alue);
22 }
23
24 in e ace In main {
25 In main ();
26 }
27
28 class Imp ( GLOBAL global al ) implemen s In {
29 Uni ( In alue ) {
30 awai global al ! se a ( alue );
3.4. EJEMPLOS 39
31 }
32 }
33
34 class Impmain ( GLOBAL global al ) implemen s In main {
35 In main () {
36 In unc 1 = new Imp ( global al );
37 unc 1 ! (1);
38
39 In unc 2 = new Imp ( global al );
40 unc 2 ! (2);
41
42 e u n 0;
43 }
44 }
45
46 {
47 GLOBAL global al = new GlobalVa iables ();
48 In main p og = new Impmain ( global al );
49 awai p og !main ();
50 }
T as ejecu a el c´odigo de inicializaci´on, en el que c eamos el obje o globa al e ins an-
ciamos un obje o que con iene la implemen aci´on de main a la que llamamos con la
ins ucci´on awai p og!main(); , nos encon amos en un es ado
((0, GlobalV a iables, [],⊥,nil [ a 7→ 0]) : (1, Impmain, (nil, S, 0),⊥,nil [global al 7→ 0]),C)
donde Ses el c´odigo de main. La a ea 0 del obje o 1 puede en a a ejecu a se con
la egla [selecABS] y podemos supone que se ejecu a po comple o, dando luga po el
camino a la c eaci´on de dos obje os de la clase Imp , lo que nos lle a al es ado
((0, GlobalV a iables, [],⊥,nil [ a 7→ 0]) :
(1, Impmain, (nil, (0),0),⊥,nil [global al 7→ 0]) :
(2, Imp , (nil [ alue 7→ 1] , S0,1),⊥,nil [global al 7→ 0]) :
(3, Imp , (nil [ alue 7→ 2] , S0,2),⊥,nil [global al 7→ 0]),C)
donde S0=awai global al!se a ( alue); .
En cualquie momen o pueden se seleccionadas las a eas 1 y 2 en sus espec i os obje os,
c eando dos a eas en el obje o 0, asociadas a cada una de las asignaciones sob e la a iable
global a . Llegando po ejemplo al es ado
((0, GlobalV a iables, (nil [ al 7→ 1] , S00,3) : (nil [ al 7→ 2] , S00,4),⊥,nil [ a 7→ 0]) :
(1, Impmain, (nil, (0),0),⊥,nil [global al 7→ 0]) :
(2, Imp , (nil [ alue 7→ 1] , awai 3,1),⊥,nil [global al 7→ 0]) :
(3, Imp , (nil [ alue 7→ 2] , awai 4,2),⊥,nil [global al 7→ 0]),C)
40 CAP´
ITULO 3. ABS: SINTAXIS Y SEM ´
ANTICA
donde S00 es el c´odigo que asigna al al a ibu o a de la clase.
Aho a la egla [selecABS] puede escoge alguna de las dos a eas del obje o 0. Es en
es e pun o donde la selecci´on de a ea da ´a luga a los dos en elazamien os posibles del
p og ama. Suponiendo que p ime o se ejecu e la a ea 3 y pos e io men e la a ea 4 se
llega a
((0, GlobalV a iables, (nil [ al 7→ 1] , ε, 3) : (nil [ al 7→ 2] , ε, 4),⊥,nil [ a 7→ 2]) :
(1, Impmain, (nil, (0),0),⊥,nil [global al 7→ 0]) :
(2, Imp , (nil [ alue 7→ 1] , awai 3,1),⊥,nil [global al 7→ 0]) :
(3, Imp , (nil [ alue 7→ 2] , awai 4,2),⊥,nil [global al 7→ 0]),C)
En es e momen o los awai de las a eas 1 y 2 pueden conclui y llegamos al es ado inal
((0, GlobalV a iables, (nil [ al 7→ 1] , ε, 3) : (nil [ al 7→ 2] , ε, 4),⊥,nil [ a 7→ 2]) :
(1, Impmain, (nil, (0),0),⊥,nil [global al 7→ 0]) :
(2, Imp , (nil [ alue 7→ 1] , ε, 1),⊥,nil [global al 7→ 0]) :
(3, Imp , (nil [ alue 7→ 2] , ε, 2),⊥,nil [global al 7→ 0]),C)
Cap´ı ulo 4
T aducci´on a ABS
La aducci´on de CABS a ABS o ma el g ueso de es e abajo. La di e encia de pa a-
digmas en e un lenguaje y o o hace que sea necesa io la implemen aci´on de algunas
es uc u as de da os adicionales ausen es en ABS.
Adem´as de dichas es uc u as, es necesa io emplea algunos ucos pa a pode ence las
es icciones del lenguaje pa a c ea el concep o de a iable global o de llamada a uncio-
nes s´ınc ona.
En es e cap´ı ulo discu i emos es e ema de una o ma abs ac a pa a pos e io men e pode
lle a a cabo la implemen aci´on de un compilado co ec o.
4.1. Va iables globales y unciones
La ausencia de memo ia compa ida en e los dis in os COGs (Concu en Objec G oup)
o conjun o de a eas de un obje o hace que la idea de a iable global no sea inmedia a.
Del mismo modo, es necesa io discu i el concep o de unci´on al es ilo de C, pese a que
los m´e odos de una in e az en ABS sean p´ublicos y a p ime a is a simila es.
Una p ime a ap oximaci´on end ´ıa dada po el uso de una ´unica clase en la que encapsula
odo nues o p og ama. Es a clase implemen a ´ıa una in e az con odas las cabece as de
las unciones de nues o p og ama. Adem´as con a ´ıa en e sus a ibu os con las a iables
globales, consiguiendo de es e modo una isibilidad comple a desde cualquie pun o del
p og ama.
Veamos qu´e ocu e con el siguien e c´odigo de ejemplo en CABS. En ´el se puede e como
se llama a la unci´on con h ead haciendo que las dos asignaciones de la a iable a 1
puedan en elaza se.
1in a 1;
2
3 oid () {
4 a 1 = 2;
41
48 CAP´
ITULO 4. TRADUCCI ´
ON A ABS
30 }
Po ´ul imo, se ´ıa con enien e (y lo se ´a m´as adelan e en la aducci´on de las unciones)
ene un m´e odo que nos de uel a el a ay global pa a usa lo con algunos ines locales
(conc e amen e el paso de a ays po e e encia en los a gumen os de una unci´on). Es o
se consigue con un m´e odo e ie e que implemen e la clase GlobalV a iables. Pa a el
ejemplo an e io , queda ´ıa como
1in e ace GLOBAL {
2A ayIn e ie ea ay ();
3In ge a ay (In indx );
4Uni se a ay (In indx , In al);
5Uni ini ();
6}
7
8class GlobalVa iables () implemen s GLOBAL {
9...
10 A ayIn e ie ea ay () {
11 e u n a ay;
12 }
13 ...
14 }
15 ...
No hay que deci que las clases que hemos implemen ado en es a secci´on pe mi en su uso
en cualquie ´ambi o local de un m´e odo, con lo que ambi´en con a emos con a ays locales
en ABS.
4.2.1. A ays mul idimensionales
El lenguaje CABS pe mi e en su sin axis decla a a ays mul idimensionales al es ilo de
C. ABS no cuen a con un ipo de da os simila , pe o, g acias a la p opues a p e iamen e
expues a, podemos simula el compo amien o de las ma ices es ableciendo una biyecci´on
con la ep esen aci´on de un a ay de ama˜no el p oduc o de los ama˜nos de las dimensio-
nes de la ma iz. En o as palab as, la aducci´on implemen ada en es e abajo conside a
las ma ices como un a ay unidimensional.
A modo de explicaci´on, sea ma una ma iz mul idimensional en e a en in N1×· · ·×in ND
y supongamos que que emos accede a la posici´on (i1, . . . , iD) donde ∀j∈ {1, . . . , D}
enemos ij∈ {0, . . . , Nj−1}, en onces la posici´on pco espondien e a dicho elemen o en
un a ay en in QD
i=1 Ni end ´ıa dada po p=PD
l=1 il·(Ql−1
j=1 Nj).
4.3. Exp esiones a i m´e icas
CABS p esen a una g an lexibilidad en sus exp esiones a i m´e ico-l´ogicas no p esen es en
ABS. La sin axis de ABS obliga a que el alo de e o no de uel o po una unci´on solo

4.3. EXPRESIONES ARITM ´
ETICAS 49
pueda se asignado a una a iable, no pudiendo se usado inmedia amen e en una exp e-
si´on del mismo ipo que el de e o no. Es o nos obliga a aduci las exp esiones a i m´e icas
en una se ie de asignaciones auxilia es cuyas a iables pos e io men e se ope an con los
alo es almacenados en ellas. Se ´a po an o necesa io ene un modo de ob ene nomb es
de a iables auxilia es que no se e e encien en ning´un o o pun o del p og ama aducido.
Sea po an o Aux :N→Va una unci´on de inida sob e los en e os que de uel e el
n-´esimo nomb e de a iable lib e. En un sen ido es ic o es a unci´on debe ´ıa oma como
a gumen o el p og ama en CABS y la aducci´on pa cial en ABS pa a sabe qu´e nomb es
de a iable han sido ya usados. A modo de simpli icaci´on podemos e i a es o ese ando
un conjun o de nomb es de a iables pa a es e p op´osi o que no sean accesibles al usua io.
Es a es la idea que pos e io men e se lle a ´a a cabo en la implemen aci´on del compilado .
De aho a en adelan e nos e e i emos a es e conjun o como Va R⊂Va . Un posible
ejemplo de subconjun o Va Rpod ´ıa se {aux a : ∈N}, que po ene la misma
ca dinalidad que Nnos pe mi e c ea una biyecci´on inmedia a.
Teniendo es o en cuen a, esul a ´acil pensa en de ini la aducci´on de las exp esiones
como una unci´on que oma una exp esi´on en CABS jun o con un na u al y que de uel e
una exp esi´on en ABS jun o con un na u al que indique el siguien e na u al no u ilizado
en la aducci´on. Si ga an izamos no epe i un mismo npa a dos exp esiones dis in as
en onces ga an izamos que las a iables auxilia es no son usadas m´as all´a de una ´unica
asignaci´on y una ´unica e e encia.
Especi icamos es a idea con la de inici´on de las unciones CAexp :Aexp →N→(ABS×N)
y su hom´ologa CBexp pa a las exp esiones booleanas:
CAexp JnK = (In (Aux ) = n, + 1)
CAexp JxK = (In (Aux ) = x, + 1) donde xes a iable en e a local.
CAexp JxK = (In (Aux ) = awai global al!ge x(), + 1)
donde xes a iable en e a global.
CAexp Ja1Aa2K = (c1;c2;In (Aux 00)=(Aux ( 0−1)) A(Aux ( 00 −1)), 00 + 1)
donde CAexp Ja1K = (c1, 0) y CAexp Ja2K 0= (c2, 00)
CBexp J alseK = (Bool (Aux ) = False, + 1)
CBexp J ueK = (Bool (Aux ) = T ue, + 1)
CBexp JxK = (Bool (Aux ) = x, + 1) donde xes a iable booleana local.
CBexp JxK = (Bool (Aux ) = awai global al!ge x(), + 1)
donde xes a iable booleana global.
CBexp Jb1Bb2K = (c1;c2;Bool (Aux 00) = (Aux ( 0−1)) B(Aux ( 00 −1)), 00 + 1)
donde CBexp Jb1K = (c1, 0) y CBexp Jb2K 0= (c2, 00)
CBexp Ja1a2K = (c1;c2;Bool (Aux 00) = (Aux ( 0−1)) (Aux ( 00 −1)), 00 + 1)
donde CAexp Ja1K = (c1, 0) y CAexp Ja2K 0= (c2, 00) y compa ado .
Pa a las llamadas a unciones supond emos po el momen o que las in e aces y clases aso-
ciadas se encuen an aducidas en alg´un o o pun o del c´odigo y que po an o podemos
50 CAP´
ITULO 4. TRADUCCI ´
ON A ABS
hace uso de sus nomb es.
CAexp J (e1. . . en)K 1= (c1. . . cn
In (Aux ( n+1)) = new Imp (global al)
In (Aux ( n+1 + 1)) = (Aux ( n+1))!((Aux ( 2−1)),...,
(Aux ( n+1 −1))), n+1 + 2)
donde CExp JeiK i= (ci, i+1) (escogiendo CAexp oCBexp seg´un con enga)
CBexp J (e1. . . en)K 1= (c1. . . cn
In (Aux ( n+1)) = new Imp (global al)
Bool (Aux ( n+1 + 1)) = (Aux ( n+1))!((Aux ( 2−1)),...,
(Aux ( n+1 −1))), n+1 + 2)
donde CExp JeiK i= (ci, i+1) (escogiendo CAexp oCBexp seg´un con enga)
4.4. T aducci´on de c´odigo
T as es a in oducci´on, podemos islumb a qu´e aspec o end ´a la aducci´on de c´odigo
lle ada a cabo en es e abajo. Ob ia emos el p e´ambulo de los p og amas ABS, que
inclui ´a la de inici´on de los clases A ay, y nos cen a emos en o os aspec os m´as impo -
an es.
Sea pues la unci´on C:CABS →N→(ABS ×N) nues a unci´on de aducci´on de
CABS a ABS de inida ecu si amen e del siguien e modo:
CJin a ;K = (In a , )
CJbool a ;K = (Bool a , )
CJ a =a;K = (c; a = (Aux ( 0−1)), 0)
donde CAexp JaK = (c, 0) y a a iable local en e a
CJ a =b;K = (c; a = (Aux ( 0−1)), 0)
donde CBexp JbK = (c, 0) y a a iable local booleana
CJ a =a;K = (c;awai global al!se a (Aux ( 0−1)), 0)
donde CAexp JaK = (c, 0) y a a iable global en e a
CJ a =b;K = (c;awai global al!se a (Aux ( 0−1)), 0)
donde CBexp JbK = (c, 0) y a a iable global booleana
CJS1S2K = (c1c2, 00) donde CJS1K = (c1, 0) y CJS2K 0= (c2, 00)
CJi (b){S1}else{S2}K = (c1;i (Aux ( 0−1)){c2}else{c3}, 000)
donde CBexp JbK = (c1, 0), CJS1K 0= (c2, 00) y CJS2K 00 = (c3, 000)
CJwhile(b){S}K = (c1;while(Aux ( 0−1)){c2c3Aux ( 0−1) = Aux ( 000 −1); }, 000)
donde CBexp JbK = (c1, 0), CJSK 0= (c2, 00) y CBexp JbK 00 = (c3, 000)
4.4. TRADUCCI ´
ON DE C ´
ODIGO 51
Sob e la aducci´on del while cabe des aca que es necesa io aduci dos eces su condi-
ci´on y el uso de una asignaci´on adicional. Es o es debido a que el concep o de while obliga
a e alua su condici´on an es de la ejecuci´on de su cue po en cada una de las i e aciones
pa a decidi si el sal o se oma o no. Po el modo en que se han aducido las exp esiones
a i m´e ico-l´ogicas, la condici´on en ABS de un while se educe a comp oba el alo asig-
nado a una a iable auxilia y es po es o po lo que, sob e dicha a iable, se ha ´a una
asignaci´on adicional al inal de oda i e aci´on.
En segundo luga , hace al a menciona que las unciones de aducci´on de exp esiones
booleanas no con emplan la eu ilizaci´on de a iables, po lo que aunque la condici´on sea
la misma, se emplea ´an unos nomb es de a iables nue os al inal del cue po del while
espec o a los que se usaban al e alua la condici´on ue a del cue po. A e ec os p ´ac icos,
es ´acil demos a que los nomb es de las a iables auxilia es no in luyen en el c´ompu o
de la exp esi´on booleana. De hecho se e cla amen e que la aducci´on es la misma sal o
un o se en el na u al que iden i ica a las a iables auxilia es.
Es po es o po lo que podemos en ende que en la aducci´on del c´odigo se puede indis-
in amen e sus i ui el c´odigo c3po c2en la egla del while si po mo i os de simplicidad
hicie a al a a la ho a de desa olla la co ecci´on de es a aducci´on. En una implemen a-
ci´on eal es o no es inmedia o po que los compilado es o in e p e es de ABS no pe mi en
la decla aci´on duplicada de a iables, p oblema que en es e abajo no nos a a˜ne a ni el
abs ac o.
Pa a la aducci´on de las unciones necesi amos p e iamen e una aducci´on de los a gu-
men os Ca g :A gs →A gsABS que en esencia lo ´unico que hace es cambia los ipos de
CABS a los de ABS.
Ca g ε=ε
Ca g (in a , a g) = In a , Ca g a g
Ca g (bool a , a g) = Bool a , Ca g a g
Usando es a aducci´on de a gumen os enemos que
CJin unc(a g){S e u n a}K = (in e ace In unc{In unc(Ca g a g); }
class Imp unc(GLOBAL global al) implemen s In unc{
In unc(Ca g a g){c c0 e u n Aux ( 00 −1)}}, 00)
donde CJSK = (c, 0) y CAexp JaK 0= (c0, 00)
CJbool unc(a g){S e u n b}K = (in e ace In unc{Bool unc(Ca g a g); }
class Imp unc(GLOBAL global al) implemen s In unc{
Bool unc(Ca g a g){c c0 e u n Aux ( 00 −1)}}, 00)
donde CJSK = (c, 0) y CBexp JbK 0= (c0, 00)
CJ oid unc(a g){S}K = (in e ace In unc{Uni unc(Ca g a g); }
class Imp unc(GLOBAL global al) implemen s In unc{
Uni unc(Ca g a g){c}}, 0) donde CJSK = (c, 0)
52 CAP´
ITULO 4. TRADUCCI ´
ON A ABS
y pa a las a iables globales enemos
CJ a =a;K = (c;awai global al!se a (Aux ( 0−1)), 0)
donde CAexp JaK = (c, 0) y a a iable global en e a
CJ a =b;K = (c;awai global al!se a (Aux ( 0−1)), 0)
donde CBexp JbK = (c, 0) y a a iable global booleana
Po ´ul imo, habla emos de la aducci´on del h ead. Como ya hemos comen ado en las
secciones an e io es, la aducci´on p opues a es simila a la de las llamadas a unci´on con
la di e encia de que no se espe a a la esoluci´on del alo u u o de e o no. Su egla es
CJ h ead (e1. . . en)K 1= (c1. . . cn
In (Aux ( n+1)) = new Imp (global al)
(Aux ( n+1))!((Aux ( 2−1)),...,(Aux ( n+1 −1))), n+1 + 1)
donde CExp JeiK i= (ci, i+1) (escogiendo CAexp oCBexp seg´un con enga)
4.4.1. T aducci´on de a ays
Como comen amos ya en el cap´ı ulo sob e la sem´an ica de CABS, los a ays queda ´an
excluidos de la demos aci´on o mal y es po ello po lo que hemos decidido no inclui los
en la de inici´on de la aducci´on. No obs an e, la implemen aci´on s´ı los iene en cuen a y
lle a a cabo la compilaci´on eniendo en cuen a lo comen ado en la secci´on sob e a ays de
es e cap´ı ulo.
Cap´ı ulo 5
Co ecci´on
A lo la go de es e cap´ı ulo usa emos las de iniciones de las sem´an icas p e iamen e expues-
as pa a comp oba que la aducci´on p opues a de CABS a ABS es co ec a. En o as
palab as, du an e las p ´oximas secciones, demos a emos que dado un c´odigo en CABS
y pa iendo de un es ado inicial podemos “ejecu a ” una se ie de pasos has a llega a un
nue o es ado que iene un hom´ologo en ABS y que esul a de ejecu a la aducci´on desde
un es ado equi alen e al inicial en CABS (y ice e sa).
Es e p ocedimien o es conocido como bisimulaci´on y nos pe mi i ´a hace a i maciones an
ue es como las que buscamos, es deci , que si enemos un c´odigo en CABS y dada su
aducci´on sabemos, usando la he amien as ya desa olladas pa a ABS, que cumple una
cie a p opiedad pa iendo de un es ado, sab emos en onces que el mismo esul ado se
sos iene pa a el c´odigo en CABS.
5.1. Equi alencia en e es ados
Sea (G,F,RP) un es ado en CABS y (O,C) un es ado en ABS. Di emos que es os es ados
son equi alen es si:
dado (id, c, RT, , a )∈Oel obje o co espondien e a la clase GlobalVa iables,
enemos que las unciones Gya son la misma.
pa a odo nomb e de unci´on unc con F( unc)=( , S, a gs, a), enemos que
CJImp uncK= (In unc,nil, me , a gc) donde me J uncKcon iene la aducci´on
de los a gumen os a gs y del c´odigo de la unci´on y los a gumen os de clase a gc
con ienen solo una a iable con el ipo de la in e az de las a iables globales.
cada elemen o en RP se co esponde con un conjun o de a eas en los obje os de
O, en conc e o, cada en o no de a iables apilado se co esponde con los a ibu os
(ob iando a iables auxilia es) de una a ea cuyo c´odigo aducido se co esponde
con un segmen o de ins ucciones del c´odigo del p oceso. Lo que se quie e deci con
es o es que, mien as que las llamadas a unci´on en CABS se co esponden con el
apilamien o de un nue o en o no de a iables y la conca enaci´on del c´odigo de la
unci´on con el c´odigo ac ual del p oceso, en ABS se c ea una nue a a ea a la que
se espe a pa a ob ene el alo de e o no.
53

54 CAP´
ITULO 5. CORRECCI ´
ON
en caso de exis i un elemen o (local :s, x =e;S)∈RP donde e iene elemen os en
Vya calculados, se iene que en la a ea del es ado equi alen e se han ejecu ado ya las
asignaciones a las a iables auxilia es co espondien es con los alo es ya calculados
y, po an o, quedan po calcula las asignaciones a a iables auxilia es es an es en
la exp esi´on. En o as palab as, cada paso de e aluaci´on de una exp esi´on se ´a una
asignaci´on en la aducci´on en ABS. Es o es ´alido an o pa a en e os como pa a
booleanos.
5.2. Co ecci´on de las exp esiones a i m´e ico-l´ogicas
Una de las peculia idades que iene CABS, es pe mi i en sus exp esiones una no aci´on
pa a ealiza llamadas a unci´on con e o no de alo . Como ya no amos en el cap´ı ulo
an e io , es o hace que la aducci´on se apoye en el uso de unas a iables auxilia es que
pe mi en di idi el c´ompu o de una exp esi´on en el c´ompu o de las dis in as subexp esio-
nes que la componen.
Cada exp esi´on u ilizada en un p og ama CABS se co esponde de o ma un´ı oca con una
a iable auxilia en ABS que almacena ´a el alo de la exp esi´on cuando es e es ´e dispo-
nible. De es e modo, en odo momen o podemos hace uso de es a in o maci´on, aunque,
po simpli ica la no aci´on, no es ´e p esen e en el es ado del p og ama.
Hecha es a in oducci´on, p ocedemos a comp oba en p ime luga que las asignaciones
hechas en CABS se co esponden con las de la aducci´on de es as a ABS, llegando de
es ados equi alen es a es ados equi alen es en un solo paso.
En es a memo ia expond emos solo el p oceso pa a las exp esiones a i m´e icas. El caso de
las exp esiones booleanas es comple amen e an´alogo sal o ipo y ope ado es empleados.
5.2.1. Va iables locales
Caso x=νcon ν∈V
Sean (G,F,RP ;(local :s, x =ν;S)) y (O;(id, c, RT ;(loc, x =aux a k;SABS, ), , a ),C)
es ados equi alen es, donde la a iable auxilia k-´esima es la a iable asignada a la exp e-
si´on νde o ma que loc(aux a k) = ν.
Tenemos que del es ado (G,F,RP ;(local :s, x =ν;S)), aplicando la egla [ass2
C], lle-
gamos al es ado (G,F,RP ;(local [x7→ ν] : s, S)) en CABS. Po o o lado, del es ado
equi alen e en ABS (O;(id, c, RT ;(loc, x =aux a k;S, ), , a ),C), aplican-
do la egla de asignaci´on local co espondien e, llegamos al es ado (O;(id, c, RT ;
(loc hx7→ A Jaux a kKloc,a i, SABS, ), , a ),C) y del hecho de que dicha a iable
auxilia enga el alo de νllegamos inmedia amen e a un es ado equi alen e.
5.2. CORRECCI ´
ON DE LAS EXPRESIONES ARITM ´
ETICO-L ´
OGICAS 55
Caso x=n
Sea (G,F,RP ;(local :s, x =n;S)) y sea (O;(id, c, RT ;(loc, In aux a k =
n;x=aux a k;SABS, ), , a ),C) su es ado equi alen e, donde la a iable auxilia
k-´esima es la a iable asignada a la exp esi´on n.
En es e caso, solo podemos aplica pa a el p oceso ac ual la egla [ass1
C] que delega la ac-
ci´on en las eglas pa a exp esiones a i m´e ico-l´ogicas. La egla aplicable en es a si uaci´on
es [numA] con lo que llegamos al es ado (G,F,RP ;(local :s, x =NJnK;S)).
En el lado de ABS aplicamos la egla de asignaci´on sob e la a iable auxilia llegando al es-
ado (O;(id, c, RT ;(loc haux a k 7→ A JnKloc,a i, x =aux a k;SABS, ), , a ),C)
p ese ´andose la equi alencia en e es ados al asigna el alo de la exp esi´on a su a iable
auxilia .
Caso x= () (simpli icaci´on sin a gumen os)
Sean los es ados equi alen es (G,F,RP ;(local :s, x = (); S)) y (O;(id, c, RT ;
(loc, In aux a (k−1) = new Imp (global al); In aux a k =awai auxi a (k−
1)! (); x=aux a k;SABS, ), , a ),C) donde la a iable auxilia k-´esima es la a ia-
ble asignada a la exp esi´on ().
La sem´an ica de CABS nos pe mi e usa la egla [ass1
C] con la egla call2
A esul ando en
el es ado (G,F,RP ;(nil :local :s, SFx=UNSTACK (a) ; S)) donde aes la exp esi´on de
e o no de .
Po o o lado, en la sem´an ica de ABS, podemos aplica p ime o la egla de c eaci´on de
obje os y a con inuaci´on la egla de llamada s´ınc ona, esul ando el es ado
(O;(id0, c0,(nil, SF
ABS, 0),⊥,a 0)
(id, c, RT ;(loc, In aux a k =awai 0;x=aux a k;SABS, ), , a ),C)
Llegados a es e pun o enemos un es ado que es equi alen e al esul an e en la sem´an ica
de CABS pues o que el concep o de apila un nue o ´ambi o de a iables en ABS se e
e lejado c eando un obje o nue o que iene como ´unica a ea asignada el c´ompu o del
c´odigo aducido de la unci´on . El obje o o iginal se e pausado po el awai has a que
no e mine de ejecu a se el c´odigo de , imi ando el concep o del c´odigo conca enado en
CABS que no deja ejecu a el es o de ins ucciones has a no e mina con las de la unci´on.
O o de alle a ene en cuen a es el indicado de a ea ac ual. T as da los dos pasos
an e io es en la sem´an ica de ABS se nos lle a a ene como a ea asignada en el nue o
obje o a ⊥. E iden emen e, an es de pode se ejecu a la p ime a ins ucci´on de es ne-
cesa io que se ejecu e la egla de selecci´on de a ea. El hecho de que ning´un obje o de
nues a aducci´on aya a ejecu a m´as de una a ea (a excepci´on del obje o de a iables
globales del que habla emos m´as adelan e) nos pe mi e ex ende la idea de equi alencia a
es e es ado ac ual, pues o que conside amos que aplica una egla de selecci´on no a ec a
en esencia a la con igu aci´on ac ual en ABS ya que solo lo hacen los “mo imien os” en el
56 CAP´
ITULO 5. CORRECCI ´
ON
c´odigo.
De o ma simila , el hecho de ene que da dos pasos ampoco a ec a, pese a exis i
una concu encia en la sem´an ica. El mo i o es que en e ambos pasos el obje o c eado
solo es e e enciado po una a iable auxilia de modo que se ga an iza que no puede
se modi icado desde ning´un o o pun o de la ejecuci´on. De es e modo podemos ol e a
ex ende el concep o de equi alencia pe mi iendo que el paso in e medio de c eaci´on del
obje o (omi ido en es e ex o) pueda se ambi´en conside ado un es ado que man iene la
equi alencia con (G,F,RP ;(nil :local :s, SFx=UNSTACK (a) ; S)). Con es o se quie e
deci que, al igual que las eglas de selecci´on de a ea, la c eaci´on de obje os no al e a
ampoco el es ado in ´ınseco del p og ama.
Caso x=UNSTACK (ν)con ν∈V
Sean los es ados equi alen es (G,F,RP ;(local0:local :s, x =UNSTACK (ν) ; S)) y
(O;(id0, c0,(loc0, e u n aux a k0, 0), 0,a 0)
(id, c, RT ;(loc, In aux a k =awai 0;x=aux a k;SABS, ), , a ),C)
donde la a iable auxilia k0-´esima es la a iable asignada a la exp esi´on ν, que iene su
alo asignado en loc0, y la k-´esima al uns ack.
En el caso de CABS, aplica la egla [ass1
C] con la egla uns ack2
Apa a la exp esi´on nos
lle a al es ado (G,F,RP ;(local :s, x =ν;S)).
En el caso de ABS, podemos aplica la egla de e o no que nos lle a a un es ado in e medio
(O;(id0, c0,(loc0, ε(AJaux a k0Kloc,a ), 0), 0,a 0)
(id, c, RT ;(loc, In aux a k =awai 0;x=aux a k;SABS, ), , a ),C)
Desde es e es ado se puede aplica la egla del awai que pe mi e ecoge el alo de νy
asign´a selo, en es e caso, a la a iable aux a k, llegando al es ado
(O;(id0, c0,[],⊥,a 0)
(id, c, RT ;(loc [aux a k 7→ ν], x =aux a k;SABS, ), , a ),C)
que man iene la equi alencia.
De nue o se nos p esen a la discusi´on de los pasos m´ul iples. El mismo a gumen o que
hemos p esen ado an e io men e es aplicable a es a si uaci´on y podemos ex ende la equi-
alencia de es ados a los es ados in e medios po los que se pasa en la sem´an ica de ABS
pa a lle a a cabo el e u n.
Cabe des aca que el concep o de desapila un en o no en CABS queda e lejado en el
hecho de que el obje o con el ´ambi o supe io no uel e a se usado y queda ac´ıo de
a eas.
5.2. CORRECCI ´
ON DE LAS EXPRESIONES ARITM ´
ETICO-L ´
OGICAS 57
Caso x=a1a2
An es de discu i es e caso con iene e que en CABS el c´ompu o de a1a2p ecisa del
c´ompu o de a1, de modo que el a gumen o que amos a segui pa a el caso compues o
es asumi que odo a bien si nos encon ´a amos con la exp esi´on a1y que po an o la
asunci´on se puede emplea pa a la exp esi´on a1a2.
O o de alle impo an e a ene en cuen a es que no se empieza a p ocesa la exp esi´on
a2has a que no hemos comple ado el c´ompu o de a1, como se e leja en las eglas de
la sem´an ica de CABS. Es o se e leja ´a ambi´en en ABS ya que las asignaciones de la
exp esi´on a2 ienen p ecedidas po las de la exp esi´on a1.
Dicho es o, sean los es ados equi alen es (G,F,RP ;(local :s, x =a1a2;S)) y
(O;(id, c, RT ;(loc, c1c2In aux a k =aux a k1aux a k2;
x=aux a k;SABS, ), , a ),C)
donde c1es el c´odigo asociado a a1,c2el asociado a a2yaux a k1,aux a k2y
aux a k las a iables asociadas a cada una de las exp esiones a i m´e icas en juego.
En conc e o enemos que la ´ul ima ins ucci´on de c1, po el modo en que hemos de ini-
do la aducci´on, se co esponde con una asignaci´on a su a iable auxilia . Po el modo
en que es ´an de inidas las exp esiones a i m´e icas, podemos aplica inducci´on es uc u al
con lo que, po hip´o esis de inducci´on enemos que los es ados equi alen es (G,F,RP ;
(local :s, x =a1;S)) y (O;(id, c, RT ;(loc, c1x=aux a k1;SABS, ), , a ),C)
llegan en un solo paso a los es ados equi alen es (G,F,RP ;(local :s, x =a0
1;S)) y
(O;(id, c, RT ;(loc, c0
1x=aux a k1;SABS, ), , a ),C).
Teniendo en cuen a es o y que si enemos un c´odigo en ABS, S1, que en un paso desde
un es ado dado al que deno a emos po sse llega a un es ado s0con c´odigo S0
1en onces
end ´ıamos un compo amien o simila con el c´odigo S1S2yS0
1S2(en o as palab as, el
conca ena c´odigo po de ´as no al e a el signi icado de los es ados in e medios), llegamos
a que de los es ados o iginales llegamos en un paso a los es ados (G,F,RP ;(local :
s, x =a0
1a2;S)) y
(O;(id, c, RT ;(loc, c0
1c2In aux a k =aux a k1aux a k2;
x=aux a k;SABS, ), , a ),C)
que son equi alen es.
Casos x=νa2yx=νµcon ν, µ ∈Z
La si uaci´on del p ime caso es comple amen e an´aloga a la del caso an e io con la di e-
encia de que la hip´o esis de inducci´on es aplicada sob e la exp esi´on a2.
Pa a el segundo caso enemos los es ados equi alen es (G,F,RP ;(local :s, x =
νµ;S)) y (O;(id, c, RT ;(loc, In aux a k =aux a k1aux a k2;x=
64 CAP´
ITULO 6. IMPLEMENTACI ´
ON: COMPILADOR DE CABS A ABS
•An´alisis l´exico: a pa i del c´odigo de o igen se ex aen los dis in os elemen os
l´exicos o okens que lo componen, po ejemplo, las palab as ese adas del
lenguaje, los nomb es de a iables, e c.
•An´alisis sin ´ac ico: usando los oken del an´alisis l´exico, median e el uso de
un au ´oma a de e minis a que econozca la g am´a ica del lenguaje, se c ea un
´a bol de sin axis abs ac a en cuyos nodos podemos encon a las piezas l´ogicas
que componen nues o p og ama, po ejemplo, las asignaciones de a iables, la
decla aci´on de unciones, e c.
•An´alisis es ´a ico: en es a ase se analizan los iden i icado es usados en el p o-
g ama, en busca de usos il´ıci os como en el caso de las asignaciones en a iables
no decla adas, y los ipos de las exp esiones que pe mi en desca a p og amas
con e o es. De es e p oceso se ob iene una abla de s´ımbolos que puede se de
ayuda en la aducci´on inal del c´odigo.
Back-end o ase de aducci´on: a pa i del ´a bol de sin axis abs ac a y del es o de
es uc u as ob enidas en la e apa an e io , el compilado gene a un c´odigo obje o
en endible pa a la m´aquina o in e p e e pa a el que es ´a des inado. En es a e apa
ambi´en se pueden lle a a cabo algunas op imizaciones, pe o habla de ello no es
nues o obje i o.
6.2. JLex
JLex1es un gene ado de analizado es l´exicos en ja a desa ollado en la Uni e sidad de
P ince on. A pa i de una especi icaci´on de los okens de un lenguaje, JLex gene a un
au ´oma a capaz de econoce los ecogido en una clase de Ja a.
El au ´oma a empleado en los analizado es l´exicos es un au ´oma a ini o de e minis a,
ca ego ´ıa en la que se encuen an los econocedo es de los lenguajes o males m´as b´asicos
conocidos como lenguajes egula es.
La especi icaci´on del analizado l´exico de CABS se puede encon a en el a chi o pa se .lex
den o del paque e pa se . A su ez, den o de es e paque e se encuen an la clase
Yy oken, que se ´a el ipo de obje o manipulado po el analizado sin ´ac ico, y el a -
chi o Yylex.ja a, con las clases asociadas al au ´oma a ini o de e minis a.
6.3. CUP
CUP2(Cons uc ion o Use ul Pa se s) es un gene ado de analizado es sin ´ac icos LALR(1)
desa ollado en Ja a y man enido po la Uni e sidad T´ecnica de Munich (TUM).
1h ps://www.cs.p ince on.edu/~appel/mode n/ja a/JLex/cu en /manual.h ml
2h p://www2.cs. um.edu/p ojec s/cup/

6.3. CUP 65
Figu a 6.1: Cap u a de las eglas pa a la gene aci´on del lexe .
Figu a 6.2: Cap u a de las eglas de la g am´a ica de CABS.
66 CAP´
ITULO 6. IMPLEMENTACI ´
ON: COMPILADOR DE CABS A ABS
Con una sin axis simila a la de YACC, se puede especi ica la g am´a ica del lenguaje
pa a el que uno quie e c ea un pa se y CUP gene a un analizado ecogido en una clase
de ja a.
La g am´a ica de CABS se encuen a en el iche o syn .cup den o del paque e pa se .
La clase pa se , con enida ambi´en en el paque e an e io , es el a chi o gene ado po
CUP.
6.4. Es uc u a del compilado
El analizado sin ´ac ico se apoya en g an medida en la es uc u a de nodos que el desa-
ollado del lenguaje de e mina pa a su c eaci´on. Pues o que as la ase de pa se se
ob iene un p ime ´a bol de sin axis abs ac a, es necesa io ya pa a es a ase conoce cu´ales
son las clases empleadas pa a es e p op´osi o.
La je a qu´ıa de los nodos empleados en CABS se di ide en los siguien es paque es:
Con olS uc u es: con iene los bloques asociados a las es uc u as de decisi´on como
son los condicionales (I Node) y lo bucles (LoopNode).
Exp essions: con iene los nodos del ´a bol de sin axis abs ac a asociados a las exp e-
siones a i m´e ico-l´ogicas. Las clases pe enecien es a es e paque e son las asociadas
a los en e os y booleanos (NumNode y BoolNode espec i amen e), los ope ado es
(Ope a o Node), las exp esiones bina ias de dos ope andos y un ope ado (Bina -
yExp ession) y una ias de un ope ando y un ope ado (Una yExp ession).
Func ions: paque e o mado con odas las clases asociadas a la decla aci´on de un-
ciones y p ocedimien os y sus llamadas, incluidas las de c eaci´on de un nue o hilo.
Va iables: paque e compues o po las clases empleadas en la decla aci´on de a iables
y a ays y su uso en asignaciones y exp esiones a i m´e ico-l´ogicas.
Adem´as de es os nodos, exis en o os nodos m´as gene ales que pe mi en comple a los
´a boles de sin axis abs ac a con el es o de cons ucciones ´ıpicas de un lenguaje de p o-
g amaci´on. Algunos de es os nodos son las asignaciones (AssNode), los bloques de c´odigo
(BlockNode y GlobalBlockNode) o los ipos de e o no y de a iables (TypeNode).
La cons ucci´on del ´a bol de de i aci´on se hace ecu si amen e, ap o echando la ecu si´on
p opia de los analizado es sin ´ac icos LALR. Pos e io men e, el con ol del es o de ases
es e omado po la clase Manage , que se enca ga de inicia los sucesi os eco idos del
´a bol pa a inicializa las ablas de iden i icado es de s´ımbolos, es deci , asocia a cada
uso de una a iable o unci´on su decla aci´on, y ealiza la comp obaci´on de ipos y la
exis encia de la unci´on main.
Po ´ul imo, si llegados a es e pun o no hay ning´un e o de compilaci´on, se p ocede a
la gene aci´on de c´odigo, pa a lo cual, cada nodo cuen a con un m´e odo de aducci´on
que p opaga la llamada ecu si amen e a los nodos de los que depende. De es e modo,
6.4. ESTRUCTURA DEL COMPILADOR 67
ap o echando la es uc u a del ´a bol, se esc ibe de o ma o denada en un a chi o las
ins ucciones del c´odigo des ino.
68 CAP´
ITULO 6. IMPLEMENTACI ´
ON: COMPILADOR DE CABS A ABS
Cap´ı ulo 7
SYCO: SYs ema ic es ing ool o
Concu en Objec s
SYCO es una de las he amien as implemen adas sob e el lenguaje ABS que pe mi e el
es ing de p og amas concu en es esc i os en es e lenguaje. La idea de SYCO es que, a
pa i del c´odigo de un p og ama, el p og amado pueda sabe de an emano las posibles
ejecuciones del p og ama adem´as de conoce si el p og ama p esen a posibles si uaciones
de deadlock.
El n´ucleo de SYCO incluye implemen aciones de ´ecnicas de pa ial-o de educ ion que
pe mi en la e aluaci´on de amas edundan es como las que se nos han p esen ado al p in-
cipio de es e abajo en algunos ejemplos.
A a ´es de una in e az web, uno puede ob ene isualmen e el esul ado que SYCO
gene a sob e el c´odigo p opo cionado.
Veamos algunos ejemplos de uso sob e el c´odigo ABS gene ado a pa i de un c´odigo en
CABS.
1in a ;
2
3in main () {
4 h ead (1);
5 h ead (2);
6 e u n 0;
7}
8
9 oid (in alue ) {
10 a = alue ;
11 }
En es e ejemplo enemos que la unci´on main lanza dos hilos que ejecu a ´an la unci´on
dando como posibles esul ados inales a = 1 y a = 2. La aducci´on a ABS queda ´ıa,
esumiendo pa e de la aducci´on que no es necesa ia pa a es e ejemplo, como:
69

70CAP´
ITULO 7. SYCO: SYSTEMATIC TESTING TOOL FOR CONCURRENT OBJECTS
1module Cabs;
2impo * om ABS . S dLib ;
3
4in e ace GLOBAL {
5In ge a ();
6Uni se a (In al );
7Uni ini ialize ();
8}
9
10 class GlobalVa iables () implemen s GLOBAL {
11 In a = 0;
12 Uni ini ialize () {
13 }
14 In ge a () {
15 e u n a ;
16 }
17 Uni se a (In al ) {
18 a = al ;
19 }
20 }
21
22 in e ace In {
23 Uni (In alue);
24 }
25 in e ace In main {
26 In main ();
27 }
28
29 class Imp ( GLOBAL global al ) implemen s In {
30 Uni ( In alue ) {
31 awai global al ! se a ( alue );
32 }
33 }
34
35 class Impmain ( GLOBAL global al ) implemen s In main {
36 In main () {
37 In aux_ a _0 = new Imp ( global al );
38 In aux_ a _1 = 1;
39 aux_ a _0 ! ( aux_ a _1 );
40 In aux_ a _2 = new Imp ( global al );
41 In aux_ a _3 = 2;
42 aux_ a _2 ! ( aux_ a _3 );
43 In aux_ a _4 = 0;
44 e u n aux_ a _4 ;
45 }
46 }
71
47
48 {
49 GLOBAL global al = new GlobalVa iables ();
50 awai global al ! ini ialize ();
51 In main p og = new Impmain ( global al );
52 awai p og !main ();
53 }
Y el esul ado que nos p opo ciona la he amien a SYCO es:
Independence cons ain s gene a ed in 908 ms.
Numbe o execu ions: 2
To al ime: 5
To al numbe o s a es explo ed du ing 2 execu ions: 16
To al numbe o asks execu ed du ing 2 execu ions: 7
Execu ion 1, numbe o asks: 6
(Click he e o see he sequence diag am)
- S a e:
|------objec (1,’GlobalVa iables’,[ ield( a ,2)])
|------objec (2,’Impmain’,[ ield(global al, e (1))])
|------objec (3,’Imp ’,[ ield(global al, e (1))])
|------objec (4,’Imp ’,[ ield(global al, e (1))])
|------objec (main,main,[])
- T ace: |------’Time: 0, Objec : main, Task: 0:main’
|------’Time: 1, Objec : GlobalVa iables_1, Task: 1:ini ialize’
|------’Time: 2, Objec : 0:main(54), Task: 0:main(54)’
|------’Time: 3, Objec : Impmain_2, Task: 3:main’
|------’Time: 4, Objec : 0:main(56), Task: 0:main(56)’
|------’Time: 5, Objec : Imp _3, Task: 5: ’
|------’Time: 6, Objec : GlobalVa iables_1, Task: 7:se a ’
|------’Time: 7, Objec : Imp _3, Task: 5: (34)’
|------’Time: 8, Objec : Imp _4, Task: 6: ’
|------’Time: 9, Objec : GlobalVa iables_1, Task: 9:se a ’
|------’Time: 10, Objec : Imp _4, Task: 6: (34)’
Execu ion 2, numbe o asks: 6
(Click he e o see he sequence diag am)
- S a e:
|------objec (1,’GlobalVa iables’,[ ield( a ,1)])
|------objec (2,’Impmain’,[ ield(global al, e (1))])
|------objec (3,’Imp ’,[ ield(global al, e (1))])
|------objec (4,’Imp ’,[ ield(global al, e (1))])
|------objec (main,main,[])
- T ace: |------’Time: 0, Objec : main, Task: 0:main’
|------’Time: 1, Objec : GlobalVa iables_1, Task: 1:ini ialize’
|------’Time: 2, Objec : 0:main(54), Task: 0:main(54)’
|------’Time: 3, Objec : Impmain_2, Task: 3:main’
|------’Time: 4, Objec : 0:main(56), Task: 0:main(56)’
72CAP´
ITULO 7. SYCO: SYSTEMATIC TESTING TOOL FOR CONCURRENT OBJECTS
|------’Time: 5, Objec : Imp _3, Task: 5: ’
|------’Time: 6, Objec : Imp _4, Task: 6: ’
|------’Time: 7, Objec : GlobalVa iables_1, Task: 9:se a ’
|------’Time: 8, Objec : GlobalVa iables_1, Task: 7:se a ’
|------’Time: 9, Objec : Imp _3, Task: 5: (34)’
|------’Time: 10, Objec : Imp _4, Task: 6: (34)’
donde podemos e las dos azas ob enidas.
Pa a un ejemplo m´as elabo ado como es
1in a ;
2in a 2;
3
4in main () {
5 h ead ();
6 h ead g();
7 e u n 0;
8}
9
10 oid () {
11 a = 1;
12 a = 2;
13 }
14
15 oid g() {
16 a 2 = 10 * a + a ;
17 }
cuya aducci´on “ esumida” es
1module Cabs;
2impo * om ABS . S dLib ;
3
4in e ace GLOBAL {
5In ge a ();
6Uni se a (In al );
7In ge a 2 ();
8Uni se a 2 (In al );
9Uni ini ialize ();
10 }
11 class GlobalVa iables () implemen s GLOBAL {
12 In a = 0;
13 In a 2 = 0;
14 Uni ini ialize () {
15 }
16 In ge a () {
17 e u n a ;
73
18 }
19 Uni se a (In al ) {
20 a = al ;
21 }
22 In ge a 2 () {
23 e u n a 2;
24 }
25 Uni se a 2 (In al ) {
26 a 2 = al ;
27 }
28 }
29
30 in e ace In {
31 Uni ();
32 }
33
34 in e ace In g {
35 Uni g();
36 }
37
38 in e ace In main {
39 In main ();
40 }
41
42 class Imp ( GLOBAL global al ) implemen s In {
43 Uni () {
44 In aux_ a _0 = 1;
45 awai global al ! se a ( aux_ a _0 );
46 In aux_ a _1 = 2;
47 awai global al ! se a ( aux_ a _1 );
48 }
49 }
50
51 class Impg ( GLOBAL global al ) implemen s In g {
52 Uni g() {
53 In aux_ a _2 = 10;
54 In aux_ a _3 = awai global al ! ge a () ;
55 In aux_ a _4 = ( aux_ a _2 * aux_ a _3 );
56 In aux_ a _5 = awai global al ! ge a () ;
57 In aux_ a _6 = ( aux_ a _4 + aux_ a _5 );
58 awai global al ! se a 2 ( aux_ a _6 );
59 }
60 }
61
62 class Impmain ( GLOBAL global al ) implemen s In main {
63 In main () {