Refinement Aliases don't work with Interfaces
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
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.
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
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<Integer> list = new ArrayList<>();
list.get(0);
}
}
This example passes verification as intended, however
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<Integer> 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<java.lang.Integer> list = new java.util.ArrayList<>() | Test2.java:20, 22
----------------------------------------------------------------------------------------------------------------------------------
- Dominant language
- Java
- Stars
- 67
- Forks
- 36
- Avg merge
- 10d 18h
- Merged PRs (30d)
- 3
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.
More from liquid-java/liquidjava
-
enhancement
liquid-java/liquidjava#240 · 1 assignee ·
-
enhancement ide
Difficulty 3/5 1-2 days Newbie friendliness 45/100
liquid-java/liquidjava#206 ·
-
tests
Difficulty 2/5 1-3 hours Newbie friendliness 25/100
liquid-java/liquidjava#198 ·
-
tests
Difficulty 4/5 3-5 days Newbie friendliness 25/100
liquid-java/liquidjava#197 ·
-
tests
Difficulty 4/5 3-5 days Newbie friendliness 35/100
liquid-java/liquidjava#196 · 2 comments ·
All issues in liquid-java/liquidjava
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
elastic/gradle-plugins#157 ·
-
enhancement Tools
Difficulty 1/5 Under an hour Newbie friendliness 75/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
apache/rocketmq-dashboard#5008 ·
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
-
DETECT_PARAMETER_NAMES=false silently disables @ConstructorProperties-based Creator detection too Open
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
FasterXML/jackson-databind#6229 ·