Java Modeling Language - Revision history

Widefox: /* Syntax */ markup code

2024-04-04T17:32:03Z

Syntax: markup code

← Previous revision		Revision as of 17:32, 4 April 2024
Line 10:		Line 10:
	== Syntax ==		== Syntax ==
	JML specifications are added to Java code in the form of annotations in comments. Java comments are interpreted as JML annotations when they begin with an @ sign. That is, comments of the form		JML specifications are added to Java code in the form of annotations in comments. Java comments are interpreted as JML annotations when they begin with an @ sign. That is, comments of the form
			<syntaxhighlight lang="java">

	//@ <JML specification>		//@ <JML specification>
			</syntaxhighlight>

	or		or
			<syntaxhighlight lang="java">

	/@ <JML specification> @/		/@ <JML specification> @/
			</syntaxhighlight>

	Basic JML syntax provides the following keywords		Basic JML syntax provides the following keywords

Widefox: Added {{No footnotes}} tag

2024-04-04T17:30:17Z

Added {{No footnotes}} tag

← Previous revision		Revision as of 17:30, 4 April 2024
Line 1:		Line 1:
	{{Short description\|Specification language for Java programs}}		{{Short description\|Specification language for Java programs}}
			{{No footnotes\|date=April 2024}}
	The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].		The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].

ElliAWB: Disambiguating links to Coq (link changed to Coq (software)) using DisamAssist.

2023-11-12T19:54:55Z

Disambiguating links to Coq (link changed to Coq (software)) using DisamAssist.

← Previous revision		Revision as of 19:54, 12 November 2023
Line 108:		Line 108:
	* [http://pag.csail.mit.edu/daikon/ Daikon], a dynamic invariant generator.		* [http://pag.csail.mit.edu/daikon/ Daikon], a dynamic invariant generator.
	* [[KeY]], which provides an open source theorem prover with a JML front-end and an [[Eclipse (software)\|Eclipse]] plug-in ([http://www.key-project.org/eclipse/JMLEditing/ JML Editing]) with support for [[syntax highlighting]] of JML.		* [[KeY]], which provides an open source theorem prover with a JML front-end and an [[Eclipse (software)\|Eclipse]] plug-in ([http://www.key-project.org/eclipse/JMLEditing/ JML Editing]) with support for [[syntax highlighting]] of JML.
	* [http://krakatoa.lri.fr Krakatoa], a static verification tool based on the [http://why.lri.fr Why] verification platform and using the [[Coq]] proof assistant.		* [http://krakatoa.lri.fr Krakatoa], a static verification tool based on the [http://why.lri.fr Why] verification platform and using the [[Coq (software)\|Coq]] proof assistant.
	* [http://jmleclipse.projects.cis.ksu.edu/ JMLEclipse], a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.		* [http://jmleclipse.projects.cis.ksu.edu/ JMLEclipse], a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
	* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], a symbolic execution based static analyzer which supports JML as a contract language.		* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], a symbolic execution based static analyzer which supports JML as a contract language.

Christian75: Adding local short description: "Specification language for Java programs", overriding Wikidata description "specification language for Java programs"

2023-03-16T15:46:48Z

Adding local short description: "Specification language for Java programs", overriding Wikidata description "specification language for Java programs"

← Previous revision		Revision as of 15:46, 16 March 2023
Line 1:		Line 1:
			{{Short description\|Specification language for Java programs}}
	The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].		The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].

93.144.21.240: the link no longer exists

2022-11-14T21:34:39Z

the link no longer exists

← Previous revision		Revision as of 21:34, 14 November 2022
Line 112:		Line 112:
	* [http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], a tool to generate files for running JUnit tests on JML annotated Java files.		* [http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], a tool to generate files for running JUnit tests on JML annotated Java files.
	* [https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO TACO], an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.		* [https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO TACO], an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.
	* [https://fmt.ewi.utwente.nl/redmine/projects/vercors-verifier/wiki VerCors verifier]

	== References ==		== References ==

PrimeBOT: /* top */Task 24: remove a maintenance template following a TFD

2022-01-18T20:37:58Z

top: Task 24: remove a maintenance template following a TFD

← Previous revision		Revision as of 20:37, 18 January 2022
Line 1:		Line 1:
	{{expert needed\|Japan\|ex2=Computing\|date=July 2010}}

	The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].		The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].

JPxG: Adding WikiProject-based categories as parameters to Template:Expert needed, Template:Expert etc, to clear out the unhelpful :Category:Articles needing unspecified expert attention.

2021-03-14T06:31:22Z

Adding WikiProject-based categories as parameters to Template:Expert needed, Template:Expert etc, to clear out the unhelpful Category:Articles needing unspecified expert attention.

