liquid-java / liquid-java/liquidjava
Ghost variables are not correctly initialized in interfaces
@pcanelas arbeitet bereits daran.
Seit 04.7.2025.
- Vorherrschende Sprache
- Java
- Sterne
- 67
- Forks
- 36
- Ø Merge
- 10 T. 18 Std.
- Gemergte PRs (30 T.)
- 3
Beschreibung
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
Beitragsleitfaden
Erste Schritte
- Lies das ganze Issue und danach den Beitragsleitfaden des Projekts.
- Schreib ins Issue, dass du es übernimmst — das erspart doppelte Arbeit.
- Forke das Repository und arbeite in einem Branch.
- Öffne einen Pull Request, der die Issue-Nummer nennt.
Bewertung
Dieses Issue wurde noch nicht bewertet.