Program Specifications and the Java Modeling Language

Program specification refers to precise statements specifying properties of a program. According to the language adopted, program specifications can be categorized into natural language ones and formalized ones. A significant portion of program specifications is articulated using formal languages, such as mathematical expressions to specify the constraints on program behaviors, and automata to describe the transitions of program states. Formalized specifications have been widely adopted in automated software engineering tasks, such as requirement engineering, software testing, and model checking.

In this work, we mainly focus on formal specifications written in Java Modeling Language (JML) describing the actual behaviors of Java programs. One example program and corresponding ground-truth specifications are illustrated in Fig.1. The specifications take the form of comments starting with //@. Generally, the specifications involved can be divided into three categories: Preconditions (Line 1), Postconditions (Line 2), and Loop Invariants (Line 5, 6, and 7).

Preconditions (line 1), described in requires statements, specify the constraints on input variables that must be met before the corresponding function (i.e., isPalindrome here) is executed.
Postconditions (line 2), described in ensures statements, specify the properties of the returned value that always hold after the corresponding function is executed.
Loop Invariants (lines 5, 6, and 7), described in maintaining statements, specify the constraints on the local variables that always hold each time before the loop body is executed.

Together, the specifications constitute a detailed articulation of the semantics of the target program. For the method isPalindrome as a whole, preconditions and postconditions specify its overall requirements and functionalities. For the internal implementation of isPalindrome, loop invariants reveal the pattern followed by local variables when their values are updated.

It is worth noting that formalized program specifications are rigorous and unambiguous compared with specifications in natural language. Moreover, formalized program specifications can thoroughly articulate program semantics. Program semantics essentially lies in the evolution of program states, which are usually defined by the set of variable values. By specifying the constraints on program variables or the transition of program states, strong program specifications are rich in semantic information and can accurately capture program behaviors. In addition, the correctness of formal specifications can be effectively validated by specification verifiers (e.g., OpenJML), which can automatically check the consistency between the given specifications and the target program. Consequently, compared with natural language specifications, the correctness of program specifications can be automatically verified.

Page updated

Google Sites

Report abuse