archives

Lessons from the JML Project


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary T. and Clifton, Curtis (2005) Lessons from the JML Project. Technical Report 05-12, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

There is a later version of this eprint available: Click here to view it.

Abstract

To have impact, a grand challenge should provide a way for diverse research to be integrated in a synergistic fashion. Synergy in the JML project comes from a shared specification language, and thus holds several lessons for the verifying compiler grand challenge. An important lesson is that the project must focus considerable resources on specification language design, which still contains many open research problems. Another important lesson is the need to involve groups doing research on extensible compilers and integrated development environments.

Keywords:verifying compiler, specification, verification, formal methods, formal interface specification, extensible compilers, integrated development environments, JML language, Java language, Hoare
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Programming Environments
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
ID code:00000370
Deposited by:Gary T. Leavens on 05 May 2005
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR05-12/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR05-12/TR.ps.gz

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu