PROGRAMEN EGIAZTAPENA
ETA ERATORPENA
Xabier Arregi
Arantza Díaz de Ilarraza
Paqui Lucio
UDAKO EUSKAL UNIBERTSITATEA
Bilbo, 1993
© Udako Euskal Unibertsitatea. Informatika Saila.
ISBN: 84-86967-50-3
Lege-gordailua: BI-22-92
Inprimategia: BOAN, S.A. Padre Larramendi 2 BILBO
Azala: Julio Pardo
Banatzaileak: UEU. General Concha 25, 6. BILBO
Zabaltzen: Igarabide, 88 DONOSTIA
Aurkibidea ____________________________________________________________ V
AURKIBIDEA
AURKIBIDEA ...................................................................................... V
SARRERA .......................................................................................... 1
1. Gaia. ESPEZIFIKAZIOA................................................................. 7
1.1. Zer da espezifikazioa ................................................................... 7
1.2. Zertarakoak ............................................................................... 8
1.3. Espezifikazio-lengoaiak................................................................ 9
1.3.1. Espezifikazio ez-formalak ................................................... 10
1.3.2. Aurre-ondoetako espezifikazio formala .................................. 17
Ariketak............................................................................................ 18
2. Gaia. DATU-MOTEN TRATAMENDU FORMALA ............................ 21
2.1. SET (Multzoa) .......................................................................... 22
2.2. ARRAY .................................................................................. 23
2.3. RECORD (Erregistroa) ............................................................... 23
2.4. FILE (Fitxategia) ....................................................................... 25
3. Gaia. LEHEN MAILAKO LOGIKAREN LENGOAIA .......................... 27
3.1. Lengoaiaren sintaxia ................................................................... 27
3.2. Lengoaiaren semantika ................................................................ 28
Ariketak........................................................................................... 34
4. Gaia. PROGRAMEN ZUZENTASUNA ............................................. 35
4.1. Testak ...................................................................................... 35
4.2. Egiaztapena ............................................................................... 37
4.2.1. Semantika axiomatikoa eta frogapen formalak ........................ 37
VI ____________________________________________________________________
4.2.2. Hoare-ren sistema formala .................................................. 40
Asignazioaren Axioma (AA) ................................................. 40
Sekuentzi konposaketaren erregela (KPE)................................ 41
Ondorioaren erregela (ODE) .................................................. 41
Baldintzazko konposaketaren erregelak (BDE) ........................... 44
Kasu-hautaketa agindua (KHE) .............................................. 47
Erazagupenak ..................................................................... 48
Ariketak........................................................................................... 50
Iterazioak eta inbariantearen kontzeptua ................................... 53
While agindua (WHE) ......................................................... 54
Repeat agindua (RPE) ......................................................... 56
Programen bukaeraren arazoa ................................................. 58
Iterazioen bukaera eta ondo oinarritutako ordenak ...................... 60
While agindurako metodoa .................................................... 62
Metodoaren egokitzapena (N,) ordenarako.............................. 64
Repeat agindurako metodoa .................................................. 65
Iterazioen ez-bukaera ........................................................... 66
Ariketak........................................................................................... 69
Array-en osagaiei egindako asignazioa (AOA) ........................... 72
For agindua (FORE) ............................................................ 73
For-downto agindua (FORE) ................................................. 77
Erregistroen eremuei egindako asignazioa eta WITH
sententzia (WTE) ................................................................ 77
Fitxategiak eta sarrera/irteerako aginduak ................................. 80
Ariketak .......................................................................................... 84
Parametrorik gabeko prozedurak (PGPE).................................. 87
Kontserbazioaren axioma (K.A.) ............................................ 88
Konjuntzioaren erregela (K.J.E.) ........................................... 88
Prozedura parametrodunak (PPE) ............................................ 90
Funtzioak (FUNE) .............................................................. 98
Ariketak .......................................................................................... 103
5. Gaia. PROGRAMA-ERATORPEN FORMALA .................................. 105
5.1. Metodoaren filosofia, interesgarritasuna eta mugak ........................... 105
Aurkibidea __________________________________________________________ VII
5.2. WP predikatu-transformatzailea ..................................................... 106
Aldagai sinpleei eginiko asignazioa ............................................... 107
Array-en osagaiei eginiko asignazioa ............................................. 107
Sekuentzi konposaketa ................................................................ 107
Baldintzazko agindua ................................................................... 109
Ariketak........................................................................................... 111
Iterazioak .................................................................................. 112
Beste sententzia batzuk ................................................................ 125
Metodoaren aplikazioak ............................................................... 127
Ariketak .......................................................................................... 138
6. Gaia. ALGORITMO ERREKURTSIBOAK......................................... 139
6.1. Indukzio estrukturala .................................................................. 139
6.2. Algoritmo errekurtsibo zuzenen diseinua ........................................ 144
Algoritmo errekurtsiboen zuzentasun-azterketa ................................. 156
Algoritmo errekursiboen egiaztapena .............................................. 161
Funtzio Errekurtsiboen Egiaztapena (FERRE) ................................. 162
Prozedura Errekurtsiboen Egiaztapena (PERRE) ............................... 163
6.3. Argitasun/eraginkortasun erlazioa errekurtsioaren erabileran ................ 166
Ariketak........................................................................................... 169
6.4. Burstall-en metodoa .................................................................... 170
Ariketak .......................................................................................... 177
BIBLIOGRAFIA ............................................................................... 179
Sarrera ____________________________________________________________ 1
SARRERA
Programazioaren hastapenetan makina-lengoaian idazten ziren programak. Ez
zegoen beste aukerarik, konputagailuak ezin bait zezakeen kode bitarrean idatzikoaz
besterik ulertu. Sasoi hartan nola-halako notazio sinbolikoa erabiltzen zen makina
eragiketak eta, hauek kateatuz, programak idazteko.
Pixkanaka, mihiztadura-lengoaiak sortu ahala, kode sinboliko hori makina-kodetik
urruntzen hasi zen. Lengoaia hauetan idatzitako kodea programa itzultzaileen bidez
(mihiztatzaileak) makina-kodera pasatzen zen. Makinatik urrundu bai, zertxobait urruntzen
zen mihiztadura-kodea, baina hala ere menpekotasun edo lotura estua zeukan makinarekiko;
hain estua ezen lengoaiako primitiboak makinaren oinarrizko hardware-eragiketak bait
ziren. Hitz gutxitan esateko, programagintza astuna zen, metodorik gabea, errore-arrisku
oso altukoa eta hauen detekzio eta arazketa benetan nekosoa.
Gauzak honela, alegiazko makina erosoago baten premia nabarmendu zen, edo, nahi
bada, erabilgarriago gertatuko zen programazio-lengoaia batena.
Diseinu-ahaleginak 1945ean hasi ziren, eta lan horien fruitu gisara 50.
hamarkadaren bukaera aldera agertu ziren estraineko programazio-lengoaiak. FORTRAN
izan zen lehenengoa, 1954 eta 1957.aren artean John Backus eta bere IBM taldeak garatua,
eta benetan eragin handikoa. Harrera eszeptikoa egin zitzaion, ez bait zen uste hain goi-
-mailako lengoaia eraginkorra izan zitekeenik, eta horregatixe ez zen inguru
akademikoetatik atera harik eta Backus-en taldeak konpiladore egokia sortu eta behe-
-mailako kodeekin bezain emaitza onak lortu zituen arte. Orduantxe eman zuten ameto
eszeptikoek. Egia esatera, FORTRAN horrek mihiztadura-lengoaien ezaugarri askotxo
zituen.
Garaitsu hartan (50.en bukaera eta 60.en hasieran) lengoaia ugari jaio zen: ALGOL,
COBOL, APL, BASIC, LISP. Guztiek, LISP-ek izan ezik, bazuten FORTRAN
lengoaiaren eraginik eta, modu batera edo bestera, hura hobetzeko asmotan sortu ziren:
programen irakurgarritasuna zela, datuen erabilpena zela, e. a.
Ugalketa horrek eztabaidari eta, bidenabar, lengoaien arteko alderaketari eman zion
bidea. Ingurune honetan sortu zen programazio-lengoaia unibertsalaren ideia eta halaxe jaio
zen 1965ean PLI lengoaia. Esperientzia honek ederki erakutsi zuen benetan zaila zela
"denetarako" balio zuen lengoaia ikasi eta ondo erabiltzea. Nabaria zen aplikazio-arlo
desberdinetan lengoaia berezituak behar zirela.
2 ______________________________________________________________________
Garai hartako literatura ("Programming in Basic", "Programming in Fortran IV")
ikusi besterik ez dago konturatzeko benetan garrantzizkoak lengoaiak zirela. Programatzen
jakitea programazio-lengoaiak jakitea zen, eta ez besterik. Programatzaileak bere kaxa
ikasten zituen oinarrizko arauak, askotan aritzeak ematen duen eskarmentura mugatzen
zirenak.
60. hamarkadan aplikazioen konplexutasuna, tamaina eta garrantziak gora egin
zuten arren, ez zen gauza bera gertatu programatzaileen iaiotasun eta tresneriarekin.
Programa gutxi eta eskasak egiten ziren, eta denbora gehiago behar izaten zen errore-
arazketan programak sortzen baino. Egoera penagarri horrek bultzatuta, 1968ko Urrian
"Software Engineering" izeneko konferentzia ospatu zen Garmisch-en (Alemanian)
NATOren babespean. Bilera hartan "Softwarearen krisiaz" hitz egin zen, hau da, beharren
eta metodoen arteko desorekak sortutako krisiaz. Bildutakoak, akademiko nahiz industri
gizonak, adostasun batera ailegatu ziren: "Softwaregintza krisian badago programazioa
orain artean gaizki ulertua izan delako da". Planteamendu horrek aurrekoarekin apurtzea eta
bide berrietatik abiatzea ekarri zuen. Urtebete barru, 1969an, IFIP elkarteak Working
Group 2.3 lan-taldea sortzea erabaki zuen, "programazio-metodologia" lantzera dedikatuko
zena, hain zuzen ere.
Talde horrek erro-errotiko aldaketak proposatu zituen: utikan artisau lana, egin
dezagun programazio zientifikoagoa! Ikusmolde horrek bi oinarri ditu:
1.- Programa baten ezaugarri nagusiak honako hauek izan behar dute: zuzentasuna,
argitasuna, aldagarritasuna eta eraginkortasuna.
2.- Programatzaileak behar-beharrezkoa du bere lana erraztuko duen tresneria eta oinarri
teorikoa.
Pentsamolde honen haritik eratorritako programazio-estiloari "Programazio
Egituratu" deitu zitzaion. Bazirudien, hasieran izandako zenbait eztabaidaren arabera
behinipehin, programazio egituratua go to agindurik gabe programatzea baizik ez zela.
Luzagabe argitu zen, ordea, hori baino zerbait gehixeago zela programazio egituratuaz
ulertu behar zena.
Hortik aurrera ez ziren falta izan era guztietako ekarpenak, hala nola, programazio-
-lengoaiak, programen disenurako metodologiak, e. a.
1970ean PASCAL programazio-lengoaia jaio zen, N. Wirth-ek diseinatua.
Lengoaia honetan notazio hobeak, kontrol-egitura argiagoak eta datuen definizio eta
maneiurako erraztasunak bildu nahi ziren. Gerora, PASCAL lengoaia hainbat
programazio-lengoaia agintzaileren aurrekaria gertatu da, esate baterako, MODULA-2 eta
ADArena.
PASCAL-arekin batera abstrakzioaren kontzeptua programazioaren mundura
ailegatu zen. Abstrakzio funtzionalak ebatzi beharreko problemaren konplexutasuna
Sarrera ____________________________________________________________ 3
zatikatzeko aukera ematen zuen. Problemari bere osotasunean aurre egin beharrean, zatika,
aldiro problemaren aspektu batzuk ebaztean, eta gainerakoei itzuri egitean, datza
abstrakzioa. Honelaxe plazaratu zuen N. Wirth-ek ondoz-ondoko finketen metodoa 1971n.
Ordutik aurrera programazio-metodologiaren funtsa hauxe izan da: programatzea ez da
soilik programak idaztea. Programen idazketa, izatekotan, analisi eta diseinu prozesuaren
azken urratsa da, eta prozesu hori metodo ordenatu batez burutu behar da, ez nola edo hala.
Ondoz-ondoko finketen metodoak berebiziko eragina izan du geroztik formulatu diren
metodoetan, esate baterako, gestiorako programen diseinuan ere beheranzko metodoa
erabiltzen da, Warnier metodoan kasu.
Programen zuzentasuna egiaztatzeko metodoek ere, ez soilik probetan
oinarritutakoek, piztualdi polita ezagutu zuten testuinguru honetan. Lehendik ere, 1949an,
A. Turing-ek plazaratua zuen behar hori, bereziki bere metodoa aurkeztu zuenean. Bada bai
ildo honetan lan egin duen aitzindaririk, besteak beste, McCarthy, Naur eta Floyd aipa
daitezke. Floyd-ek, 1967an, Turing-en ideian oinarritutako metodoa aurkeztu zuen, baina
asertzio gisa aldagaien balioak erlazionatzen zituzten formulak erabili zituen. Guzti horren
buruan inor gutxik jartzen zuen zalantzan programen fidagarritasuna hobetzearen beharra
eta, halaber, testak soil geratu eta ez zirela nahikoa. Dijkstra-k zioen bezala, probek
programak erroreak badituela froga dezakete, baina ez ordea erroregabea denik. Horretan
dago, hain zuzen, koxka; horregatik da hain interesgarria programak egiaztatzea.
1969an, Hoare-k, Floyd-en ideiak berreskuratuz, axioma eta inferentzi erregelatako
sistema formala eratu zuen. Sistema honek programen zuzentasun formala frogatzeko balio
du eta asertzio inbarianteen metodoaren euskarria da.
Geroztik programen zuzentasuna formalki frogatzeko zenbait metodo azaldu da, hala
nola, "aldizkako asertzioena" edo semantika denotazionalean oinarritutakoa. Baina
guztietan erabiliena Hoare-ren kalkulua izan da ezbairik gabe.
Handik laisterrera, ondoz-ondoko birfinketen diseinu-metodoa eta asertzio
inbarianteen egiaztapen-metodoa ezkontzeko asmoa sortu zen. Asmoa sinplea zen:
arrazoizkoa da, eta eraginkorragoa gainera, programa egin ahala zuzena dena frogatzea, bi
eginkizunak, diseinua eta egiaztapena, ideia beretsuen garapenak bait dira. Horrez gain,
programagintza-metodo horrek aukera aparta eskaintzen du diseinuaren propietateak eta
erabilitako ideiak ondo dokumentatuta uzteko, eta hori bai dela eskertzekoa programen
mantenimendu-fasean.
Dijkstra-k programen eratorpen formala izeneko metodoa planteatu zuen 1975ean,
hau ere Hoare-ren kalkulutik eratorritakoa. Metodo horren arabera, programaren helburua
espezifikazio jakin bat betetzea da eta horretara zuzendu behar da diseinua.
Espezifikazioaren ondoko baldintzak, batetik, lortu nahi den emaitza nolakoa den
adieraziko digu eta aurreko baldintzak, bestetik, datuek bete behar dituzten murriztapenak
4 ______________________________________________________________________
finkatuko ditu. Programazioa hala planteatuz gero ondoko baldintza bihurtzen da
diseinuaren gidari, baina, hori bai, diseinuak eskatzen dituen gutxienezko betebeharrak
aurreko baldintzak biltzen dituela aurreikusiz. Funtsezko ideia eta formalismoa Dijkstra-k
azaldu bazuen ere, Gries izan zen espezifikaziotik abiatuta programak eratortzeko metodoa
gehixeago landu eta ezagutzera eman zuena.
Programen eraldakuntzak ere badu zeresanik aipatzen ari garen arrazonamendu eta
zuzentasunaren egiaztapenean oinarritutako metodologian. Normalean, eraldatu, programa
sinpleak eraldatzen dira, espezifikazioa betetzen dutenak baina eraginkorrak ez direnak.
Programa horien semantika babestuz (zuzentasunari eutsiz) baliokide eraginkorragoak lortu
nahi izaten dira. Ez da, beraz, beheranzko metodoa, horizontala baizik. Gehienetan,
programa eraginkorrak ulergaitzak dira, eta zaila izaten da zuzentasunari buruz arrazonatzea.
Horrelakoetan, askozaz erosoagoa gertatzen da jatorrizko programa zuzena zela eta
eraldaketak zuzentasunari eusten diola egiaztatzea.
Egia da programa-eraldakuntzak programa batetik besterako pausoa ematen duela eta
ez espezifikaziotik programarakoa. Eraldakuntzan ere badira, ordea, espezifikazioaren eta
egiaztapenaren beharra duten problema batzuk, txukun ebatziko badira behintzat.
Eraldaketak programen zuzentasuna kontserbatzen duela frogatu nahi bada, esate batera,
beharrezkoa da programaren espezifikazioa ezagutzea eta egiaztapen-teknikak erabiltzea.
Gainera, zenbait eraldaketak ez du, murriztapenik ezarri ezean, zuzentasuna beti
kontserbatzen.
Programa errekurtsiboak gehientsuenetan sinpleak eta ulerterrazak dira, baina baita
ez-eraginkorrak ere. Ez da harritzekoa, beraz, errekurtsibo-iteratibo ereduko eraldakuntzak
izatea gaur egun erabilienak eta landuenak.
Programen sintesia edo programazio automatikoa ere espezifikaziotik hasi eta
programa sortzera jotzen duen metodoa da, baina kasu honetan adimen artifizialaren
inguruko teknikak erabiltzen dira. Batzuetan, espezifikazioa lengoaia funtzionalean idazten
denean, sintesia ez da programa-eraldakuntza mekanizatua baizik. Beste batzuetan,
espezifikaziotik programa bat lortzen da zuzenean eta gero programa hori hobetu egiten da
programa-eraldakuntzaz.
Programen egiaztapen-prozesuak dituen aspektu mekanikoenak automatizatzeko
joerak, ikerkuntz adar berri bati eman zion sorrera egiaztapenaren alorrean. Programazio-
inguruneetan tresna berri bat integratu nahi zen: egiaztapen-sistemak; eta hartara
programen zuzentasun semantikoa egiaztatzeko erraztasunak eskaini. Hamaika ahalegin
egin da 70.etik aurrera egiaztapen-metodo mekanizagarriak deskribatzeko eta egiaztapen-
sistema batzuk eraiki ere egin dira, baina elkarrekintzazkoak eta esperimentalak dira
oraingoz. Etorkizunean egiaztapen-sistemak programazio-ingurune integratuetako osagaiak
izango dira, editoreak, konpiladoreak eta liburutegiak bezalaxe.
Sarrera ____________________________________________________________ 5
Abstrakzioarekin zerikusia duen beste programazio-metodo inportantea programa-
eskematan oinarritzen dena da. Programa-eskema algoritmo generikoa da, ekintza, funtzio
eta objektu abstraktuak (interpretatu gabeak) dauzkana.
Programa-eskemek ideia zahar batean dute jatorria: ebatzi nahi dugun problemak
beste batekin erlazio estua badu, eta azken honen ebazpena ezaguna bada, ebatzi dezagun
jatorrizkoa bigarrenean oinarrituta.
Azken finean, algoritmo askok portaera beretsua dutela aipatzen duten liburuak
programa-eskemen erabileraz ari dira, nahiz eta ez duten diseinu-metodo hau esplizituki
aipatzen.
Dijkstra-k "programa-familiak" aipatzen ditu egoki baino egokiago, hau da,
algoritmo abstraktu batetik (oraindik birfintzeke dagoena) erator daitezkeen programak
jotzen ditu senide eta hauek, bere ustetan, problema-mota (edo familia) bati aplika
dakizkioke. Eskema bera, jatorrizko algoritmo abstraktua alegia, dokumentazio ezin
aproposagoa da mantenimendu-faserako.
Eskemen bidezko programa-diseinurako problemak klaseka bildu behar dira,
ebazpidean erabiltzen diren ezaugarri komunen arabera. Honela, behin problema klaseren
batean sailkatuta, programa-eskema zehatz bat aukeratzen da ebazpenerako, eta eskema
horretatik ekintzak eta objektu abstraktuak birfindu beste lanik gabe, programa lortzen da.
Orain artean azaldutako programazio-metodologiaren aspektu horietan oinarritu gara
liburu honen edukia mamitzean. Esan behar da, gainera, programazioaren inguruko
ikerkuntz lerro nagusiak ingurune horretan ari direla garatzen gaur egun.
Hemen jasotzen den materiala programazioko 2. mailara zuzenduta dago eta bertan
programazio agintzailearen oinarrizko ezagutza duen irakurleari programazio metodikoaren
bidea erakutsi nahi zaio. Garrantzizkoa deritzogu bide hau urratzeari, izan ere, Dijkstra-k
esan zuen bezala, zaila bait da artisau-programazioan ohituta dagoenari programazio
metodikoaren komenientzia ikustaraztea.
Gure iritziz, programatzea ez da "funtzionatzen" duten programak idaztea soilik.
Hori baino areago, programei argitasuna, moldagarritasuna, dokumentazio aproposa,
eraginkortasuna eta estilo horretako ezaugarriak eskatu behar zaizkie.
Programatzea ez da iharduketa nabaria, ezta sinplea ere. Ezin da edozein moduz
programatu, baizik eta lagungarri gertatuko diren tresneria eta ezagutza egokiez baliatuta.
Programen diseinu-prozesuak ideien antolaketa eta zorroztasunez egindako azterketa
eskatzen du derrigor. Hala egiteak, zenbaitetan bederen, programazioa zaildu egiten duela
eman lezake, baina egiaz diseinu-erroreak egiteko arriskua txikitu egiten du (hauek dira
gainera detektatzeko eta zuzentzeko gaitzenak) eta ondorioz programazio-lana erraztu.
6 ______________________________________________________________________
Horrez gain, txukun arrazonatu eta eratutako diseinua da izan daitekeen
dokumentaziorik egokiena, eta aspektu inportanterik bada programazioan, horietako bat
dokumentazioa da.
Behin problemaren ezaugarriak aztertuta, komeni da programazio-metodo egokiena
aukeratzeko gai izatea. Baina horretarako beharrezkoa da metodo eta kontzeptu desberdinak
noiz eta nola erabili behar diren jakitea.
Sarrera gisako honetan ukitu ditugun aspektu hauetako batzuk lantzen dira liburuan
zehar, beti ere programa zuzen, argi, eta ulergarriak idatzi nahi dituenari laguntza eskaini
nahian.
Espezifikazioa __________________________________________________________ 7
1. ESPEZIFIKAZIOA
1.1. ZER DA ESPEZIFIKAZIOA
Espezifikazioa, hiztegiek diotenez, egin beharreko lanaren deskribapen zehatza da.
Baina, baieztapen hau emanez gero:
"... LA (lerro-amaiera) karakterearen bidez banantzen diren lerroez osatutako testua
emanda, bertatik irazkin guztiak, hau da, `(´ eta `)´ karaktereen arteko sekuentzia guztiak
ezabatzen dituen programa..."
Deskribapen zehatza al da? Bistan da deskribapena dela, ez zehatza ordea. Inork
programa hau egin behar balu, edo egindakoren bat ulertu, berehala hasiko litzateke
galdezka:
- Nola detektatzen da testu-amaiera?
- Egon al litezke irazkin okerrak? hau da, ixten ez diren parentesi irekiak edo
alderantzizkoak?
- Litekeena al da irazkin kabiatuak egotea?, eta irazkin hutsak?
- Zer egiten du (edo zer egin beharko luke) programak balizko irazkin okerren aurrean?
- Irazkinak ezabatzean hutsunerik utzi behar al da? Ezezkoan, gehienez ere zenbat karaktere
jar daitezke lerro berean?
Aldiz, aurreko enuntziatuaren ordez beste hau idatzi izan balitz:
datuak: Karakterez osatutako testua, non karaktereak honela sailkatzen bait dira:
- Testu-amaiera: TA
- Lerro-amaiera: LA
- `(´ eta `)´ parentesiak
- Karaktere arruntak: gainontzekoak, ondoko baldintza hauen pean:
- TA behin agertzen da eta beti azkena
- Lerro bakoitza, gehienez ere, 80 karakterez osatzen da.
- `(´ eta `)´ karaktereen arteko sekuentziak kabia daitezke.
emaitzak: testua, non:
- Karaktere-sekuentzia sarrerako testuaren berdina bait da; `(´ , `)´ eta hauen
artekoak, eta LA izan ezik. Guzti hauek ezabatu egiten dira ordezko
karaktererik idatzi gabe.
- `(´ eta `)´-aren arteko sekuentziak kabia daitezke.
8 ______________________________________________________________________
- Ixten ez diren parentesi irekiek edo alderantzizkoek (ireki gabe ixten
direnek) programa amaiarazi egiten dute errore-mezu batez.
- Lerro bakoitza, gehienez ere, 80 karakterez osatzen da.
Honako hau espezifikazotzat onar daitekeen deskribapen zehatzagoa da.
Espezifikazio kontzeptuak zerikusi zuzena du abstrakzioarekin. Abstrakzioa
programak modulutan banatzeko erabiltzen da, baina ulergaitz gertatzen da ez badago
deskribatuko duen espezifikaziorik.
Datu edo sarrera-objektuen funtzio gisa uler daiteke programa bat, emaitza edo
irteera-objektuak lortzeko helburuarekin. Programa bat abstrakzio funtzional baten
inplementazioa da. Abstrakzio funtzional bat era desberdinetan inplementa daiteke, baina
guztiek bete behar dute espezifikazioa. Hots, espezifikazioak abstrakzio funtzionala
definitu edo deskribatzen du, eta inplementatzen duen programak, bestalde, funtzio hori
kalkulatzeko modu bat definitzen du. Espezifikazioa, sarrera-objektu posibleen eta
dagozkien irteera-objektuen arteko erlazioaren deskribapen zehatza da.
1.2. ZERTARAKOAK
Gaur egun espezifikazioa informatikako hamaika alorretan ageri da. Batetik, edozein
programaren diseinurako premiazkoa da ebatzi beharreko problemaren ezagutza zehatza
(anbiguetaterik gabea) edukitzea diseinuari ekin aurretik; izan ere, diseinatu ahala
adabatzeak akats ugari sortzen bait du. Problema espezifikatzeak ideiak egituratzera
behartzen gaitu eta aspektu nabariak agerian uztera bidenabar. Aspektu hauek,
espezifikazioan ez bada, diseinuan agertzen dira edo, are okerrago, ez dira agertzen, eta
orduan programa desegokia izango da, ez bait du nahi dugun problema ebatziko.
Talde-lanei dagokienez espezifikazioak komunikazio-disziplina eragin behar du.
Modulutako banaketa sistemaren eginbeharrak zehatz-mehatz ezagutuz egin behar da eta
modulu bakoitzeko diseinatzaileak, bai ebatzi beharreko problema, bai beste moduluekiko
elkarrekintzak, inolako anbiguetaterik gabe ezagutu behar ditu.
Programen testak diseinatzeko ere ezinbesteoak dira espezifikazioak, bereziki "kutxa
beltza" izeneko testetan.
Bestalde, ez dugu ahantzi behar programak behin egin eta askotan irakurtzen direla.
Programa baten mantenimendurako beharrezkoa da dokumentazio aproposa edukitzea,
edozeinek programa horrek zer egiten duen zehazki uler dezan aparteko ahaleginik gabe.
Gerora ere, aldaketaren bat burutu beharko denean, ezinbestekoa izango da dokumentazioa.
Kontutan hartu, aldaketa hauek egiten dituena eta hasierako diseinua egin zuena normalean
ez direla pertsona bera izaten.
Espezifikazioa __________________________________________________________ 9
Programen egiaztapenerako ere espezifikazioak dira abiapuntua, azken finean
programak egiaztatzea espezifikazioak betetzen dituztela formalki frogatzea bait da, hau da,
diseinatu zeneko eginbeharrak betetzen dituela frogatzea. Beraz, espezifikazioak,
egiaztapenean oinarritzen diren programen diseinu-metodologien abiapuntua ere badira.
Programen sintesia, espezifikazioan oinarrituz programak era automatikoz sortzean
datza. Azkenik, espezifikazio-lengoaia exekutagarriak ere baditugu, hau da, programazio-
lengoaia bilakatu diren espezifikazio-lengoaiak, nolabait problemaren deskribapena
egikaritzen dela.
1.3. ESPEZIFIKAZIO-LENGOAIAK
Espezifikazioak hainbeste zereginetan erabiltzeak espezifikazio-lengoaien ugaltzea
ekarri du: nolako helburua, halako idazkera aproposa. Edozein lengoaia definitzerakoan bi
aspektu hauek hartu behar dira kontuan:
* Sintaxia: Zer idatz dezakegu?
* Semantika: Zer adierazten du idazten dugunak?
Lengoaia bat formaltzat hartuko dugu baldin eta bere sintaxia eta semantika
formalki definituta badaude (zehaztasun matematikoz). Helburuak baldintzatuko du
lengoaiaren formaltasun-maila: taldeen arteko komunikaziorako, test-diseinurako edo
dokumentaziorako lengoaia ez oso formala nahikoa izan daiteke; baina egiaztapenerako,
programen sintesirako edo espezifikazioen exekuziorako ezinbestekoa da lengoaia formala,
espezifikazioak matematikoki eta/edo automatikoki tratatzen bait dira.
Espezifikazio formalek esanahi zehatza bermatzen dute. Aldiz, espezifikazio ez-
formalak errazago idatzi edo irakurtzen dira, baina zaila da esanahi guztiz zehatza adieraztea.
Espezifikazio-lengoaia formalek nahiz ez-formalek ondoko ezaugarriak bete behar
dituzte:
- Argitasuna: Espezifikazio ulerterrazak (lengoaia ezagutzen duen edonorentzat).
- Laburtasuna: Ahalik eta laburrenak, erredundantziarik gabekoak.
- Zehaztasuna: Anbiguetateak uxatzen dituztenak.
- Murriztasuna: Inplementazio onartezinak ametitzea ekiditen dutenak.
- Orokortasuna: Premiagabeko baldintzarik ez, espezifikazioek ez dute inplementazio onar-
garririk baztetu behar.
Azken bi ezaugarriek, abstrakzio funtzionalen funtsezko aspektuak juxtu-juxtu
definitu behar direla adierazten dute, axolagabeko xehetasunak albo batera utziz.
10 _____________________________________________________________________
1 . 3 . 1 . Espezifikazio ez-formalak
Espezifikazio ez-formalerako teknika batek edozein abstrakzio funtzionalen aspektu
nabariak klausulen bidez adierazteko formatoa finkatzen du. Moldea bai, baina klausulak
adierazteko lengoaia formalik ez du ezartzen. Espezifikatzen duenaren esku geratzen da,
hortaz, notazio matematiko eta/edo teknikoaren hautaketa, lengoaia naturalaren laguntzaz
deskribapen argiak, laburrak eta zehatzak idatzi ahal izateko.
Ikus dezagun espezifikazio ez-formalerako teknika bat:
- espezifikazioa: < abstrakzio-funtzional-izena >
- datuak: < datuen-mota-eta-izena >
- emaitzak: < emaitzen-mota-eta-izena >
- aldatuak: < aldatu-diren-datuak >
- aurreko-baldintza: < datuen-murriztapenak >
- eragina: < portaeraren-deskribapena >
- salbuespenak: < aurrikusten-diren-salbuespen-kasuen-deskribapena >
Metodo honen ideia, batetik, sintaxia karakterizatzea da, datuetatik emaitzerako
funtzio matematikoari abstrakzio funtzional bat egokituz, eta horretara daude zuzenduak,
hain zuzen, lehen hiru klausulak. Bestetik, semantika ere karakterizatu behar da, hau da,
sarrera eta irteeraren arteko erlazioa, eta hauxe da lau azken klausulen helburua.
Aurreko-baldintza klausulak funtzioaren eremua mugatzen du (funtzio partzialak)
eta aldatuak klausularen bidez abstrakzio funtzionala eta funtzio matematikoa desberdintzen
dira, abstrakzio funtzionalak aldatzen dituen datuak aipatuz. Azkeneko bi klausuletan
abstrakzio funtzionalak normalki duen eragina eta salbuespen-kasuen arteko banaketa
egiten da. Ikus ditzagun adibide batzuk, horietan nabarmentzen bait da klausulen egitekoa
eta espezifikazioen ezaugarriak ondo betetzearen garrantzia.
1.1. adibidea: Bi zenbaki arrunten arteko zatidura osoa kalkulatzen duen ekintza
abstraktua espezifikatu.
Enuntziatu hau irakurrita bi galdera nagusiri erantzun beharrean aurkitzen gara:
Zatitzailea zeroa izan al daiteke? Emaitza non utziko dugu?
Horra aukeratu dugun erantzuna:
- espezifikazioa: ZATI
- datuak: x,y : osoak
- emaitzak: z : osoa
- aldatuak: (ez dago, honelakoetan klausula hau ez da jartzen)
- aurreko-baldintza: x 0 eta y > 0
- eragina: z = e zenbaki oso haundiena, non e x/y
- salbuespenak: (salbuespen-kasurik ez dagoenez klausula hau idatzi beharrik ez dago)
Espezifikazioa _________________________________________________________ 11
Aurrekoaren bariantea, x eta y-ren arteko zatidura kalkulatu eta x-n emaitza uzten
duena:
- espezifikazioa: ZATIM
- datuak: x,y : osoak
- emaitzak: x : osoa
- aldatuak: x
- aurreko-baldintza: x 0 eta y > 0 eta x = a
- eragina: x = a/y
Nola erabili aldagai aldatuen hasierako balioak? Abstrakzioaren eragina adierazteko
beharrezkoa da balio hauen erabilera finkatzea eta, horretarako, aukera bat baino gehiago
proposatzen da.
Autore batzuek Xaurre, Xondo edo X, X' bezalakoen bidez adierazten dituzte X
aldagaiaren hasierako eta bukaerako balioak, hain zuzen notazio-arazoa besterik ez bait da.
Guk erabiliko dugun notazioa aurreko baldintzan hasierako balio sinboliko bat ematean
datza.
1.2. adibidea: Array bat eta elementu bat emanda, elementu hori aurkitzen deneko
posizioetako bat itzultzen duen ekintzaren espezifikazioa.
- espezifikazioa: BILA
- datuak: A : array [1..n] osozkoa; t : osoa
- emaitzak: i : osoa
- aurreko-baldintza: n 1
- eragina: 1 i n eta A[i] = t
- salbuespenak: i=0, baldin A[j] t edozein 1 j n-rentzat
Hauxe da espezifikazio orokorrena, baina ez litzateke onargarria izango elementua ageri den
lehenengo posizioa lortu nahi bagenu; kasu honetan murriztaileagoa egin beharko genuke:
- eragina: 1 i n eta A[i] = t eta A[j] t edozein 1 j < i-rentzat
1.3. adibidea: Osozko sekuentzia baten azken zenbaki negatiboa eta dagoen posizioa
kalkulatzen duen abstrakzio funtzionala espezifikatu:
- espezifikazioa: AZKENG
- datuak: : osoak
- emaitzak: i, x : osoak
- aurreko-baldintza: k 1 ( k 0 sekuentzia hutsa onartuz gero)
- eragina: 1 i k eta x = ei < 0 eta ei+1,...,ek 0
- salbuespenak: i = 0 eta x = 0, baldin e1,..., ek 0 (edo k = 0)
12 _____________________________________________________________________
Parentesien bidez, lengoaia naturaleko enuntziatuan argi ez dauden aspektu
desberdinak aukeratu ditzakegula adierazten da.
Orain arteko adibideek garbi asko erakutsi digute zein den espezifikazio ez-
-formalerako teknika honek eskatzen duen erabilera. Hala ere, enuntziatu labur eta ulerkor
hauetan ez da benetan nabarmentzen espezifikazioaren komenientzia eta teknika honen
interesa. Ondoko adibedeetan erraz konprenitzen da zenbateraino den inportantea notazio
egokiz eta txukun espezifikatzea, enuntziatuak berak konplexuak edo ilunskak direlako,
hain zuzen ere.
1.4. adibidea: Jo dezagun ondokoa burutzen duen programa espezifikatu behar dugula:
$ ikurraz banantzen diren N elementutako azpisekuentziez osatutako zenbaki osoen
fitxategia emanda (azken azpisekuentziak N elementu baino gutxiago edukiko ditu)
kalkulatu azpisekuentzien kopurua, azken azpisekuentziaren luzera eta elkarren segidan
dauden zenbaki berdinen lehenengo bikotea eta, bestalde, azpisekuentzia bakoitzarentzat, ea
azpisekuentziaren elementurik txikiena eta handienaren arteko zenbaki lehen guztiak dauden
ala ez eta zero baten atzetik doazen elementu bikoitien kopurua.
Espezifikatzen hasitakoan, dudarik ez, zalantzak sortuko litzaizkiguke:
- N zenbakia datu gisa hartu behar al da?
- $ ikurraz hasi eta bukatzen al da sekuentzia?
- Azpisekuentzia hutsak onartuko al dira? Eta azpisekuentziarik ez egotea?
- Elkarren segidako al dira $ ikurra tartean duten zenbakiak?
- Elkarren segidan dauden zenbaki berdinen bikoterik ez badago, zer egin behar du
programak?
Galdera guzti horiei erantzun eta programaren eginbeharrak zehazten dituen
espezifikazioa hauxe izan daiteke:
Espezifikazioa _________________________________________________________ 13
- espezifikazioa: AZPISEK
- datuak: N: osoa,
S: < $ as1 $ as2 $ ... $ ask $ >, non
asi = < ei1 , ei2 , ... , eiN > edozein 1 i < k-rentzat
ask = < ek1 , ek2 , ... , ekL >
eiz : osoak
- emaitzak: zenbatas, luzazk: osoak,
bikote: osoak x osoak,
n1, n2, ... , nk: osoak,
b1, b2, ... , bk: boolearrak,
- aurreko-baldintza: k 0 eta 0 L < N eta N > 0
- eragina:
zenbatas = k
luzazk = L
bikote = ( eiZ , eiZ+1 ) non eiZ = eiZ+1 eta
epm epm+1 honakoetan:
p < i eta 1 m < n
edo
p = i eta 1 < m < z
Edozein 1 i k-rentzat:
ni = kard { ( eiZ , eiZ+1 ) / eiZ = 0 eta eiZ+1 bikoitia da }
bi = true b.s.b. asi { x / x lehena da eta min (asi) x max (asi) }
- salbuespenak:
baldin epm epm+1 bada edozein p,m-rentzat, orduan:
bikote = ( 0 , 1)
1.5. adibidea: Demagun damen antzeko joko batean ari diren bi jokalarien iharduera
gestionatuko duen programa bat diseinatu behar dugula. Bi jokalariek ordenadorea aukeratu
dute euskarri bezala, teklatutik adierazten dituzte beren mugimenduak eta pantailaz
baliatzen dira unean-uneko jokoaren egoera ikusteko. Damen antzeko jokoa diogu, izan ere
ia-ia dametan ari bait dira baina bi mugapen ezarri dituzte: ez da derrigorrezkoa jatea eta
aurkako eremuaren azken muturrera iristen diren fitxei ez zaie mugimendu-ahalmen
berezirik ematen.
14 _____________________________________________________________________
Delako programak, jokoaren gestioa behar bezala burutu nahi badu, hainbat gauza
eduki beharko ditu kontuan: nori dagokion jokatzea, jokaldien irakurketa, ea jokaldiak
legezkoak diren, ...
Lehenbiziko hurbilpen gisa honako algoritmo abstraktu hau eman genezake:
begin
HASIERAKO_EGOERA (e);
MARRAZTU_EGOERA (e);
HASIERAKO_TXANDA (tx);
while not JOKOAREN_BUKAERA (e) do
begin
IRAKUR_JOKALDIA (jok);
if LEGEZKO_JOKALDIA (e, jok, tx) then
begin
JOKALDIA_BURUTU (e, jok, tx);
TXANDA_ALDATU (tx);
MARRAZTU_EGOERA (e)
end
else IDATZ_MEZUA (tx)
end;
IRABAZLEA (e)
end.
Algoritmo honetan e: EGOERA, jok: JOKALDI eta tx:TXANDA aldagaiak erabili
dira, oraindik mota horiek espezifikatu gabe badaude ere.
Diseinuaren jarraipenak ekintza abstraktuak birfintzea eskatzen du, baina hori baino
lehenago ezinbestekoa da ekintza horiek espezifikatzea. Bestela, zer egiten duten zehaztasun
handiz jakin gabe, nola birfinduko ditugu? Egia da ekintzen izenek nola edo hala
eginkizunaren ideia iradokitzen dutela, baina hori ez da nahikoa.
Espezifikatzera joko dugu, beraz, baina horretarako beharrezkoa da erabilitako datu-
motei buruz zerbait gehiago jakitea.
EGOERA motako aldagaiak 8x8 matrizeak izango dira, eta bertan taulatuko
laukitxo guztien berri jasoko da, hau da, eiZ bakoitzak (1i,z8) 'T', 'B' edo ' ' balioak har
ditzake, (i,z) laukitxoan fitxa txuria, beltza edo fitxarik ez dagoela adierazteko. EGOERA
datu-mota beste zenbait informazioz ere aberastu daiteke, esate baterako, jokalari bakoitzak
zenbat fitxa dauzkan edo zenbat jokaldi pasa diren elkarri jan gabe adieraziz. Aspektu hauek
beharrezko gerta daitezke hainbanaketa noiz gertatzen den antzemateko.
Espezifikazioa _________________________________________________________ 15
JOKALDIA = LAUKITXO x LAUKITXO izango da, lehenengoa jatorrizkoa eta
bigarrena helburu-laukitxoa. Halaber, LAUKITXO = OSOA x OSOA izango da, errenkada
eta zutabea adieraziz hurrenez hurren.
TXANDA = ('T', 'B') hartuko dugu.
Ikus ditzagun, bada, HASIERAKO_EGOERA eta LEGEZKO_JOKALDIA
ekintzen espezifikazioak:
- espezifikazioa: HASIERAKO_EGOERA
- emaitzak: e:EGOERA
- eragina:
eiZ = 'T' baldin eta ondorengo kasuren bat gertatzen bada:
a) (i = 1 edo i = 3) eta z bakoitia, 1 z 8
b) i = 2 eta z bikoitia, 1 z 8
eta
eiZ = 'B' baldin eta ondorengo kasuren bat gertatzen bada:
a) (i = 6 edo i = 8) eta z bakoitia, 1 z 8
b) i = 7 eta z bikoitia, 1 z 8
eta
eiZ = ' ' gainontzeko kasuetan.
16 _____________________________________________________________________
- espezifikazioa: LEGEZKO_JOKALDIA
- datuak:
e =
e11, e12, . . . , e18
e21, e22, . . . , e28
..., ..., ..., ..., ...
e81, e82, . . . , e88










