// $Id: Map.java,v 1.2 1999/11/05 19:21:30 leavens Exp $ package lib; public class Map implements Iterator { protected Function saved_proc; protected Iterator saved_seq; /*@ public invariant: saved_proc != null && saved_seq != null @*/ public Map(Function proc, Iterator seq) //@ requires: proc != null && seq != null; { saved_proc = proc; saved_seq = seq; } public boolean hasMore() { return saved_seq.hasMore(); } public void advance() { saved_seq.advance(); } public Object getElement() { return saved_proc.value(saved_seq.getElement()); } }