Skip to content

arraylist.md

Latest commit

 

History

History
35 lines (27 loc) · 1012 Bytes

arraylist.md

File metadata and controls

35 lines (27 loc) · 1012 Bytes
Raw
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.

import liquidjava.specification.*;

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

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

    public E get(@Refinement("0 <= _ && _ < size()") int index);
}
ArrayList<String> list = new ArrayList<>();
list.add("apple");
list.get(0);
list.get(1); // Refinement Error

The key idea is that LiquidJava turns the usual runtime condition for get(i) into a static precondition over the tracked size ghost variable.