Refinement Aliases don't work with Interfaces

Commencez par exécuter les deux exemples Java de l’issue et comparez la gestion des refinement aliases pour les déclarations de la classe abstraite et de l’interface. Suivez les chemins de transition d’état et de traitement des interfaces afin d’identifier pourquoi l’interface produit l’incohérence d’état présentée ; le travail est terminé lorsque l’exemple d’interface se vérifie de manière cohérente avec l’exemple de classe abstraite.

@RefinementAlias works as intended for classes and abstract classes but when attempting to use them for interfaces, LiquidJava is not able to correctly compare states

Example

import liquidjava.specification.*;
import java.util.ArrayList;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int x")
@RefinementAlias("IsZero(ArrayList t) {size(t) == 0}")
public abstract class Test1 {

	@StateRefinement(to = "IsZero(this)")
	public abstract void ArrayList();

	@StateRefinement(from = "(IsZero(this))")
	public abstract int get(int index);

}

class T1 {

	public static void main(String[] args) {
		ArrayList<Integer> list = new ArrayList<>();
		list.get(0);
	}
}

This example passes verification as intended, however

import liquidjava.specification.*;
import java.util.ArrayList;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int x")
@RefinementAlias("IsZero(ArrayList t) {size(t) == 0}")
public interface Test2 {

	@StateRefinement(to = "IsZero(this)")
	public abstract void ArrayList();

	@StateRefinement(from = "(IsZero(this))")
	public abstract int get(int index);

}

class T1 {

	public static void main(String[] args) {
		ArrayList<Integer> list = new ArrayList<>();
		list.get(0);
	}
}

This one fails, the only difference is the latter is declared as an interface and not an abstract class.

The error given is

______________________________________________________
Failed to check state transitions when calling list.get(0) in:

list.get(0)

Expected possible states:(IsZero(this))

State found:
----------------------------------------------------------------------------------------------------------------------------------
∀#list_6:ArrayList,  (IsZero(#list_6)) && x(#list_6) == x(old(#list_6)) 
----------------------------------------------------------------------------------------------------------------------------------

Instance translation table:
----------------------------------------------------------------------------------------------------------------------------------
| Variable Name                    | Created in                                                   | File 
----------------------------------------------------------------------------------------------------------------------------------
| #list_6                          | java.util.ArrayList<java.lang.Integer> list = new java.util.ArrayList<>() | Test2.java:20, 22 
----------------------------------------------------------------------------------------------------------------------------------