JML – Java Modelling Language and KeY Prover

JML (Java Modeling Language) provides several keywords and constructs to specify properties of Java programs. Here are some common ones:

1. \old(expression): Represents the value of an expression before the execution of the method.
2. \result: Represents the return value of a method.
3. \forall type identifier; condition; expression: Quantifies over all elements of a collection.
4. \exists type identifier; condition; expression: Quantifies over at least one element of a collection.
5. \nothing: Represents the absence of a value, used typically in ensures clauses to specify that something does not change.
6. /*@ pure @*/: Indicates that a method has no side effects and its return value depends only on its parameters.
7. /*@ non_null @*/: Indicates that a method’s return value or a field cannot be null.
8. /*@ nullable @*/: Indicates that a method’s return value or a field can be null.
9. /*@ invariant condition; */: Specifies a class or interface invariant.
10. //@ requires condition;: Specifies a precondition for a method.
11. //@ ensures condition;: Specifies a postcondition for a method.
12. //@ assignable expressions;: Specifies which variables may be modified by the method.
13. // @param
    
    

These are some of the most commonly used constructs in JML specifications. They allow you to specify various properties of Java methods and classes formally.

JML follows Backus-Naur Form (BNF) grammar

jml-special-symbol ::= ==> | <== | <==> | <=!=> | -> | <- | <: | .. | ‘{|’ | ‘|}’ | <# | <#=

illegal line er ekta bepar asey writing e , oita dekhte hobe
Annotations must hold entire grammatical units of JML specifications, in the sense that the text of some nonterminals may not be split across two separate annotations. For example the following is illegal, because the postcondition of the ensures clause is split over two annotations, and thus each contains a fragment instead of a complete grammatical unit. //@ ensures 0 <= x // illegal! //@ && x < a.length;

ref:
https://www.cs.ucf.edu/~leavens/JML/refman/jmlrefman.pdf

what is the meaning of public normal_behavior in jml?

In Java Modeling Language (JML), public normal_behavior is a specification clause used to describe the normal behavior of a method. Here’s what it means:

1. Visibility Modifier: public specifies that this behavior is publicly accessible from outside the class.
2. Behavior Type: normal_behavior indicates that the specifications following this clause describe the expected behavior of the method under normal circumstances.

When you use public normal_behavior, you are essentially stating that the specifications that follow pertain to the normal operation of the method when it is invoked under typical conditions.

Within the normal_behavior block, you can include requires, ensures, modifies, and other clauses to specify preconditions, postconditions, and other aspects of the method’s behavior. These specifications serve as formal documentation of what the method should do, which can aid in understanding, testing, and verifying the correctness of the code.

Solution about swapping and with KeY proving :

public class Swap {
public int x, y;

/*@
  public normal_behavior
  requires true;
  ensures x == \old(y) && y == \old(x);
@*/

public void swapViaPlusMinus() {        
    // Swapping using add/subtract method
    x = x + y;
    y = x - y;
    x = x - y;
}

public static void main(String[] args) {
    // Testing the swapViaPlusMinus method
    Swap swap = new Swap();
    swap.x = 5;
    swap.y = 10;
    swap.swapViaPlusMinus();
}

}

Tips: don’t use any extra info like print out in method, otherwise it will not make the KeY prover goal success

Also some jml needful ref: https://formal.kastel.kit.edu/beckert/teaching/Formale-Verifikation-SS09/05JML.pdf
KeY Prover:

Tool to check if written java code with jml spec is correct.

ref: https://www.key-project.org/
https://www.key-project.org/getting-started/

chapter 15: https://formal.kastel.kit.edu/biblio/projects/key/chapter15.pdf
chapter 16: https://formal.kastel.kit.edu/beckert/pub/keytutorial2016.pdf
chapter 17: https://www.informatik.tu-darmstadt.de/media/se/publication_preprints/key_book_preprints/KeY_Hoare.pdf
student notes: https://formal.kastel.kit.edu/key/download/hoare/students.pdf

Hoare Logic to JML

The specication
{T}
R := X;
Q := 0;
WHILE Y <= R DO (R := R – Y; Q := Q + 1)
{R < Y ^ X = R + (Y X Q)}
whenever the given sequence of commands is executed, then Q is
the quotient and R is the remainder of dividing X into Y.

