Pipa is a behavioral interface specification language (BISL)tailored to AspectJ, an aspect-oriented programming language. Pipa isa simple and practical extension to the Java Modeling Language (JML),a BISL for Java. Pipa uses the same basic approach as JML to specifyAspectJ classes and interfaces, and extends JML, with just a few newconstructs, to specify AspectJ aspects. Pipa also supports aspect specificationinheritance and crosscutting. This paper discusses the goals andoverall approach of Pipa. It also provides several examples of Pipa specificationsand discusses how to transform an AspectJ program togetherwith its Pipa specification into a corresponding Java program and JMLspecification. The goal is to facilitate the use of existing JML-based toolsto verify AspectJ programs.