search

OpenJML / OpenJML

This is the primary repository for the source code of the OpenJML project. The source code is licensed under GPLv2 because it derives from OpenJDK which is so licensed. The active issues list for OpenJML development is here and the wiki contains information relevant to development. Public documentation for users is at the project website:
http://www.openjml.org
140 stars 33 forks source link

Support for primitive arbitrary precision numeric types. #12

Open openjml-project opened 21 years ago

openjml-project commented 21 years ago

Details are given in the two papers cited below (and available from http://www.cs.concordia.ca/~faculty/chalin).

* Improving JML: For a Safer and More Effective Language. TR 2003-001.2, Computer Science Department, Concordia University, May 2003.

Abstract. An unusually high number of published JML specifications are invalid or inconsistent, including cases from the security critical area of smart card applications. We claim that these specification errors are due to a mismatch between user expectations and the current JML semantics of expressions over numeric types. After a short discussion of JML language design goals and objectives, we introduce JMLa, an adaptation of JML supporting primitive arbitrary precision numeric types. To support our claim that the identified specification errors are due to JMLs divergence from user expectations, we demonstrate that the invalidities and inconsistencies disappear under JMLa semantics with either no, or minor syntactic changes to the specifications. Other advantages of JMLa are illustrated including safetyhow it allows an automated static checker like ESC/Java to detect more specification and implementation errors.

* JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics (Extended Abstract). TR 2003-002.1, Computer Science Department, Concordia University, May 2003.

Original comment by: chalin

openjml-project commented 18 years ago

Logged In: YES user_id=633675

Is this done (or half done)?

Original comment by: leavens

davidcok commented 7 years ago

The primitive types are supported in OpenJML. Not all the details of the arithmetic modes are supported yet. I think this issue was originally entered against JML2, but we'll take it now as a reminder to finish arithmetic modes in OpenJML