liquid-java / liquid-java/liquidjava

Refinement Aliases don't work with Interfaces

Abierto
#50 2 comentarios 0 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

bug
Lenguaje dominante
Java
Estrellas
67
Forks
36
Merge medio
10 d 18 h
PR fusionados (30 d)
3

Descripción

`@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
----------------------------------------------------------------------------------------------------------------------------------
```

Guía de contribución

Abrir la guía de contribución

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Línea de trabajo

Comienza ejecutando los dos ejemplos de Java del issue y compara el manejo de refinement aliases para las declaraciones de la clase abstracta y de la interfaz. Sigue las rutas de transición de estados y de procesamiento de interfaces para identificar por qué la interfaz produce la discrepancia de estado mostrada; se considera terminado cuando el ejemplo de la interfaz se verifica de forma coherente con el ejemplo de la clase abstracta.

Escrito por el modelo de indexación a partir del texto del issue.

Evaluación

Stack tecnológico
java
Área
compilers
Tipo de issue
Error
Dificultad
4/5
Tiempo estimado
3-5 días
Estado de actividad
Estancado
Claridad
Bastante claro
Aptitud para principiantes
35/100

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.