Desugaring JML Method Specifications
Desugaring JML Method Specifications
File
Date
2005-05-01
Authors
Raghavan, Arun
Leavens, Gary
Leavens, Gary
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Department
Computer Science
Abstract
JML, which stands for ``Java Modeling Language,'' is a behavioral interface specification language (BISL) designed to specify Java modules. JML features a great deal of syntactic sugar that is designed to make method specifications more expressive. This paper presents a desugaring process that boils down all of the syntactic sugars in JML method specifications into a much simpler form. This desugaring will help one understand the meaning of these sugars, for example for use in program verification. It may also help manipulation of JML method specifications by tools.
Comments
Copyright © 2000, 2001, 2003, 2005 by Iowa State University