liquid-java / liquid-java/liquidjava
Ghost variables are not correctly initialized in interfaces
@pcanelas is already working on this.
Since Jul 4, 2025.
- Dominant language
- Java
- Stars
- 67
- Forks
- 36
- Avg merge
- 10d 18h
- Merged PRs (30d)
- 3
Description
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
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.