Pipa: A behavioral interface specification language for AspectJ

Jianjun Zhao, Martin Rinard

Research output: Contribution to journalArticle

24 Citations (Scopus)

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 languageEnglish
Pages (from-to)150-165
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2621
Publication statusPublished - Dec 1 2003
Externally publishedYes

Fingerprint

Specification languages
Specification Languages
Java
Modeling Language
Specifications
Specification
Aspect oriented programming
Computer programming languages
Aspect-oriented Programming
Interfaces (computer)
Modeling languages
Programming Languages
Transform
Verify

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

@article{6c0882996c634c1d9ee3d6d051d69a70,
title = "Pipa: A behavioral interface specification language for AspectJ",
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.",
author = "Jianjun Zhao and Martin Rinard",
year = "2003",
month = "12",
day = "1",
language = "English",
volume = "2621",
pages = "150--165",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

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 -