Abstract
Pipa is a behavioral interface specification language (BISL) tailored to AspectJ, an aspect-oriented programming language. Pipa is a simple and practical extension to the Java Modeling Language (JML), a BISL for Java. Pipa uses the same basic approach as JML to specify AspectJ classes and interfaces, and extends JML, with just a few new constructs, to specify AspectJ aspects. Pipa also supports aspect specification inheritance and crosscutting. This paper discusses the goals and overall approach of Pipa. It also provides several examples of Pipa specifications and discusses how to transform an AspectJ program together with its Pipa specification into a corresponding Java program and JML specification. The goal is to facilitate the use of existing JML-based tools to verify AspectJ programs.
| Original language | English |
|---|---|
| Pages (from-to) | 150-165 |
| Number of pages | 16 |
| Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Volume | 2621 |
| Publication status | Published - Dec 1 2003 |
| Externally published | Yes |
Fingerprint
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Computer Science(all)
Cite this
Pipa : A behavioral interface specification language for AspectJ. / Zhao, Jianjun; Rinard, Martin.
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 2621, 01.12.2003, p. 150-165.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Pipa
T2 - A behavioral interface specification language for AspectJ
AU - Zhao, Jianjun
AU - Rinard, Martin
PY - 2003/12/1
Y1 - 2003/12/1
N2 - Pipa is a behavioral interface specification language (BISL) tailored to AspectJ, an aspect-oriented programming language. Pipa is a simple and practical extension to the Java Modeling Language (JML), a BISL for Java. Pipa uses the same basic approach as JML to specify AspectJ classes and interfaces, and extends JML, with just a few new constructs, to specify AspectJ aspects. Pipa also supports aspect specification inheritance and crosscutting. This paper discusses the goals and overall approach of Pipa. It also provides several examples of Pipa specifications and discusses how to transform an AspectJ program together with its Pipa specification into a corresponding Java program and JML specification. The goal is to facilitate the use of existing JML-based tools to verify AspectJ programs.
AB - Pipa is a behavioral interface specification language (BISL) tailored to AspectJ, an aspect-oriented programming language. Pipa is a simple and practical extension to the Java Modeling Language (JML), a BISL for Java. Pipa uses the same basic approach as JML to specify AspectJ classes and interfaces, and extends JML, with just a few new constructs, to specify AspectJ aspects. Pipa also supports aspect specification inheritance and crosscutting. This paper discusses the goals and overall approach of Pipa. It also provides several examples of Pipa specifications and discusses how to transform an AspectJ program together with its Pipa specification into a corresponding Java program and JML specification. The goal is to facilitate the use of existing JML-based tools to verify AspectJ programs.
UR - http://www.scopus.com/inward/record.url?scp=33748329543&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33748329543&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:33748329543
VL - 2621
SP - 150
EP - 165
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
SN - 0302-9743
ER -