This snippet appears to be a program or algorithm written in a notation similar to Hoare logic. Let’s break it down:

• {T}: This represents the precondition, denoted by “T”. It specifies the conditions that must be true before the execution of the program.
• R := X;: This assigns the value of X to the variable R.
• Q := 0;: This assigns the value of 0 to the variable Q.
• WHILE Y <= R DO: This initiates a loop that continues while Y is less than or equal to R.
• (R := R - Y; Q := Q + 1): This is the body of the loop. It subtracts Y from R and increments Q by 1.
• {R < Y ^ X = R + (Y * Q)}: This represents the postcondition, denoted by “R < Y ^ X = R + (Y * Q)”. It specifies the conditions that must hold true after the execution of the program.

So, in Hoare logic terms:

• The precondition specifies the initial state of the program.
• The loop represents the iterative process.
• The postcondition specifies the desired properties that must hold true after the program has finished executing.

JML from here:

/**
 * This method divides an integer x by an integer y and assigns the quotient to q
 * and the remainder to r.
 *
 * @param x the dividend
 * @param y the divisor (must not be zero)
 * @param q the variable to store the quotient
 * @param r the variable to store the remainder
 * @requires y != 0
 * @ensures r < y && x == r + (y * q)
 */
public static void divideWithRemainder(int x, int y, int[] q, int[] r) {
    // Implementation not shown
}

Explanation:

• @param x: Describes the dividend.
• @param y: Describes the divisor.
• @param q: Describes the variable to store the quotient.
• @param r: Describes the variable to store the remainder.
• @requires y != 0: Specifies that the divisor must not be zero because division by zero is undefined.
• @ensures r < y && x == r + (y * q): Ensures that the remainder r is less than y, which aligns with the postcondition R < Y from the Hoare logic-like notation. Additionally, it ensures that the dividend x equals the remainder r plus the product of the divisor y and the quotient q, which aligns with the postcondition X = R + (Y * Q) from the Hoare logic-like notation.

In the provided JML specification, the precondition (@requires) and postcondition (@ensures) are as follows:

• Precondition (@requires):
  • y != 0: Specifies that the divisor y must not be zero, ensuring that division by zero does not occur. This condition ensures the safety of the method and prevents undefined behavior.
• Postcondition (@ensures):
  • r < y: Ensures that the remainder r is less than the divisor y, aligning with the condition R < Y from the Hoare logic-like notation.
  • x == r + (y * q): Ensures that the dividend x equals the remainder r plus the product of the divisor y and the quotient q, aligning with the condition X = R + (Y * Q) from the Hoare logic-like notation.

These conditions define the expected behavior and properties of the method both before and after its execution, respectively. The precondition specifies the conditions that must be true before the method is called, and the postcondition specifies the conditions that must hold true after the method has executed.

what is param x, param y then ?ChatGPT

Apologies for the oversight. Let me clarify:

In the provided JML specification:

• @param x: Describes the parameter representing the dividend.
• @param y: Describes the parameter representing the divisor.

These annotations are used to document the parameters of the method. They indicate that x is the dividend and y is the divisor. This documentation helps users of the method understand the purpose and usage of each parameter. However, in the context of preconditions and postconditions, they do not directly represent pre- or postconditions themselves. Instead, the @requires and @ensures annotations are used for that purpose, specifying the conditions that must hold true before and after the execution of the method, respectively.

code:

public class DivisionViaSubtraction {
    public int x, y, q, r;

    /*@
      @ public normal_behavior
      @ requires y != 0;
      @ ensures r < y && x == r + (y * q);
      @ diverges true;
      @*/
    public void divide() {
        r = x;
        q = 0;
        /*@
          @ loop_invariant r >= 0 && r < |y|;
          @ loop_invariant x == r + (y * q);
          @ decreases r;
          @*/
        while (y <= r) {
            r = r - y;
            q = q + 1;
        }
    }
}

Key Hoare:
Some syntax to follow:

• In order to do the verication in the tool, we have to
  declare the variables.
  \functions{
  int x0;
  int y0;
  }
  \programVariables{
  int x,y, d;
  }
  \hoare{ { x = x0&y = y0 }
  [{ d = x;
  x = y;
  y = d; }]
  { x = y0&y = x0 } }

ref: https://cs.unibg.it/gargantini/didattica/info3/restricted/anni_passati/200809/M7_KeyHoare.pdf