liquid-java / liquid-java/liquidjava

Ghost variables are not correctly initialized in interfaces

Open
#44 1 comment 0 reactions 1 assignee View on GitHub

@pcanelas is already working on this.

Since Jul 4, 2025.

bug enhancement
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

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.