Verifieerbare Generalisatie van XSLT Document Transformaties

Tijdens de opkomst van Internet is HTML flink uit haar voegen gegroeid, en daarom wordt nu geprobeerd documenten weer beter te structureren door over te stappen op XML en XSLT als standaarddataformaten. XML wordt daarbij gebruikt om pure data weer te geven, terwijl alle representatie-specifieke aspecten in een XSLT stylesheet worden gestopt.

De data-weergave in XML is voor de databasegroep interessant, zeker ook omdat gewerkt wordt aan een querytaal genaamd XQL. Maar ook XSLT is bijzonder interessant, omdat het bijvoorbeeld ook kan worden gebruikt om data in tussen verschillende conceptuele te transformeren. Echter, op dit gebied schiet XSLT tekort zodra die transformatie meerdere databronnen moet integreren tot een geheel. Het eerste zwaartepunt van deze opdracht is dan ook het uitbreiden van XSLT tot een taal die deze beperking niet kent.

Het tweede zwaartepunt is van wiskundige aard. Doordat XML en XSLT heel expliciet omgaan met documentstructuur is het zeer doenlijk om uitspraken te doen over alle toegestane structuren voor documenten. En dat kan worden gebruikt in een bewijstechniek die structurele inductie heet, ofwel het aantonen van een eigenschap voor alle denkbare structuren binnen een syntax. Vertaald naar de uitgebreide XSLT taal betekent dit dat het mogelijk wordt om algebraische eigenschappen zoals transitiviteit en commutativiteit van een transformatie aan te tonen, en ook vaak zul je een inverterende stylesheet kunnen afleiden. Het automatiseren van zulke bewijzen is dan ook opgenomen in deze opdracht.

Voor deze opdracht moet je dus werken aan de esthetische kant van taalontwerp, aan de implementatie van een stylesheet-gedreven compilertje, en aan algebraische bewijsvoering. Denk je dat jij de duizendpoot bent die we zoeken, loop dan eens langs om golflengtes af te stemmen!

XML, XSL en nog wat hype...

Pfff, dacht je d'r te zijn nu je HTML onder de knie hebt, heeft de web-wereld weer wat nieuws bedacht: XML, de eXtensible Markup Language. Hmmm, eigenlijk niet eens zo'n raar concept: Probeer wat meer structuur aan te brengen in het web door mensen toe te staan zelf <TAGS> te bedenken, en vast te laten pinnen in welke structuren die allemaal genest mogen worden. Da's handiger dan HTML omdat je dan niet de layout specificeert, maar gewoon de kennis die je wilt webben. Natuurlijk moet die layout worden omgezet in opmaak, maar daar kun je dan een omzettingstaal voor gebruiken... en zo onstaat ook XSL, de eXtensible Stylesheet Language.

XSL is cool. Want niet alleen kun je er je zelfbedachte XML structuren mee omzetten in bijvoorbeeld HTML of LaTeX, maar ook kun je er handige trucs mee uithalen als je programmeert. Want wat XSL doet is structuur herkennen in de tags (het is dus een soort parser) om op herkende structuren een herschrijvingsactie toe te passen. Er is niets wat je beperkt om bijvoorbeeld Java of Perl te genereren uit zo'n stylesheet!

Ik gebruik die truc steeds vaker; niet alleen om uit conceptuele structuren (van state diagrammen in mijn geval) programma's te maken, maar ook begeleid ik momenteel een ontwerpproject waarin de studenten een door hun bedacht XML formaat voor GUI beschrijving automatisch omzetten in een implementatie. Ze maken een XSL omzetter die Java genereert, eentje voor Delphi, een andere voor HTML en voor Tcl/Tk. Vier stylesheets, vier andere implementaties, alle uit dezelfde GUI beschrijving! Maar in dit project komen ook tekortkomingen van XSL naar voren met betrekking tot deze trukendoos.

Het zou fraaier zijn wanneer XSL niet alleen 1-op-1 omzetting (van 1 input file naar 1 output file) mogelijk zou maken, maar ook N-op-1, enzovoort. Bijvoorbeeld als je wilt `linken', ofwel een aantal deelprogramma's samenvoegen, dan wil je een aantal input files kunnen combineren tot 1 output. Je kunt stylesheets op de manier van algebra gaan zien, maar dan in een leuk jasje: Het zijn operatoren op data. En de huidige operatoren zijn heel beperkt, want ze hebben maar 1 argument.

In de algebra kijken we bij operatoren vaak ook nog naar associativiteit, commutativiteit, en dat soort eigenschappen. Die betekenen bij de eerder genoemde linker eigenlijk iets heel nuttigs, namelijk dat je de delen bij het linken in willekeurige volgorde kunt samenstellen. Als je een stylesheet bouwt en wilt testen of die eigenschap wel telt, dan zou je dat kunnen testen door de structuren in de stylesheet te onderzoeken. En dan zou je weleens verrassend op foutjes kunnen worden gewezen. Vergelijk het maar met compiler errors: De computer tikt je op de vingers als je regeltjes gaat overtreden. Soms irritant, vaak nuttig.

Hier hangt dan ook een interessante afstudeeropdracht in de lucht, die het mogelijk maakt om met XSL vertalingen van een willekeurig aantal input files naar een willekeurig aantal output files te kunnen transformeren, en om over zulke stylesheets, op basis van de structuren die erin staan, bewijzen te leveren over algebraische eigenschappen. Een hele uitdaging, en zoals het nu lijkt ook nog behoorlijk vernieuwend binnen de XML wereld!