We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support
both concurrent reads and information hiding, we combine fractional permissions with abstract predicates. As an example, we
present a separation logic contract for iterators that prevents data races and concurrent modifications. Our program logic
is presented in an algorithmic style: we avoid structural rules for Hoare triples and formalize logical reasoning about typed
heaps by natural deduction rules and a set of sound axioms. We show that verified programs satisfy the following properties:
data race freedom, absence of null-dereferences and partial correctness.