liquid-java / liquid-java/liquidjava

Refinement Aliases don't work with Interfaces

Open
#50 2 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

bug
Dominant language
Java
Stars
67
Forks
36
Avg merge
10d 18h
Merged PRs (30d)
3

Description

`@RefinementAlias` works as intended for classes and abstract classes but when attempting to use them for interfaces, LiquidJava is not able to correctly compare states

Example
-
```java
import liquidjava.specification.*;
import java.util.ArrayList;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int x")
@RefinementAlias("IsZero(ArrayList t) {size(t) == 0}")
public abstract class Test1 {

@StateRefinement(to = "IsZero(this)")
public abstract void ArrayList();

@StateRefinement(from = "(IsZero(this))")
public abstract int get(int index);

}

class T1 {

public static void main(String[] args) {
ArrayList list = new ArrayList<>();
list.get(0);
}
}
```
This example passes verification as intended, however
```java
import liquidjava.specification.*;
import java.util.ArrayList;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int x")
@RefinementAlias("IsZero(ArrayList t) {size(t) == 0}")
public interface Test2 {

@StateRefinement(to = "IsZero(this)")
public abstract void ArrayList();

@StateRefinement(from = "(IsZero(this))")
public abstract int get(int index);

}

class T1 {

public static void main(String[] args) {
ArrayList list = new ArrayList<>();
list.get(0);
}
}
```
This one fails, the only difference is the latter is declared as an interface and not an abstract class.

The error given is
-
```
______________________________________________________
Failed to check state transitions when calling list.get(0) in:

list.get(0)

Expected possible states:(IsZero(this))

State found:
----------------------------------------------------------------------------------------------------------------------------------
∀#list_6:ArrayList, (IsZero(#list_6)) && x(#list_6) == x(old(#list_6))
----------------------------------------------------------------------------------------------------------------------------------

Instance translation table:
----------------------------------------------------------------------------------------------------------------------------------
| Variable Name | Created in | File
----------------------------------------------------------------------------------------------------------------------------------
| #list_6 | java.util.ArrayList list = new java.util.ArrayList<>() | Test2.java:20, 22
----------------------------------------------------------------------------------------------------------------------------------
```

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.

Research direction

Start by running the two Java examples from the issue and compare refinement-alias handling for the abstract class and interface declarations. Trace the state-transition and interface processing paths to identify why the interface produces the shown state mismatch; done means the interface example verifies consistently with the abstract-class example.

Written by the indexing model from the issue text.

Assessment

Tech stack
java
Domain
compilers
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.