Ghost variables are not correctly initialized in interfaces

Aperta
#44 1 commento 0 reazioni 1 assegnatario Vedi su GitHub

@pcanelas ci sta già lavorando.

Dal 4/7/2025.

Valutazione

Questa issue non è ancora stata valutata.

Descrizione

bug enhancement

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

@ExternalRefinementsFor("java.util.List")
@Ghost("int size2")
public interface ListRefinements<E> {

	@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);
}

	public static void main(String[] args) {
		List<Integer> 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

Lingua principale
Java
Stelle
67
Fork
36
Merge medio
10g 18h
PR unite (30g)
3

Guida per i contributori

Apri la guida per i contributori

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di liquid-java/liquidjava

Tutte le issue di liquid-java/liquidjava

Issue simili

Altre issue su Java

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.