Wilhelm Kärde

The Java Modeling Language A study and an implementation of JML

Sammanfattning

Det här är en studie gjord på “The Java Modeling Language” genom att presentera dess viktigaste funktioner samt applicera dessa på en algoritm baserad på ”Binary Decision Diagrams”. JML är ett ”Design By Contract” verktyg för java. Idén bakom DBC är att en klient och en metod ur en klass har ett kontrakt med varandra. Detta kontrakt realiseras genom pre- och post-vilkor som måste uppfyllas före och efter exekveringen av metoden.

Den intressanta studien fick en trist uppföljning när det visade sig att JML kompilatorn inte är kompatibel med java 1.5 och senare. Detta resulterade i kompilatorn inte kände igen generiska typer och ”for-each” loopar t.ex.

Däremot, om man är villig att koda i java 1.4 så kunde flertalet fördelar med JML upptäckas. JMLs ”runtime assertion checker” fungerar utmärkt för att förhindra och upptäcka buggar. Specifikationerna fungerade dessutom som bra kod dokumentation. Men viktigast av allt var hur JML tvingar en att tänka på relationen mellan klasser och metoder och invarianter som ska hålla för dessa.