Project developed at Lasige logo FCUL logo




content-photo

Extending Java with
Refinement Types

Extend your Java code with Refinement Types and catch more bugs!
LiquidJava implements an additional type system with Refinement Types on top of Java. It allows developers to express better restrictions on the code and discover more bugs before executing the program.







Install LiquidJava plugin

Download here the Visual Studio Code plugin

Requirements:
Visual Studio Code

JDK 11
Language Support for Java by Red Hat plugin

Command Line

1. Open the terminal in the folder of the downloaded .vsix file
2. Insert the command:

code --install-extension liquid-java-0.0.14.vsix

VSCode GUI

1. Open the Extensions side view inside VSCode;
2. Expand More Actions clicking on ... on the top;
3. Install from VSIX;
4. Select downloaded file;
5. Re-open VSCode.



Use example:
  1. Install the IDE Extension
  2. Clone the github exercises repository
  3. Open the folder parte3-liquidJava/together1 on VSCode
  4. Wait for the notification "LiquidJava Extension is ON! Enjoy!" and uncomment the code in one of the Test.java files. An error should appear underlining the incorrect part. Hover the element or open the Problems tab for more error information.

Predicates

Refinement Types extend a language with predicates over the basic types. @Refinement("x > 0") int x; is an example of a variable x that has the basic type int, and is refined with the predicate x > 0.
The predicates allowed inside the refinement belong to quantifier-free linear integer arithmetic logic. Some examples can be seen below.

Equals     ==

@Refinement("x == 0")
int x;

Different     !=

@Refinement("x != 0")
int x;

Inequality Symbols     > >= < <=

@Refinement("y <= 0")
int y = 0;

Negate     !

@Refinement("!(y > 0)")
int y = -200;

And     &&

@Refinement("(0 <= y) && (y <= 100)")
int y = 25;

Or     ||

@Refinement("(x == 0) || (x == 100)")
int y = 100;

Arithmetic Operators     + - * / %

@Refinement("(v + 20) < 100")
int v = 79;

Arithmetic Operators     * / %

@Refinement("(odd % 2) != 0")
int odd = 5;

Represent Variable     _

@Refinement("_ > 0 ")
int y = 100;

If then else     ()? ():()

@Refinement("(a > b)? (_ == a) : (_ == b)")
public int max(int a, int b){...}

To simplify the usage of refinements, we can create Predicate Aliases and apply them to the variables inside a @Refinement.


Alias

@RefinementAlias("Percentage(int v) { 0 <= v && v <= 100 }")
public class X {...}

Alias Usage

@Refinement("Percentage(y)")
int y = 25;

Refinements can also be used to model Object State by adding the possible states and transitions to the class and the desired Ghost predicates to model class properties.

Class States

@StateSet({"open", "close"})
public class ReadFile{...}

Use States

@StateRefinement(from="open(this)", to="close(this)")
public void closeFile(){...}

Class Ghost

@Ghost("int size")
public class List{...}

Use Ghost

@StateRefinement(to = "size(this) == (size(old(this)) + 1)")
public void add(int elem){...}

Refinements in Variables

We can add a @Refinement in any place we already have a basic type in the code. Hence, in declarations of variable or class fields it is possible to add a refinement type.

Positive

The variable has a value greater than zero.

            @Refinement("positive > 0")
            int positive;
            positive = 50; //Correct
            positive = -1; //Error
        

Percentage

Lower and upper bounds are set to the variable. The _ represents the variable on which the refinement is being applied, in this case _ >= 0 is the same as percentage >= 0.

            @Refinement("_ >= 0 && _ <= 100")
            int percentage;

            percentage = 50; //Correct
            percentage = 10 + 99; //Error
        

RGB fields

Class fields can have refinements just like any local variable. This example shows the use of the Alias RGB in the fields of MyColor class. The alias limits the values that an rgb color can have (an interval between 0 and 255) ensuring that each field only has values that belong to the correct interval.

