liquid-java / liquid-java/liquidjava
Ghost variables are not correctly initialized in interfaces
@pcanelas ci sta già lavorando.
Dal 4/7/2025.
- Lingua principale
- Java
- Stelle
- 67
- Fork
- 36
- Merge medio
- 10g 18h
- PR unite (30g)
- 3
Descrizione
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
```java
@ExternalRefinementsFor("java.util.List")
@Ghost("int size2")
public interface ListRefinements {
@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);
}
```
```java
public static void main(String[] args) {
List 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
Guida per i contributori
Apri la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Valutazione
Questa issue non è ancora stata valutata.