Refinement Aliases don't work with Interfaces

Bắt đầu bằng cách chạy hai ví dụ Java từ issue và so sánh việc xử lý refinement aliases đối với các khai báo lớp trừu tượng và interface. Theo dõi các đường đi chuyển trạng thái và xử lý interface để xác định tại sao interface tạo ra sự không khớp trạng thái được hiển thị; hoàn thành có nghĩa là ví dụ interface được xác minh nhất quán với ví dụ lớp trừu tượng.

@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 
----------------------------------------------------------------------------------------------------------------------------------