liquid-java / liquid-java/liquidjava

Ghost variables are not correctly initialized in interfaces

Offen
#44 1 Kommentar 0 Reaktionen 1 zugewiesene Person Auf GitHub ansehen

@pcanelas arbeitet bereits daran.

Seit 04.7.2025.

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

Beitragsleitfaden öffnen

Erste Schritte

  1. Lies das ganze Issue und danach den Beitragsleitfaden des Projekts.
  2. Schreib ins Issue, dass du es übernimmst — das erspart doppelte Arbeit.
  3. Forke das Repository und arbeite in einem Branch.
  4. Öffne einen Pull Request, der die Issue-Nummer nennt.

Bewertung

Dieses Issue wurde noch nicht bewertet.

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.