← Previous revision		Revision as of 06:31, 14 March 2021
Line 1:		Line 1:
	{{expert needed\|date=July 2010}}		{{expert needed\|Japan\|ex2=Computing\|date=July 2010}}

	The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].		The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].

Mark in wiki: /* References */ wikilink added

2021-02-17T09:11:24Z

References: wikilink added

← Previous revision		Revision as of 09:11, 17 February 2021
Line 120:		Line 120:
	* [[Gary T. Leavens]], Albert L. Baker, and Clyde Ruby. ''JML: A Notation for Detailed Design''; in Haim Kilov, [[Bernhard Rumpe]], and Ian Simmonds (editors), ''Behavioral Specifications of Businesses and Systems'', Kluwer, 1999, chapter 12, pages 175-188.		* [[Gary T. Leavens]], Albert L. Baker, and Clyde Ruby. ''JML: A Notation for Detailed Design''; in Haim Kilov, [[Bernhard Rumpe]], and Ian Simmonds (editors), ''Behavioral Specifications of Businesses and Systems'', Kluwer, 1999, chapter 12, pages 175-188.
	* [[Gary T. Leavens]], Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. [http://www.jmlspecs.org/jmlrefman/jmlrefman_toc.html HTML]		* [[Gary T. Leavens]], Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. [http://www.jmlspecs.org/jmlrefman/jmlrefman_toc.html HTML]
	* Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. ''Formal specification with JML''. 2014. [http://primo.bibliothek.kit.edu/primo_library/libweb/action/dlDisplay.do?vid=KIT&docId=KITSRCE1000041881&tab=kit_evastar&srt=date download (CC-BY-NC-ND)]		* [[Marieke Huisman]], Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. ''Formal specification with JML''. 2014. [http://primo.bibliothek.kit.edu/primo_library/libweb/action/dlDisplay.do?vid=KIT&docId=KITSRCE1000041881&tab=kit_evastar&srt=date download (CC-BY-NC-ND)]

	== External links ==		== External links ==

DannyS712 bot: Task 70: Update syntaxhighlight tags - remove use of deprecated tags

2020-05-11T18:00:12Z

Task 70: Update syntaxhighlight tags - remove use of deprecated <source> tags

← Previous revision		Revision as of 18:00, 11 May 2020
Line 42:		Line 42:

	as well as standard [[Java syntax]] for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated and that have appropriate visibility. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like		as well as standard [[Java syntax]] for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated and that have appropriate visibility. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like
	<~~source~~ lang="java">		<syntaxhighlight lang="java">
	public class BankingExample		public class BankingExample
	{		{
Line 98:		Line 98:
	}		}
	}		}
			</syntaxhighlight>
	</source>
	Full documentation of JML syntax is available [http://jmlspecs.org/jmlrefman/jmlrefman_toc.html in the JML Reference Manual].		Full documentation of JML syntax is available [http://jmlspecs.org/jmlrefman/jmlrefman_toc.html in the JML Reference Manual].

InternetArchiveBot: Rescuing 1 sources and tagging 0 as dead.) #IABot (v2.0

2020-02-01T09:22:47Z

Rescuing 1 sources and tagging 0 as dead.) #IABot (v2.0

← Previous revision		Revision as of 09:22, 1 February 2020
Line 113:		Line 113:
	* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], a symbolic execution based static analyzer which supports JML as a contract language.		* [http://www.sireum.org/?q=node/21/ Sireum/Kiasan], a symbolic execution based static analyzer which supports JML as a contract language.
	* [http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], a tool to generate files for running JUnit tests on JML annotated Java files.		* [http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlunit.html JMLUnit], a tool to generate files for running JUnit tests on JML annotated Java files.
	* [http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO TACO], an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.		* [https://web.archive.org/web/20110706084805/http://www.dc.uba.ar/inv/grupos/rfm_folder/TACO TACO], an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.
	* [https://fmt.ewi.utwente.nl/redmine/projects/vercors-verifier/wiki VerCors verifier]		* [https://fmt.ewi.utwente.nl/redmine/projects/vercors-verifier/wiki VerCors verifier]

← Previous revision		Revision as of 17:30, 4 April 2024
Line 1:		Line 1:
	{{Short description\|Specification language for Java programs}}		{{Short description\|Specification language for Java programs}}
			{{No footnotes\|date=April 2024}}
	The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].		The '''Java Modeling Language''' ('''JML''') is a [[specification language]] for [[Java (programming language)\|Java]] programs, using [[Hoare logic\|Hoare style]] [[Precondition\|pre-]] and [[postcondition]]s and [[Invariant (computer science)\|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]].