Formele aspecten van de programmeertaal XSLT: determinisme, terminatie en complexiteit

Abstract

The eXtensible Stylesheet Language Family (XSL) is een verzameling talen om een XML-document te transformeren naar een nieuwe XML-boom. De inputboom is bijvoorbeeld een database in XML en het resultaat is een presenteerbaar formaat. Je kan vanuit éénzelfde XML-document zowel een brochure in PDF opstellen, als een site in HTML. XSL is opgedeeld in twee deelspecificaties. Als eerste is er de eXtensible Stylesheet Language for Transformations (XSLT) die een gegeven boom omzet in een andere boom. Wanneer deze stap voltooid is, gaan we het bekomen resultaat omzetten in leesbaar formaat. Teksten kunnen ingekleurd worden en verschillende opmaakstijlen zijn voorhande. Dit deel wordt verricht door de eXtensible Stylesheet Language - Formatting Objects (XSL-FO). In deze thesis gaan we dieper in op XSLT.We willen XSLT in een abstracte syntax gieten en de semantiek formeel beschrijven. Met deze formalisatie gaan we dan op zoek naar allerhande eigenschappen voor XSLT 1.0. Wanneer we daarmee klaar zijn, kijken we naar een essentieel feature dat toegevoegd werd in XSLT 2.0, namelijk de temporary trees. Na een inleidend hoofdstuk bespreken we boomautomaten. Deze automaten zijn in staat bomen van een bepaalde boomtaal te accepteren of bomen te herschrijven. Natuurlijk leunt dat laatste sterk aan bij XSLT. Ook geeft het de typische onderdelen weer van formele semantiek, zoals het definiëren van configuraties en het opstellen van een transitiefunctie tussen deze configuraties. Vervolgens gaan we herschrijfsystemen onder de loep nemen. Uiteraard is XSLT een herschrijfsysteem voor bomen. Daarom gaan we in het algemeen enkele bekende eigenschappen van herschrijfsystemen bekijken en definiëren we ook het concept ’confluentie’. Met deze twee voorgaande hoofdstukken hebben we een stevige basis opgebouwd om een formeel model voor XSLT uit te werken. We beschouwen XSLT als een subtree replacement system, waarop we dus stellingen en lemma’s uit het vorige hoofdstuk kunnen toepassen. We trachten aan te tonen dat XSLT confluent is. Een eerste belangrijke toepassing van ons uitgedokterd herschrijfsysteem is de terminatie van XSLT 1.0. We stellen ons de vraag of het mogelijk is om, voor een gegeven programma en een gegeven inputboom, te achterhalen of de transformatie stopt. Hiermee eindigen we de studie van XSLT 1.0 en gaan we door met XSLT 2.0. Na een kort overzicht geschetst te hebben van de nieuwe features van XSLT 2.0, richten we ons op de meest belangrijke nieuwigheid, namelijk de temporary trees. We eindigen de thesis met te kijken welke enorme invloed deze hebben op het aantal berekenbare boomtransformaties die uitgevoerd kunnen worden met behulp van XSLT.