liquid-java-external-libs/ArrayDequeRefinements.java at main · liquid-java/liquid-java-external-libs · GitHub

41 lines (30 loc) · 1.14 KB

package together1;

import repair.regen.specification.ExternalRefinementsFor;

import repair.regen.specification.Ghost;

import repair.regen.specification.Refinement;

import repair.regen.specification.StateRefinement;

/**

Refinements for the ArrayDeque class

Only modelling the size of the array deque

@ExternalRefinementsFor("java.util.ArrayDeque")

@Ghost("int size")

public interface ArrayDequeRefinements<E> {

public void ArrayDeque();

@StateRefinement(to="size(this) == (size(old(this)) + 1)")

public boolean add(E elem);

@StateRefinement(to="size(this) == (size(old(this)) + 1)")

public boolean offerFirst(E elem);

@StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))")

public E getFirst();

@StateRefinement(from="size(this) > 0", to = "size(this) == (size(old(this)))")

public E getLast();

@StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)")

public void remove();

@StateRefinement(from="size(this)> 0", to="size(this) == (size(old(this)) - 1)")

public E pop();

@Refinement("_ == size(this)")

public int size();

@Refinement("_ == (size(this) <= 0)")

public boolean isEmpty();

}

Expand file tree