liquid-java / liquid-java/liquidjava
Refinement Aliases don't work with Interfaces
未關閉
還沒有人認領這個 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
----------------------------------------------------------------------------------------------------------------------------------
貢獻指南
從這裡開始
- 先讀完整個 Issue,再讀專案的貢獻指南。
- 在 Issue 下留言說明你要接手 —— 這能避免兩個人做同樣的事。
- Fork 儲存庫,在一個分支上完成修改。
- 送出 Pull Request,並在描述裡引用這個 Issue 編號。
研究方向
先執行 issue 中的兩個 Java 範例,並比較抽象類別與介面宣告的 refinement aliases 處理方式。追蹤狀態轉換與介面處理路徑,以找出介面為何會產生所示的狀態不一致;完成的標準是介面範例能與抽象類別範例一致地通過驗證。
由索引模型根據 Issue 內容生成。
評估
- 技術堆疊
- java
- 領域
- compilers
- Issue 類型
- 缺陷
- 難度
- 4/5
- 預估耗時
- 3-5 天
- 活躍度
- 停滯
- 描述清晰度
- 基本清楚
- 新手友好度
- 35/100