liquid-java / liquid-java/liquidjava
Refinement Aliases don't work with Interfaces
Personne n'a encore pris cette issue.
- Langage dominant
- Java
- Étoiles
- 67
- Forks
- 36
- Merge moyen
- 10 j 18 h
- PR mergées (30 j)
- 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
----------------------------------------------------------------------------------------------------------------------------------
```
Guide de contribution
Ouvrir le guide de contribution
Par où commencer
- Lisez l'issue en entier, puis le guide de contribution du projet.
- Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
- Forkez le dépôt et travaillez sur une branche.
- Ouvrez une pull request qui référence le numéro de l'issue.
Piste de recherche
Commencez par exécuter les deux exemples Java de l’issue et comparez la gestion des refinement aliases pour les déclarations de la classe abstraite et de l’interface. Suivez les chemins de transition d’état et de traitement des interfaces afin d’identifier pourquoi l’interface produit l’incohérence d’état présentée ; le travail est terminé lorsque l’exemple d’interface se vérifie de manière cohérente avec l’exemple de classe abstraite.
Rédigé par le modèle d'indexation à partir du texte de l'issue.
Évaluation
- Stack technique
- java
- Domaine
- compilers
- Type d'issue
- Bug
- Difficulté
- 4/5
- Temps estimé
- 3-5 jours
- Activité
- À l'abandon
- Clarté
- Plutôt claire
- Accessibilité débutants
- 35/100