liquid-java / liquid-java/liquidjava

Refinement Aliases don't work with Interfaces

未關閉
#50 2 則留言 0 個 reaction 已指派 0 人 在 GitHub 檢視

還沒有人認領這個 Issue。

bug
主要語言
Java
星號
67
分支
36
平均合併
10 天 18 小時
30 天內合併 PR
3

描述

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

貢獻指南

開啟貢獻指南

從這裡開始

  1. 先讀完整個 Issue,再讀專案的貢獻指南。
  2. 在 Issue 下留言說明你要接手 —— 這能避免兩個人做同樣的事。
  3. Fork 儲存庫,在一個分支上完成修改。
  4. 送出 Pull Request,並在描述裡引用這個 Issue 編號。

研究方向

先執行 issue 中的兩個 Java 範例,並比較抽象類別與介面宣告的 refinement aliases 處理方式。追蹤狀態轉換與介面處理路徑,以找出介面為何會產生所示的狀態不一致;完成的標準是介面範例能與抽象類別範例一致地通過驗證。

由索引模型根據 Issue 內容生成。

評估

技術堆疊
java
領域
compilers
Issue 類型
缺陷
難度
4/5
預估耗時
3-5 天
活躍度
停滯
描述清晰度
基本清楚
新手友好度
35/100

把新 issue 寄到你的電子郵件信箱

精選適合新手參與的 GitHub issue 摘要。