![]() | This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations .(April 2024) |
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.
JML is a behavioural interface specification language for Java modules. JML provides semantics to formally describe the behavior of a Java module, preventing ambiguity with regard to the module designers' intentions. JML inherits ideas from Eiffel, Larch and the Refinement Calculus, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer. Various tools are available that make use of JML's behavioral specifications. Because specifications can be written as annotations in Java program files, or stored in separate specification files, Java modules with JML specifications can be compiled unchanged with any Java compiler.
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 specification>
or
/*@ <JML specification> @*/
Basic JML syntax provides the following keywords
requires
ensures
signals
signals_only
assignable
pure
assignable \nothing
but can also throw exceptions). Furthermore, a pure method is supposed to always either terminate normally or throw an exception.invariant
loop_invariant
also
assert
spec_public
Basic JML also provides the following expressions
\result
\old(<expression>)
<expression>
at the time of entry into a method.(\forall <decl>; <range-exp>; <body-exp>)
(\exists <decl>; <range-exp>; <body-exp>)
a ==> b
a
implies b
a <== b
a
is implied by b
a <==> b
a
if and only if b
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
publicclassBankingExample{publicstaticfinalintMAX_BALANCE=1000;private/*@ spec_public @*/intbalance;private/*@ spec_public @*/booleanisLocked=false;//@ public invariant balance >= 0 && balance <= MAX_BALANCE;//@ assignable balance;//@ ensures balance == 0;publicBankingExample(){this.balance=0;}//@ requires 0 < amount && amount + balance < MAX_BALANCE;//@ assignable balance;//@ ensures balance == \old(balance) + amount;publicvoidcredit(finalintamount){this.balance+=amount;}//@ requires 0 < amount && amount <= balance;//@ assignable balance;//@ ensures balance == \old(balance) - amount;publicvoiddebit(finalintamount){this.balance-=amount;}//@ ensures isLocked == true;publicvoidlockAccount(){this.isLocked=true;}//@ requires !isLocked;//@ ensures \result == balance;//@ also//@ requires isLocked;//@ signals_only BankingException;public/*@ pure @*/intgetBalance()throwsBankingException{if(!this.isLocked){returnthis.balance;}else{thrownewBankingException();}}}
Full documentation of JML syntax is available in the JML Reference Manual.
A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc
which converts JML annotations into runtime assertions, a documentation generator jmldoc
which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit
which generates JUnit test code from JML annotations.
Independent groups are working on tools that make use of JML annotations. These include:
Eiffel is an object-oriented programming language designed by Bertrand Meyer and Eiffel Software. Meyer conceived the language in 1985 with the goal of increasing the reliability of commercial software development; the first version becoming available in 1986. In 2005, Eiffel became an ISO-standardized language.
Design by contract (DbC), also known as contract programming, programming by contract and design-by-contract programming, is an approach for designing software.
The Vienna Development Method (VDM) is one of the longest-established formal methods for the development of computer-based systems. Originating in work done at the IBM Laboratory Vienna in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language—the VDM Specification Language (VDM-SL). It has an extended form, VDM++, which supports the modeling of object-oriented and concurrent systems. Support for VDM includes commercial and academic tools for analyzing models, including support for testing and proving properties of models and generating program code from validated VDM models. There is a history of industrial usage of VDM and its tools and a growing body of research in the formalism has led to notable contributions to the engineering of critical systems, compilers, concurrent systems and in logic for computer science.
In computing, aspect-oriented programming (AOP) is a programming paradigm that aims to increase modularity by allowing the separation of cross-cutting concerns. It does so by adding behavior to existing code without modifying the code, instead separately specifying which code is modified via a "pointcut" specification, such as "log all function calls when the function's name begins with 'set'". This allows behaviors that are not central to the business logic to be added to a program without cluttering the code of core functions.
In computer programming, specifically when using the imperative programming paradigm, an assertion is a predicate connected to a point in the program, that always should evaluate to true at that point in code execution. Assertions can help a programmer read the code, help a compiler compile it, or help the program detect its own defects.
In computer programming, specifically object-oriented programming, a class invariant is an invariant used for constraining objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object.
ESC/Java, the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as extended static checking, which is a collective name referring to a range of techniques for statically checking the correctness of various program constraints. For example, that an integer variable is greater-than-zero, or lies between the bounds of an array. This technique was pioneered in ESC/Java and can be thought of as an extended form of type checking. Extended static checking usually involves the use of an automated theorem prover and, in ESC/Java, the Simplify theorem prover was used.
This article compares two programming languages: C# with Java. While the focus of this article is mainly the languages and their features, such a comparison will necessarily also consider some features of platforms and libraries. For a more detailed comparison of the platforms, see Comparison of the Java and .NET platforms.
The syntax of Java is the set of rules defining how a Java program is written and interpreted.
Many programming language type systems support subtyping. For instance, if the type Cat
is a subtype of Animal
, then an expression of type Cat
should be substitutable wherever an expression of type Animal
is used.
C# is a general-purpose high-level programming language supporting multiple paradigms. C# encompasses static typing, strong typing, lexically scoped, imperative, declarative, functional, generic, object-oriented (class-based), and component-oriented programming disciplines.
In the Java computer programming language, an annotation is a form of syntactic metadata that can be added to Java source code. Classes, methods, variables, parameters and Java packages may be annotated. Like Javadoc tags, Java annotations can be read from source files. Unlike Javadoc tags, Java annotations can also be embedded in and read from Java class files generated by the Java compiler. This allows annotations to be retained by the Java virtual machine at run-time and read via reflection. It is possible to create meta-annotations out of the existing ones in Java.
Haxe is a high-level cross-platform programming language and compiler that can produce applications and source code for many different computing platforms from one code-base. It is free and open-source software, released under the MIT License. The compiler, written in OCaml, is released under the GNU General Public License (GPL) version 2.
This article describes the syntax of the C# programming language. The features described are compatible with .NET Framework and Mono.
The ANSI/ISO C Specification Language (ACSL) is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as C annotation comments to the C program, which hence can be compiled with any C compiler.
The expression problem is a challenging problem in programming languages that concerns the extensibility and modularity of statically typed data abstractions. The goal is to define a data abstraction that is extensible both in its representations and its behaviors, where one can add new representations and new behaviors to the data abstraction, without recompiling existing code, and while retaining static type safety. The statement of the problem exposes deficiencies in programming paradigms and programming languages, and as of 2023 is still considered unsolved, although there are many proposed solutions.
Whiley is an experimental programming language that combines features from the functional and imperative paradigms, and supports formal specification through function preconditions, postconditions and loop invariants. The language uses flow-sensitive typing also known as "flow typing."
Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go and Python. It supports formal specification through preconditions, postconditions, loop invariants, loop variants, termination specifications and read/write framing specifications. The language combines ideas from the functional and imperative paradigms; it includes support for object-oriented programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#.
ECMAScript is a JavaScript standard developed by Ecma International. Since 2015, major versions have been published every June.