: EGOERA
jok = ( (x,y), (u,z) ) : JOKALDIA
tx : TXANDA
- emaitzak: b:boolearra
- aurreko-baldintza: 1 x, y, u, z 8
- eragina:
b = true b.s.b.
1) exy = tx eta euz = ' ' eta
2) ondoko kasuren bat gertatzen da:
a)
(u,z) =
(x +1,y-1)
edo
(x +1,y+1)








baldin tx = 'T'
(x-1,y-1)
edo
(x-1,y+1)








baldin tx = 'B'


















b) badago era honetako laukitxo-sekuentzia bat:
< (u1, z1), (u2, z2), . . . , (un, zn) > , non:
· n 2 eta (u1, z1) = (x,y) eta (un, zn) = (u,z)
· baldin tx = 'T', orduan edozein 1 i < n-rentzat:
(ui+1, zi+1) = (ui+2, zi-2) eta eui+1, zi-1 = 'B'
edo
(ui+1, zi+1) = (ui+2, zi+2) eta eui+1, zi+1 = 'B'
· baldin tx = 'B', orduan edozein 1 i < n-rentzat:
(ui+1, zi+1) = (ui-2, zi-2) eta eui-1, zi-1 = 'T'
edo
(ui+1, zi+1) = (ui-2, zi+2) eta eui-1, zi+1 = 'T'
Espezifikazioa _________________________________________________________ 17
1 . 3 . 2 . Aurre-ondoetako espezifikazio formala
Programen egiaztapena eta eratorpen formalerako ezinbestekoa da espezifikazio
formalak erabiltzea. Aurre-ondoetako espezifikazioa aurreko baldintza eta ondoko baldintza
izeneko bi formulez osatzen da. {} P {} notazioak, non aurreko baldintza, P programa
eta ondoko baldintza diren, P programak eta formulen bidez adierazitako
espezifikazioa betetzen duela baieztatzen du, hau da, P exekutatu aurretik egiazkoa bada,
orduan exekutatu ondoren ere egiazkoa izango dela. Esate baterako, {y 0} P {z = x/y}
notazioaren bidez hauxe adierazten da: hasieran y aldagaiak zero balioa ez duen guztietan, P
programa exekutatzearen ondorioz z-n x eta y-ren arteko zatidura edukiko dugu. Baina,
aurreko eta ondoko baldintzak idatzita dauden lengoaiaren arabera aurre-ondoetako
espezifikazioa formala edo ez-formala izan daiteke. Gure helburuetarako lengoaia formala
hautatu dugu: lehen mailako logikaren lengoaia. Aurreko baldintza formularen aldagaiak
programaren sarrerako datuak dira, nolabait bete beharreko baldintzak definitzen dituelarik.
Ondoko baldintzak datu eta emaitzen arteko erlazioa finkatzen du, programaren esanahia
agerian utziz.
Beraz, formula bion bidez objektuen propietateak adierazten dira. Ezin ahantzi, hala
ere, objektu hauek datu-mota batekoak edo bestekoak direla eta, horregatik, erabiliko
dugun lengoaia ikusi aurretik, Pascal-eko datu-moten erabilera formalari erreparatuko
diogu, notazioak behar bezala finka ditzagun.
18 _____________________________________________________________________
Ariketak
1.1.- Espezifikatu ez-formalki ondorengo abstrakzio funtzionalak:
- Erabaki ea zenbaki oso bat kapikua den.
- Emandako bi array-en elementu errepikatuak lortu.
- Zenbaki osoen multzo bat bi azpimultzo disjuntutan banatu, non azpimultzo
hauetako elementuen baturak berdinak izatea bete behar bait da.
- Input-etik zenbaki osoen sekuentzia bat irakurri eta output-ean idazten du.
Abstrakzio honek input-eko zenbakiak goranzko ordenan idazten ditu, lerro
bakoitzean zenbaki bana eta, ondoren, zenbaki hori input-ean zegoeneko
posizioa. Zenbaki errepikatuak daudenean, dagozkien posizioak goranzko ordenan
idazten dira. Adibide honetan sarrera konkretu bati dagokion irteera ikus daiteke:
input = < 3, 4, 7, 3, 2 >
output = < < 2, 5 >, < 3, 1 >, < 3, 4 >, < 4, 2 >, < 7, 3 > >
- S[1..n] eta I[1..n] array-etan n koloretako konbinazioak gordetzen dira
(errepikapenik gabe), koloreak hauexek izan daitezkeela: gorria, urdina, horia,
txuria, beltza, berdea eta marroia. S eta I emanda, a) eta b) emaitzak lortzen ditu
abstrakzio funtzional honek, non:
a) I-n eta S-n egon bai, baina posizio desberdinetan dauden koloreen kopurua,
b) I-n eta S-n egoteaz gain, posizio berdinetan dauden koloreen kopurua.
Adibidez:
S=(gorria, marroia, horia, berdea, urdina)
eta
I=(berdea, marroia, txuria, beltza, gorria) edukiz gero,
a) partean lortutako kopurua 2 litzateke (berdea eta gorria koloreengatik)
eta b)n, berriz, 1 (marroiarengatik).
- A[1..n] array-an n koloretako konbinazio bat daukagu, kolore gisa gorria, txuria
eta urdina onartzen direlarik. A emanda, array berean hasierako koloreen
konbinazio ordenatua (gorri guztiak hasieran, txuriak erdian eta urdinak bukaeran)
lortzen du ekintza abstraktu honek.
Espezifikazioa _________________________________________________________ 19
- N erreginen problema ebatzi: "n x n jake-taulan n erregina kokatu elkar jan
gabe".
- Luzera berdineko azpisekuentziez osatutako zenbaki osoen fitxategia emanda,
non fitxategiaren lehen elementuak azpisekuentzi kopurua adierazten duen eta
bigarrenak hauen luzera, kalkulatu:
a) Fitxategi osoarentzat:
- Gutxienez 0 bat daukaten azpisekuentzien kopurua.
- Azpisekuentzi kopurua bikoitia bada, azken azpisekuentziaren
elementuen batura.
b) Azpisekuentzia bakoitzarentzat:
- Azpisekuentziako zenbaki lehen handiena, baldin eta azpisekuentziako
maximoa ere bada.
- Sarrerako fitxategiaren testuko bokalen agerpen-maiztasuna kalkulatu.
Datu-moten tratamendu formala _____________________________________________ 21
2. DATU-MOTEN TRATAMENDU FORMALA
Datu-mota, balio-multzoa eta multzo horren gaineko eragiketa-multzoa da.
Balioa, izatez, ezaugarri denboral edo espazialik ez duen abstrakzio matematikoa da eta,
horregatixe, aldaezina da, nahiz eta ordenadorearen memorian errepresenta daitekeen.
Objektuak, aldiz, ezaugarri denboral eta espazialak baditu eta programan zehar indefinituta
egon edo balioren bat eduki dezake. Objektuak balio bat edukitzeak balio horren
errepresentazioa duela esan nahi du, ezinbestean memoriako espazioa hartuz. Konstantea,
bere balioa aldaezina den objektua da. Aldagaia, ordea, balioa alda dezakeen objektua da.
Eragiketa balioen funtzio matematikotzat har daiteke. Eragiketa-sinbolo edo eragile
batek eragiketa zehatz bat adierazten du. Horrela osatutako adierazpenak ere objektuak dira.
Datu-mota batek ondokoak biltzen ditu:
- Balio-multzoa: Mota horretako objektuek har ditzaketen balioen multzoa (motaren
heina). h(T) notazioaren bidez adieraziko dugu T motaren heina.
- Eragiketa-multzoa: Motako balio-multzoan eremua eta/edo heina duten eragiketen mul-
tzoa (motari dagozkion eragiketak).
Datu-moten erabilpenak honako abantail hauek dakartza:
- Objektuei buruzko ideiak argitu eta egituratzen laguntzen dio erabiltzaileari.
- Konpilazioaldiko moten gaineko kontrolaren inguruan: Programaren testua aztertze
soilarekin aski du konpiladoreak objektuen gaineko eragiketak motekiko koherenteak
diren egiaztatzeko.
- Objektuen eta moten erazagupena kontuan hartuz, programaren exekuziorako behar den
memoria finka dezake konpiladoreak.
Datu-motaren kontzeptuak ere badu zerikusirik abstrakzioarekin, datu-mota
bakoitzeko bi maila bereiz daitezke eta:
- Maila abstraktua: Balioen heina eta dagozkion eragiketak.
- Inplementazio-maila: Balioen memoriako errepresentazioa eta eragiketen
inplementaziorako algoritmoak.
Aldagai baten datu-motak bere balio guztien ezaugarri komunak finkatzen ditu,
(barne-errepresentazioari erreparatu gabe) oinarrizko eragiketen propietateen bidez (hauen
inplementazioak ere kontuan hartu gabe). Axioma-multzoen bitartez adierazi ohi diren
oinarrizko eragiketen propietateek, inplizituki, balioak karakterizatzen dituzte, ezin bait
dira erabili eragiketa hauen bidez ez bada.
22 _____________________________________________________________________
Goi-mailako lengoaietan gehien erabiltzen diren datu-motek eredu matematiko
ezagunekin lotura estua dute eta, horregatik, beraien propietate matematikoak ederki
mugatuta daude. Esate baterako, Osoak, Errealak, Biderkaketa Cartesiarra, Multzoak edo
Sekuentziak bezalako motak nahiko adierazgarriak dira.
Pascal izan zen kontzeptuok honela erabili zituen lehenengoetako lengoaia, aurretik
datu-motak balio-multzoak besterik ez bait ziren.
Pascal-ez datu-mota sinple eta egituratuak bereizten dira. Datu-mota sinpleak,
honakoak: Integer, Real, Char eta Boolean. Datu-mota hauetako objektu eta eragiketen
notazioa, formalismoa eta propietateak, bakoitzari egokitzen zaion eredu matematikoaren
araberakoak dira. Hots, Integer-entzat (Z, +, *, div, /, -, old, ...) eta Real-entzat (R, +, *,
/, ...), Char-entzat ({`a´,..., `z´, `0´, ..., `9´, ` ´, ...} ord, suc, pred,...) eta Boolean-entzat
Booleren algebra ({T, F}, not, and, or, ...). Eredu hauek dagoeneko ezagunak ditugu.
Datu-mota egituratuetako objektuak, objektu sinpleagoen bildumez (normalean
osagaiak deitutakoak) eta atzipenerako nahiz aldaketarako oinarrizko eragiketez osatzen
dira, era batean edo bestean. Pascal-ez lau modu desberdinetan konposatzen dira aldagai
sinpleak, bakoitzari kontzeptu matematiko desberdina dagokiola.
2.1. SET (MULTZOA)
Pascal-eko set motako objektuak multzoak dira. Zehazkiago, type M = set of T
erazagupenak M datu-mota definitzen du, eta
h (M) = (h(T)), non
T oinarrizko mota bait da eta (A)k A multzoaren parteen multzoa denotatzen bait du.
Adibidea: type KL = set of `a´..`c´ erazagutuz gero, KLren heina = ({`a´,`b´,`c´})
Beraz, edozein var x: KL aldagaik ({`a´,`b´,`c´}) honetako edozein multzo har
lezake baliotzat, hau da, multzo hutsa edo `a´,`b´ eta `c´ karaktere guztiez edo batzuez
osatutako edozein multzo.
Mota honetako eragiketei multzoetako eragiketa matematikoak dagozkie, sintaxia
aldatu besterik gabe.
Pascal Matematikak
in (barnekotasuna)
+ (bilketa)
* (ebaketa)
- - (kenketa)
Datu-moten tratamendu formala _____________________________________________ 23
2.2. ARRAY
Array mota bi ikuspegi desberdinetatik formaliza daiteke:
a.- Multzo baten eta bere buruaren arteko biderkadura Cartesiarra.
A x B biderkadura Cartesiarra honela definitzen da:
(a,b) AxB aA eta bB
eta bere elementuen arteko berdintza:
(a,b) = (c,d) a = c eta b = d
Hortaz, Mn = M x M x ...x M
n
1 244 344
multzoa, M multzoko elementuen n-koteez
osatutako multzoa, ondokoa besterik ez da:
(m1, m2, ..., mn) Mn mi M edozein 1 i n-rentzat
eta bere elementuen arteko berdintasuna:
(m1, m2, ..., mn) = (d1, d2, ..., dp) n = p eta mi = di edozein 1 i n-rentzat
Bada, type A = array [1..n] of T definizioak, oinarrizko mota T dela, A datu-mota
definitzen du, non motaren heina hauxe bait da:
h (A) = h (T)n = {(t1, ..., tn) / ti h (T) edozein 1 i n-rentzat}, hau da, var a : A
aldagaiak h (T)nren barneko edozein (a1, ..., an) n-kote eduki dezake balio gisa. Eragiketei
buruz, berriz, A motari n eragile dagozkio, 1 i n balio guztientzat bana:
[i] : h (T)n h (T), non [i] ((a1, ..., an)) = ai
eta Pascal-ez [i] (a) denotatzeko a[i] idazten da.
b.- Indize-multzoan eremua duten funtzioak.
Array-ak, bestalde, indize-multzotik oinarrizko motarako funtzioak bezala ere
formaliza daitezke. type A = array [1..n] of T emanez gero, A datu-motaren heina funtzio-
multzo hau litzateke: {a: {1..n} h(T)}. Kasu honetan, motako eragiketak eremuen
gaineko array-ak berak dira, Pascal-eko a[i] notazioak eremuko i balioaren funtzioa
adierazten duelarik, hau da, a(i) adierazpena. Hari beretik, funtzio-konposaketa ere definituta
dago eta Pascal-eko a[b[i]] adierazpenak (a (b(i)) = a°b(i) konposaketa denotatzen du.
2.3. RECORD (ERREGISTROA)
Erregistroei atxikitutako eredu matematikoa ere biderkadura Cartesiarra da, baina
multzo desberdinen artekoa.
type R = record
s1 : T1 ;
...
sn : Tn
end;
24 _____________________________________________________________________
sententziaren bidez definitutako R motaren heina h(T1 ) x ... x h (Tn)ren n-koteez
osatutako multzoa da:
h(R) = h(T1 ) x...x h(Tn) = {(t1 ,..., tn) / ti h(Ti) edozein 1 i n-rentzat}
Mota honi n eragiketa dagozkio, 1 i n bakoitzarentzat bana:
Si : h(T1) x ... x h(Tn) h (Ti) non,
t = (t1,...,tn) h(T1) x ... x h(Tn) emanik, orduan Si (t) = ti, Pascal-eko puntu-notazioaz
honela adieraziko litzatekeena: t . si .
Pascal-ez badaude erregistro aldagarriak ere, eta berauen barne-kontzeptu
matematikoa T1,...,Tn multzoen bildura disjuntua da. Har dezagun:
type RA2 = record
case tag : (k1, k2) of
k1 : (s1: T1);
k2 : (s2: T2)
end;
non k1, k2 konstante-identifikadoreak bait dira, eta RA2ren heina T1 eta T2ren arteko
bildura disjuntua bait da, honela: {k1} x h (T1) {k2} x h (T2)
Orokorrean:
type RA = record
case tag : (k1,...,kn) of
k1 : (S1,1: T1,1 ,..., S1,m1
: T1,m1
);
...
kn : (Sn,1: Tn,1 ,..., Sn,mn
: Tn,mn
)
end;
eta definizio honen heina honako bildura disjuntua da:
{k1} x h (T1,1) x ... x h (T1,m1
) ... {kn} x h (Tn,1) x ... x h (Tn,mn
)
Hortaz, var t: RA erazagutuz gero t-ren balioa edozein (to,...,tp) p-kote izan liteke,
non to = ki izango den 1 i n batentzat eta, halabeharrez, p = mi. Hauetako i bakoitzari
mi+1 eragiketa dagozkio:
- tag eragiketa, non tag (t) = to bait da, Pascal-ez t.tag adierazpenaren bidez denotatzen
dena.
- Si,j eragiketak (guztira mi), 1 j mi bakoitzarentzat bana, non Si,j funtzio partziala
den:
Si,j (t) : h (RA) h(T1,1) ... h (T1,m1
) ... h(Tn,1) ... h (Tn,mn
)
Si,j(t)=
tj baldin t0 = ki
indefinitua bestela






Pascal-ez Si,j (t) denotatzeko t.si,j erabiltzen da.
Datu-moten tratamendu formala _____________________________________________ 25
2.4. FILE (FITXATEGIA)
Fitxategien barne-kontzeptua sekuentzia da, biderkadura Cartesiarraren bidez honela
defini daitekeena:
T multzoa eta n zenbaki arrunta emanda, n aldiz egindako T eta bere buruaren arteko
biderkadura Cartesiarrari Tn deituko diogu, hau da, Tn = T x T x .. x T
n
1 244 344
, non To = {< >}
eta T1 = T kasu partikularrak diren. Gatozen definitzera:
a) T* multzoa, Tko elementuen sekuentzien multzoa:
T* = To T1 ... Tn ...
eta T+, Tko elementuen sekuentzia ez-huts guztien multzoa:
T+ = T1 T2 ...
b) Sekuentzi kateamendua: T*-ren barneko < a1,..., an > eta < b1,..., bm > sekuentziak
emanda, bi sekuentzion kateamendua, < a1,..., an> · jarriz adieraziko
duguna, < a1,..., an, b1,..., bm > T* sekuentzia da.
c) Sekuentzia ez-huts baten lehena:
lehen : T+ T , non
lehen (< a1,..., an >) = a1
d) Sekuentzia ez-huts baten hondarra:
hondar : T+ T* ,
non, hondar (< a1, a2, ..., an >) = < a2, ..., an >.
Hots, edozein s T+-rentzat
· hondar (s) = s izango da.
"Type F = file of T" definituz gero F datu-motaren heina h(F) = h(T)* da.
Aurreko datu-motetan ez bezala, ez dago zuzeneko atzipenik, eragiketa bakarra atzipen
sekuentziala da eta. Elementu bakar bat atzi daiteke aldiberean. Atzipen sekuentziala
formalizatu ahal izateko, beharrezkoa da fitxategi motako objektuaren egoera kontutan
hartzea, alegia, ez dela sekuentzia motako balioa bakarrik ezagutu behar, baizik eta une
bakoitzean atzigarria den sekuentziaren elementua ere bai.
s
f ·
r
f notazioaz f T*
adieraziko dugu, f =
s
f ·
r
f , non f = lehen (
r
f ) une bakoitzeko elementu atzigarria izango
den. Horregatik, fitxategien gaineko oinarrizko eragiketak,
r
f ,
s
f eta f aldiberean
aldatzen dituzten eragiketen baliokideak dira. Baliokidetasun hauek, aldibereko asignazioen
bidez azalduko ditugu:
26 _____________________________________________________________________
reset (f) = [
r
f:=
s
f ·
r
f
s
f : = <>
f:= lehen (
s
f ·
r
f) ]
get (f) = [
s
f:=
s
f · < lehen (
r
f) >
r
f : = hondar (
r
f)
f:= lehen (hondar (
r
f))]
put (f) = [
s
f:=
s
f ·< f >
f := indefinitua
r
f := < > ]
rewrite (f) = [
s
f := < >
r
f := < > ]
eof (f) [
r
f = < >]
Ariketa gisa interesgarria litzateke lerro-egitura duten fitxategiak formalizatzea
sekuentziaz osatutako sekuentziak bezala (lerro bakoitza karaktere-sekuentzia da, eta
fitxategia lerro-sekuentzia).
Lehen mailako logikaren lengoaia ___________________________________________ 27
3. LEHEN MAILAKO LOGIKAREN LENGOAIA
Lengoaia formal bat definitzeko bere sintaxia eta semantika mugatu behar dira.
Lehen mailako logika aztertzeko, lengoaiaren sintaxia aldagai, funtzio eta predikatu
sinboloez osatutako alfabeto generiko baten gainean definituta eduki behar da. Lengoaia
hau Pascal-ez idatzitako programen zuzentasunaz arrazonatzeko erabiliko dugunez, horretara
egokitutako alfabetoa finkatuko dugu:
- Aldagai-sinboloak edozein motatako aldagai-identifikadoreak dira:
A, f, input, f, x, y, z, aurre, zenb
- Konstante-sinboloak:
3, `a´, < 5,7 >, < >, (3,2,1)
- Funtzio-sinboloak Pascal-eko funtzio standard guztien ikurrak edo dagozkien ikur
matematikoak, "suc, "*", "div", "mod", "", "+", "round", e.a., dira. Notazio
matematiko edo laburdura gisa erabili ohi diren funtzioak ere onartuko ditugu: , !, e.a.
- Predikatu-sinboloak Pascal-eko funtzio boolear guztiak dira ("odd", , , , ...) eta,
bereziki, berdintasuna (=). Era berean, matematiketako edozein predikatu edo laburdura
ere erabil daiteke, esate baterako.
Funtzio- eta predikatu-sinbolo bakoitzari anizkotasun jakin bat datxekio, behar
dituen eragigaien kopurua adierazten duena.
Zenbat eta zabalagoa izan onartzen den alfabetoa, orduan eta malguagoa eta
aberatsagoa da lengoaia, eta errazago gertatzen da beraren bidez propietateak adieraztea.
Hauxe da, hain zuzen ere, notazio matematiko hauek onartzearen arrazoia.
Alfabetoa finkatu ondoren, gatozen lengoaiaren sintaxia definitzera.
3.1. LENGOAIAREN SINTAXIA
Gaiak:
a) Edozein konstante gaia da,
b) Edozein aldagai gaitzat hartzen da, eta
c) t1,...,tn gaiak badira eta f funtzio-sinbolo n-tarra bada, f (t1,...,tn) ere gaia izango da.
Gaien eta funtzio-sinboloen sintaxiaren arteko komunztadura beharrezkoa da, bestela,
sortutako gaiak ez bait lirateke onargarriak izango.
28 _____________________________________________________________________
Formulak:
d) t1,...,tn gaiak badira eta P predikatu n-tarra, orduan P(t1,...,tn) formula (atomikoa) da.
Aipagarria da "=" berdintasun predikatu bitarra, maiz erabiliko dugu eta.
e) eta formulak badira, ¬(), ( ), ( v ), ( ), ( ) ere formulak
dira.
f) x aldagaia eta formula bada, x() eta x() formulak dira, non . eta
kuantifikatzaile unibertsala eta existentziala diren hurrenez hurren.
Formuletako aldagaien artean bi motatakoak bereiziko ditugu, segun-eta nolakoak
diren beren agerpenak:
formulan x aldagaiaren agerpena librea dela esango dugu baldin eta ez badago
inongo kuantifikatzaileren eraginpean, eta agerpena atxekia izango da bestelako kasuetan.
Aldagai batek agerpen libreak eta atxekiak eduki ditzake formula berean. Aldagai bat librea
da formula batean, gutxienez agerpen libre bat badauka formula horretan, eta bestela
atxekia izango da.
3.1. adibidea: Ondokoak lehen mailako formulak dira:
a) x (0z) z (z>x)
Formula honetan x-ren lehenengo agerpena atxekia da eta hirugarrena librea,
eta z-ren lehenengoa librea eta bigarrena atxekia; hortaz, bai x, bai z aldagai
libreak dira.
b) z (z>0 z Kasu honetan z-ren bi agerpenak atxekiak dira eta x-rena, berriz, librea.
Beraz, z aldagai atxekia da eta x librea.
3.2. LENGOAIAREN SEMANTIKA
Lengoaiaren semantikak gaien eta formulen esanahia definitzen du. Gaiek eta
formulek esanahirik eduki dezaten, ezinbestekoa da aldagaiek balio zehatzak hartzea. Balio
hauek, landuko dugun alorrean, programaren exekuzioko instant konkretu batean aldagaiek
dituztenak dira, konputazio-egoerari dagozkionak, alegia. Horregatik semantikaren
formalizazioari ekin aurretik konputazio-egoera modu zehatzago batez definituko dugu.
S konputazio-egoera funtzio bat da, non:
. Eremua aldagai-identifikadoreen multzoa den,
. Heina aldagai guztien moten heinen bildura den eta
. Aldagai bakoitzari bere motako balio bat egokitzen zaion.
Lehen mailako logikaren lengoaia ___________________________________________ 29
Egoera funtzioa bikote-multzo batez adieraziko dugu aurrerantzean, bikote
bakoitzak aldagai-identifikadore bat eta honi egokitutako balioa dituela.
3.2. adibidea: Ondorengo programak a eta b zenbaki oso ez-negatiboen batura
kalkulatzen du, baten gehiketa eta baten kenketaz aparteko eragiketarik erabili gabe:
begin
x: = a; y : = b;
while y > 0 do
begin (*)
x:=x+1;
y:=y-1
end
end
Programa honen bukaeran gerta litezkeen egoera batzuk hauek lirateke:
{(a,7), (b,3), (x,10), (y,0)}
{(a,0), (b,5), (x,5), (y,0)}
(*) seinaleaz markatutako kontrol-puntuko egoera posible batzuk:
{(a,7), (b,3), (x,8), (y,2)}
{(a,7), (b,3), (x,9), (y,1)}
Ondorengoak, aitzitik, (*) puntuan gerta ezinezkoak dira:
{(a,7), (b,3), (x,6), (y,4)}
{(a,7), (b,3), (x,8), (y,4)}
{(a,7), (b,3), (x,9), (y,1)}
Egoera aldatu ere egin daiteke, bai (aldagaia, balioa) bikote berri bat erantsiz, bai
aldagai bati balio zaharraren ordez beste berri bat egokituz. Edozein modutan ere, S egoeran
x aldagaiari b balioa egokituz sortzen den egoera berria S[b/x] notazioaz adieraziko dugu.
Lehen mailako formula bat, , S egoeran ondo definituta dagoela esaten da, baldin
eta -ko aldagai libreen identifikadore bakoitzari Sn bere motako balioren bat badagokio.
Gaien eta formulen balioztapena soilik ondo definituta dauden egoeretan burutu daiteke.
Ikus dezagun, bada, gaiak eta formulak nola balioztatzen diren.
30 _____________________________________________________________________
Gaien balioztapena S egoeran
a) S (konstantea) = konstantea.
b) S (aldagaia) = S egoeran aldagaiari dagokion balioa.
c) S (f (t1, ..., tn)) = f (S (t1), ...,S (tn))
Formulen balioztapena S egoeran
d) S P t1,t2,L,tn( )( )=
true baldin P S t1( ),L,S tn( )( )= true
false bestela








Egin kontu konstanteak, funtzioak eta predikatuak ez direla interpretatzen, ikur
interpretagarriak izan ordez, aldez aurretiko interpretazio standard ezaguna bait dute.
e)
S ¬( )=
true baldin S ( )= false
false baldin S ( )= true








S ( )=
true baldin S ( )=S ( )= true
false bestela






S ( )=
true baldin S ( )= true edo S ( )= true
false bestela






S ( )=
true baldin S ( )= false edo S ( )= true
false bestela






S ( )=
true baldin S ( )=S ( )
false bestela






f)
S x( )=
true baldin x - ren motako a balioren bat existitzen bada, non
S a / x( ) ( )= true
false bestela










S x( )=
true baldin x - ren motako edozein a baliorentzat
S a / x( ) ( )= true betetzen bada
false bestela










Lehen mailako logikaren lengoaia ___________________________________________ 31
3.3. adibidea: Adibide honetako edozein aldagairen eremua zenbaki osoen multzoa dela
suposatuko dugu.
- Izan bedi S1 = {(x,4)} egoera, S1(y z (y*z = x y = z)) = true izango da, zeren
eta
S1(yz = x y = z)y,z
2,2
= S1(2*2 = x 2 = 2) =
(2*2 = 4 2 = 2) = true bait da.
- Izan bedi S2 = {(y,1), (z,2)} egoera, S2(x (x > 0 z*x > y)) = true izango da,
S2 (x > o 2x > 1)x
a
= true bait da edozein a zenbakirentzat (betiere osoen
eremuan).
- Azkenik, izan bedi S3 = {(y,2), (z,1)}, S3( x(x > 0 z*x > y)) = false da,
S3(x>0 2x>2)= (1 > 0 2 > 2) = false bait da.
Gure helburua programen kontrol-puntuetan gertatzen diren egoera-multzoak
formulen bidez adieraztea da, nolabait konputazio-egoeren ezaugarri komunak dira agerian
uzten direnak. Testuinguru honetan erabilitako formulei asertzio deitzen zaie.
Asertzio batek egiazkoa deneko egoera-multzoa errepresentatzen du (egoera-multzo
hau infinitua izan daiteke). Hortaz, T-k egoera-multzo osoa errepresentatzen du eta F-k
egoera-multzo hutsa. Esate baterako, programaren puntu batean x aldagaiak zenbaki lehen
bat duela esan nahi bagenu, asertzioa honako hau litzateke:
lehena_da (x) = x 2 yz(x = y*z (y=1 v y =x))
3.4. adibidea: 3.2 adibidean azaldutako programak asertzio hauek edukiko lituzke:
begin {x,y0}
x: = a; y : = b; { x=a y=b x,y0}
while y > 0 do
begin {x+y=a+b xa0 0 x:=x+1; y:=y-1
end
end; {x=a+b y=0 x,a,b0}
formula baino gogorragoa dela esaten da -k errepresentatzen duen egoera-
multzoa -k errepresentatzen duenaren partea bada. Kasu honetan baino ahulagoa dela
esaten da. Formula gogorragoek murriztapen gehiago ezartzen diete beren aldagai libreei.
Honen arabera erraz konpreni daiteke "true" beste edozein formula baino ahulagoa dela eta
"false" dela formularik gogorrena. formula baino gogorragoa baldin bada, orduan
S()=true izango da edozein S egoeratan.
32 _____________________________________________________________________
3.5. adibidea: Formula gogorrago eta ahulagoak:
(a) (x=5 z=25) z=x2
(b) (x=A[i] 1in) k(x=A[k] 1kn)
(c) k(xkz A[k]p) A[(x+z) div 2]p
(d) false , edozein -rentzat
(e) true , edozein -rentzat
Eta, azkenik, programen egiaztapenerako berebizikoa den eragiketa batez arituko
gara, aldibereko ordezpenaz.
Izan bitez formula, x aldagaia eta t gaia, formulan x-ren agerpen libre guztiak t
gaiaz ordeztu ondoren lortutako formula honela denotatuko dugu: x
t
Batzuetan, -n lehendik ere bazegoen aldagairen bat t gaian ageri denean, ordezpena
egitean aldagai-talka gertatzen da. Aldagai-talkarik gertatzen ez denean -k x-ri buruz eta
x
t
­k t-ri buruz gauza bera diote. Hau ezin daiteke baieztatu, ordea, talkarik gertatzen bada.
3.6. adibidea: Izan bedi =(z (1 gainean egindako ordezpenak:
a) x
5
= z (1 b) x
A[i]
= z (1 c) d
d+1
= z (1 d) d
x
= z (1 e) x
x·z
= z (1 a), b) eta c) adibideetan ez da formulen esanahia aldatzen (gaiak bai, baina gaiei
buruzkoa ez). Aldiz, d) eta e) adibideetan formulen semantika erabat aldatzen da, talken
kariaz.
Era berean, x1, ..., xn aldagaiak eta t1, ..., tn gaiak emanez gero, xi (1in) aldagai
guztiak ti (1in) gaiez aldi berean ordeztuta lortzen den formula x1 ,x2 ,...,xn
t1 ,t2 ,...,tn
formaz
idazten da.
Aldagai-talkari buruzkoak kasu honetan ere badu zentzurik.
Lehen mailako logikaren lengoaia ___________________________________________ 33
3.7. adibidea: Izan bedi = 1in A[i]=x z (1z a) i,x
3,'a'
= 13n A[3]='a' z (1z<3 A[z]'a')
b) i,x
i+1,A[i]
= 1i+1n A[i+1]=A[i] z (1z a) adibidean ez dago aldagai-talkarik, baina b)-n bai.
eta x
t
formulak parekoak izango dira, baldin eta formulan x-ren agerpen
libreak eta x
t
formulan t-ren agerpen libreak leku berdinetan gertatzen badira (gai baten
agerpena librea da bere aldagai guztiak libreak badira).
Bi formula baliokideak dira egoera-multzo bera errepresentatzen badute, hau da, biek
gauza bera baieztatzen badute.
eta x
z
parekoak badira, orduan x eta zx
z
eta, era berean, x eta zx
z
formulak elkarren baliokideak dira. t gaia f(z) erako funtzioa denean ere gauza bera
gertatzen da. Hortaz, ordezpenak talkarik sortzen ez duenean, formulen kuantifikazioak
baliokideak dira.
3.8. adibidea:
a) Izan bedi = x > 0 s (s z),
x eta z(x
z
)= z (z > 0 s (s z)) ez dira baliokideak baina
x eta p (x
p
) = p (p > 0 s (s z)) baliokideak dira.
b) Izan bedi formula, x1, ..., xi sekuentziaren batura S dela baieztatzen duena:
i S= xj
j=1
i









eta i S= xj
j=1
i+1









baliokideak dira
i eta i i
i+1
erakoak dira, hurrenez hurren.
c) i (1in x=A[i]) eta i (1i+1n x=A[i+1]) formulak ere baliokideak
dira.
34 _____________________________________________________________________
Ariketak
3.1. Idatzi ondoko baieztapenak lehen mailako formulez:
- Osozko A[1..n] array-aren i-garren elementuaren ondoren dauden guztiak zeroak
dira.
- A[1..n] array-an x badago, i..j sekzioan egongo da.
- A[1..n]-k bi zero dauzka.
- i posizioak A[1..n] array-a erdibitu egiten du, x baino txikiagoak batetik eta x
baino handiagoak bestetik.
- f karaktere-fitxategian ez daude bi txurigune jarraian.
- A[1..n] array-ak badauka zehazki k zerotako sekzio bat.
- S[1..n] eta A[1..m] array-ek amankomunean dituzten el

Programen egiaztapena eta eratorpena