FilesExpand file tree

 main

/

ArrayDequeRefinements.java

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

41 lines (30 loc) · 1.14 KB

 main

/

ArrayDequeRefinements.java

Top

File metadata and controls

• Code
• Blame

41 lines (30 loc) · 1.14 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

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();

}