Refinement Aliases don't work with Interfaces

まず issue にある 2 つの Java の例を実行し、抽象クラスとインターフェースの宣言に対する refinement aliases の処理を比較します。状態遷移とインターフェース処理の経路を追跡して、なぜインターフェースが示されている状態の不一致を生成するのかを特定します。完了とは、インターフェースの例が抽象クラスの例と一貫して検証されることです。

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