@RefinementAlias("RGB(int x) {x >= 0 && x <= 255}")
class MyColor{
  @Refinememt("RGB(r)") int r;
  @Refinememt("RGB(_)") int g;
  @Refinememt("RGB(_)") int b;
}



Refinements in Methods

In methods, both the parameters and the return value can have refined types.
The parameters refinements will ensure that the method is only invoked with the expected types.
The return refinement guarantees that the return inside the method's body corresponds to the expected type.

Absolute

To refine the return type of a method, we can add the @Refinement annotation above the method. We use the _ wild variable to refer to the return value. In this example, we state that the return of absolute has a value between 0 and the parameter n.


@Refinement("_ >= 0 && _ >= n")
public static int absolute(int n) {
  if(0 <= n)
      return n;
  else
      return 0 - n;
}

Add Bonus - Grade

We can also refine the type of the method's parameters. In this example, both parameters have to be a Percentage (alias for _ >= 0 && _ <= 100) and bonus must be lesser than grade.
We can refer to a previous parameter in the current parameter's refinement, but not the other way around. For example, bonus can refer to grade but grade cannot use bonus in its refinement.


@RefinementAlias("Percentage(int x) { x >= 0 && x <= 100}")
public class Grade{

    @Refinement("Percentage(_)")
    public static int addBonus(@Refinement("Percentage(_)")
                               int grade,
                               @Refinement("Percentage(_) && bonus < grade")
                               int bonus){
        if((bonus + grade) > 100)
            return 100;
        else
            return grade + bonus;
    }

}

Refinements in Classes

LiquidJava contains the mechanisms to model Object Type State.
Since class methods can have effects on the internal state of objects, each method can be annotated with the allowed state transitions using the @StateRefinement(from = "...", to = "...") annotation. In this annotation, the from argument represents the object states in which the method can be invoked, whereas the to argument represents the state the object will have at the end of the method execution.
There are two possibilities of modelling object state:
State Sets: If a class has a defined set of states, it is possible to create multiple @StateSet that include the allowed object states.
Ghost Properties: To model other properties (int or boolean) it is possible to create @Ghost properties that work as uninterpreted functions.
In either case, whenever there is a need to refer to the previous state of the object, it is possible to use the old keyword.

If a class follows an implicit protocol that can be described by a DFA, then the protocol can be described in LiquidJava to ensure that the different methods are invoked in the correct order.
To define the possible object states we create a string array with their names inside the @StateSet annotation.
Then these states can be used inside @StateRefinement annotations to ensure the object state of the object in the beginning of the method call (from) and change the state at the end of the invocation (to).
This example implements an order for the composition of an email:
- Constructor - constructor starts the object with emptyEmail state
- From Method - changes state from emptyEmail to senderSet
- To Method - can accept the object in senderSet state or receiverSet state
- Subject Method - the object needs to be in receiverSet state but does not transition to another, staying in the same state. The invocation of this method is optional to complete the protocol
- Method Body - once the receiver is set the body of the email also be set, changing the object state to bodySet.

@StateSet({"emptyEmail", "receiverSet", "senderSet", "bodySet"})
public class Email {

  @StateRefinement(to = "emptyEmail(this)")
  public Email() {...}

  @StateRefinement(from = "emptyEmail(this)", to = "senderSet(this)")
  public void from(String s) {...}

  @StateRefinement(from = "(senderSet(this)) || (receiverSet(this))",
                   to =  "receiverSet(this)")
  public void to(String s) {...}

  @StateRefinement(from = "receiverSet(this)",  to = "receiverSet(this)")
  public void subject(String s) {...}

  @StateRefinement(from= "receiverSet(this)", to = "bodySet(this)")
  public void body(String s) {...}

}

Invocation

//Correct
Email e = new Email();
e.from("Alice");
e.to("Bob");
e.to("Carol");
e.body();

//Error
Email e = new Email();
e.to("Bob");
e.from("Alice");
e.to("Carol");
e.subject("Hello World!");
e.body();