Sunbelt Computer Software

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;
    }

}

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();