Ghost variables are not correctly initialized in interfaces
@pcanelas がすでに取り組んでいます。
2025年7月4日 から。
評価
この issue はまだ評価されていません。
説明
Ghost variable initialization is dependent on declaring the constructor for the type the that the refinements are for. This declaration implicitly initializes int variables in a way equivalent to @StateRefinement(to = "var(this) == 0")
It is not possible to declare constructors for interface types as these don't have constructors. This prohibits the correct initialization of both Ghost variables and States for interfaces
@ExternalRefinementsFor("java.util.List")
@Ghost("int size2")
public interface ListRefinements<E> {
@StateRefinement(to = "size2(this) == (size2(old(this)) + 1)")
public boolean add(E elem);
@StateRefinement(from = "size2(this) > 0", to = "size2(this) == (size2(old(this)) - 1)")
public void remove(@Refinement("index >= 0") int index);
}
public static void main(String[] args) {
List<Integer> l = new ArrayList<>();
l.add(0);
int a = l.remove(0);
}
The error provided is Failed to check state transitions when calling l.remove(0)
This error messages is identical to the error message that would appear when attempting the same operation on a concrete class without a declared constructor in the Refinement definitions
- 主要言語
- Java
- スター
- 67
- フォーク
- 36
- 平均マージ
- 10日 18時間
- マージ済み PR（30日）
- 3
コントリビューションガイド
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
liquid-java/liquidjava のほかの issue
-
enhancement
liquid-java/liquidjava#240 · 担当者 1 名 ·
-
enhancement ide
難易度 3/5 1〜2日 初心者へのやさしさ 45/100
liquid-java/liquidjava#206 ·
-
tests
難易度 2/5 1〜3時間 初心者へのやさしさ 25/100
liquid-java/liquidjava#198 ·
-
tests
難易度 4/5 3〜5日 初心者へのやさしさ 25/100
liquid-java/liquidjava#197 ·
-
tests
難易度 4/5 3〜5日 初心者へのやさしさ 35/100
liquid-java/liquidjava#196 · コメント 2 件 ·
liquid-java/liquidjava の issue をすべて見る
似ている issue
-
bug untriaged
難易度 2/5 1〜3時間 初心者へのやさしさ 84/100
opensearch-project/ml-commons#5094 ·
-
bug
難易度 2/5 1〜3時間 初心者へのやさしさ 85/100
-
emitter:client:csharp feature
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
-
affects/8.10 affects/8.9 component/clients kind/bug likelihood/mid severity/mid
難易度 2/5 1〜3時間 初心者へのやさしさ 78/100
-
Two open-case totals on one screen: the Programs tile says 15,858 and the nav badge says 15,868 オープンbug frontend maui-pilot
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100