Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
The Java Modeling Language – A study and an implementation of JML.
KTH, School of Computer Science and Communication (CSC).
2011 (English)Independent thesis Advanced level (professional degree), 10 credits / 15 HE creditsStudent thesis
Abstract [en]

This is a study on the Java Modeling language, presenting its main features and applying them onto an algorithm based upon Binary Decision Diagrams. JML is a Design by Contract tool for java. The principal idea behind Design by Contract is that clients calling methods in a class have a contract with each other. These contracts consist of pre- and post-conditions that are to be validated before and after the execution of any method with such a contract.

As interesting as it was studying JML, at the implementation stage it became clear that the JML2 tool set was not upgraded for any java upgrades beyond java 1.4. Using generic types and other language features such as the for-each loop was not recognized by the JML compiler.

However, once up and running with a J2SE4 environment, many advantages could be discovered. The runtime assertion checker worked great as a bug prevention tool and the JML specifications serve as a good way to document code properly. More important though is the way it forces the developer to take into consideration all the different relationships between classes and their methods and also to define set invariants to hold for these.

Abstract [sv]

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.

Place, publisher, year, edition, pages
2011.
Series
Kandidatexjobb CSC, K11056
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-130841OAI: oai:DiVA.org:kth-130841DiVA: diva2:654288
Educational program
Master of Science in Engineering - Computer Science and Technology
Uppsok
Technology
Supervisors
Examiners
Available from: 2013-10-07 Created: 2013-10-07

Open Access in DiVA

No full text

Other links

http://www.csc.kth.se/utbildning/kandidatexjobb/datateknik/2011/rapport/karde_wilhelm_K11056.pdf
By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 20 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf