Resum
La creixent complexitat dels sistemes software ha condu¨it al desenvolupament de
metodologies formals per a la verificaci´o i la correcci´o de dates y programes. Generalment,
establir si un programa es comporta seguint les intencions originals del
programador o controlar la consist`encia i la correcci´o de grans conjunts de dates, no
son tarees trivials, com manifesten els numerosos casos d’estudio que trobem en la
bibliografia.
En aquesta tesi, abordem dos problemes oberts de verificaci´o i correcci´o. En
concret, la verificaci´o i correcci´o de programes declaratius i la verificaci´o i correcci´o
de Web site (es decir, conjunts de dates semiestructurats).
En primer lloc, s’ha definit un esquema general per la correcci´o autom`atica de
programes declaratius basats en regles, que exploten una combinaci´o de t´ecniques
de aprenentatge inductiu top-down i bottom-up. La nostra metodologia h´ibrida pot
inferir correccions que son `ardues, o incl`os imposibles, de aconseguir con un sistema
m´es simple d’aprenentatge autom`atic purament top-down o bottom-up. A m´es m´es
s’ha particularitzat l’esquema general a dos paradigmes de programaci´o declarativa
ben coneguts: el paradigma l`ogic funcional i el paradigma funcional.
En segon lloc, s’ha formalitzat un marc per la verificaci´o autom`atica de Web
sites, que es pot utilitzar per la especificaci´o de condicions de integritat d’ells, i despr
´es comprovar autom`aticament si estes condicions es satisfeixen. D’una banda,
hem definit un llenguatge d’especificaci´o basat en regles, que permeteixen la definici´o
de propietats sint´actiques i sem`antiques de un Web site. De l’altra, s’ha formalitzat
una t`ecnica de verificaci´o que detecta patrons incorrectes/prohibits i car`encia
d’informaci´o, per eixemple p`agines Web incompletes o mancants. Durant el proc´es
de verificaci´o, es recol·lecteix l’informaci´o ´util, que pot ser utiltzata per la reparaci´o
del Web site. Per tant, despr´es de la fase de verificaci´o, tamb´e se poden inferir algunes
posibles correccions per a arranjar semi-autom`aticament el Web site erroni. La
nostra metodologia descansa en una nova t`ecnica basata en rewriting, en la qual es
sustitueix el tradicional mecanisme de pattern matching con una t`ecnica de ajustatge
m´es convenient (tree simulation) que simplifica el reconeixement de patrons en un
document semiestructurat.