Java Modeling Language
The Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler. Various verification tools, such as a runtime assertion checker and the Extended Static Checker (ESC/Java) aid development.
- Comment
- enThe Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler. Various verification tools, such as a runtime assertion checker and the Extended Static Checker (ESC/Java) aid development.
- Has abstract
- enThe Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler. Various verification tools, such as a runtime assertion checker and the Extended Static Checker (ESC/Java) aid development.
- Hypernym
- Language
- Is primary topic of
- Java Modeling Language
- Label
- enJava Modeling Language
- Link from a Wikipage to an external page
- primo.bibliothek.kit.edu/primo_library/libweb/action/dlDisplay.do%3Fvid=KIT&docId=KITSRCE1000041881&tab=kit_evastar&srt=date
- jmleclipse.projects.cis.ksu.edu/
- pag.csail.mit.edu/daikon/
- www.key-project.org/eclipse/JMLEditing/
- www.openjml.org/
- www.sireum.org/%3Fq=node/21/
- web.archive.org/web/20051016013145/http:/secure.ucd.ie/products/opensource/ESCJava2/
- www.eecs.ucf.edu/~leavens/JML/index.shtml
- jmlspecs.org/jmlrefman/jmlrefman_toc.html
- www.jmlspecs.org/jmlrefman/jmlrefman_toc.html
- www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html
- krakatoa.lri.fr
- web.archive.org/web/20110706084805/http:/www.dc.uba.ar/inv/grupos/rfm_folder/TACO
- why.lri.fr
- Link from a Wikipage to another Wikipage
- Assertion (computing)
- Bernhard Rumpe
- Category:Articles with example Java code
- Category:Formal specification languages
- Category:Java platform
- Class invariant
- Compiler
- Coq
- Design by contract
- Eclipse (software)
- Eiffel (programming language)
- Exception handling
- Existential quantifier
- Gary T. Leavens
- Hoare logic
- Invariant (computer science)
- Java
- Java (programming language)
- Java2
- Java annotation
- Javadoc
- Java syntax
- JUnit
- KeY
- Larch family
- Loop invariant
- Marieke Huisman
- Method (computer science)
- Postcondition
- Precondition
- Refinement Calculus
- Semantics
- Specification language
- Syntax highlighting
- Universal quantifier
- SameAs
- 2NQSV
- Java Modeling Language
- Java Modeling Language
- Java Modeling Language
- Java Modeling Language
- Java Modeling Language
- Java Modeling Language
- Java Modelling Language
- JML
- m.07wnhj
- Q2517517
- Subject
- Category:Articles with example Java code
- Category:Formal specification languages
- Category:Java platform
- WasDerivedFrom
- Java Modeling Language?oldid=1121920357&ns=0
- WikiPageLength
- 8674
- Wikipage page ID
- 2668299
- Wikipage revision ID
- 1121920357