---
title: ArrayList
parent: Examples
nav_order: 8
permalink: /examples/arraylist/
description: An external refinement for ArrayList that prevents out-of-bounds access.
---

# ArrayList

This example refines the `java.util.ArrayList` standard-library class without modifying its source code. A ghost variable tracks the size of the list, and a parameter refinement prevents out-of-bounds accesses.

```java
import liquidjava.specification.*;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int size")
public interface ArrayListRefinements {
    public void ArrayList();

    @StateRefinement(to="size() == size(old(this)) + 1")
    public boolean add(E elem);

    public E get(@Refinement("0