liquid-java / liquid-java/liquidjava
Refinement Aliases don't work with Interfaces
まだ誰も着手していません。
- 主要言語
- Java
- スター
- 67
- フォーク
- 36
- 平均マージ
- 10日 18時間
- マージ済み PR(30日)
- 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
-
```java
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 list = new ArrayList<>();
list.get(0);
}
}
```
This example passes verification as intended, however
```java
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 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 list = new java.util.ArrayList<>() | Test2.java:20, 22
----------------------------------------------------------------------------------------------------------------------------------
```
コントリビューションガイド
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
調査の方向性
まず issue にある 2 つの Java の例を実行し、抽象クラスとインターフェースの宣言に対する refinement aliases の処理を比較します。状態遷移とインターフェース処理の経路を追跡して、なぜインターフェースが示されている状態の不一致を生成するのかを特定します。完了とは、インターフェースの例が抽象クラスの例と一貫して検証されることです。
索引モデルが issue の本文から書いたものです。
評価
- 技術スタック
- java
- 領域
- compilers
- issue の種類
- バグ
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 活発さ
- 停滞
- 明瞭さ
- おおむね明確
- 初心者へのやさしさ
- 35/100