Ghost variables are not correctly initialized in interfaces
@pcanelas ya está trabajando en esto.
Desde el 4/7/2025.
Evaluación
Este issue todavía no se ha evaluado.
Descripción
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
- Lenguaje dominante
- Java
- Estrellas
- 67
- Forks
- 36
- Merge medio
- 10 d 18 h
- PR fusionados (30 d)
- 3
Guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de liquid-java/liquidjava
-
enhancement
liquid-java/liquidjava#240 · 1 asignado ·
-
enhancement ide
Dificultad 3/5 1-2 días Aptitud para principiantes 45/100
liquid-java/liquidjava#206 ·
-
tests
Dificultad 2/5 1-3 horas Aptitud para principiantes 25/100
liquid-java/liquidjava#198 ·
-
Diagnostic Based Test Results Abiertotests
Dificultad 4/5 3-5 días Aptitud para principiantes 25/100
liquid-java/liquidjava#197 ·
-
tests
Dificultad 4/5 3-5 días Aptitud para principiantes 35/100
liquid-java/liquidjava#196 · 2 comentarios ·
Todos los issues de liquid-java/liquidjava
Issues similares
-
bug
Dificultad 2/5 1-3 horas Aptitud para principiantes 85/100
-
Two open-case totals on one screen: the Programs tile says 15,858 and the nav badge says 15,868 Abiertobug frontend maui-pilot
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 76/100
objectionary/eo-graphs#74 ·
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 65/100