Transcript jml-akom

Java Modeling Language
Research Seminars on Software Reuse
Alan Kelon Oliveira de Moraes
<[email protected]>
Summary


Motivation
Design by ContractTM


Java Modeling Language



Some Approaches for DbC
JML Tools
Conclusions
References
2
Motivation
3
What is a component?

A software component is a unit of composition with
contractually specified interfaces and explicit context
dependencies only. A software component can be
independently deployed and is subject to third-party
composition [Szyperski, 2002]
4
[Jézéquel and Meyer, 1997] Design by
Contract: The Lessons of Ariane

On June 4, 1996, the maiden flight of the European
Ariane 5 launcher crashed, about 40 seconds after
takeoff.
$ 500 million software error
The exception was due to a floating point error during
a conversion from a 64-bit floating-point value,
representing the flight’s “horizontal bias,” to a 16-bit
signed integer
You can’t blame management, the language, the
design and the implementation
But you really have to blame reuse specification
Reuse without a precise, rigorous
specification mechanism is a risk of
potentially disastrous proportions.




5
[Alvaro et al., 2005] Software Component
Certification: A Survey

Software components certification is still immature
6
[Meyer, 1998] Providing Trusted Components
to the Industry

Test, test, and retest


The implicit motto of much of the industry, is expensive and
wasteful.
The Trusted Component Project1 proposes to apply a
mix of formal and informal approaches:






Design by contract
Formal validation
OO and reuse techniques
Global public scrutiny
Extensive testing
Metrics efforts
1: http://www.trusted-components.org/
7
What we need?
1.
2.
3.
Theory
Implementation
Tools
8
How to build/assure
reliable components?
9
Design by ContractTM

Software Quality key concerns [Meyer, 1997]:





Reliability: correctness and robustness
Modularity: extendibility and reusability
Compatibility, portability, easy of use, efficiency, timeliness,
economy, functionality
The key factor for reliability is Design by Contract.
Bolstad (2004) states: “DbC is a step on the road
toward quality software”
10
Design by ContractTM



View the relationship between a supplier and its clients
as a formal agreement, expressing each party’s rights
and obligations [Meyer, 1997]
The term Design by Contract first appeared in 1986
[Meyer, 1986] (republished as [Meyer, 1992]), but
formal verification dates back from 1969 [Hoare,
1969]
Brings the specification to source code and make it
explicit
11
Correctness property

Correctness is a relative notion
public void f(int y) {
x = y + 1;
}
?


A software is correct when it is in accordance with its
specification
So is reasonable to use the word consistent software
instead of correct software
[Hoare, 1969]
12
Precondition and Postcondition

Let A be some operation, a correctness formula is an
expression of the form
{P} A {Q}

Any execution of A, starting in a state where P holds,
will terminate in a state where Q holds
E.g.: {x >= 9} x = x+ 5 {x>= 13}
[Hoare, 1969]
13
Precondition and Postcondition
[Meyer, 1997]
14
Class invariants


There is also a need for expressing global properties of
the instances of a class, which must be preserved by
all routines
Invariant rule

An assertion I is a correct class invariant for a class C if and
only if it meets the following two conditions:


Every creation procedure of C, when applied to arguments
satisfying its precondition in a state where the attributes have
their default values, yields a state satisfying I.
Every exported routine of the class, when applied to arguments
and a state satisfying both I and the routine’s precondition, yields
a state satisfying I.
[Meyer, 1997]
15
Assertion


An assertion is an expression involving some entities
of the software, and stating a property that these
entities may satisfy at certain stages of software
execution
A runtime assertion violation is the manifestation of a
bug in the software


A precondition violation is a bug in the client
A postcondition is a bug in the supplier
[Meyer, 1997]
16
Non-redundancy principle


Under no circumstances shall the body of a routine
ever test for the routine’s precondition -> No defensive
programming
However Firesmith (1999) argues that defensive
programming is the right approach to software
development:




Decreases message coupling
Better supports encapsulation
Eliminates concurrency bugs
Eliminates redundant code by reusing precondition checking
code.
[Meyer, 1997]
17
Some Approaches for DbC
18
Eiffel

Eiffel language has a native language support for DbC



[Meyer, 1992a] Applying "Design by Contract“
[Meyer, 1992b] Eiffel: the language
[Meyer, 1997] Object-oriented software construction
19
[Warmer and Kleppe, 1999] The object constraint
language: precise modeling with UML.

OCL (Object Constraint Language) is a textual specification language to adorn UML
diagrams and make a UML model far more semantically precise, detailed and thus
productive (i.e., subject to automated processing leading to code).









Formal language with well-defined semantics based on set theory and first-order
predicate logic
Object-oriented functional language: constructors syntactically combined using functional
nesting and object-oriented navigation in expressions that take objects and/or object
collections as parameters and evaluates to an object and/or an object collection as return
value
Strongly typed language where all expression and sub-expression has a well-defined
type that can be an UML primitive data type, a UML model classifier or a collection of
these
Semantics of an expression defined by its type mapping
Declarative language that specifies what properties the software under construction must
satisfy, not how it shall satisfy them
Side effect free language that cannot alter model elements, but only specify relations
between them (some possibly new but not created by OCL expressions)
Pure specification language that cannot alone execute nor program models but only
describe them
Both a constraint and query language for UML models
There is mappings from OCL to JML [Hamie, 2002]
20
iContract



[Kramer, 1998] iContract - The Java(tm) Design by
Contract(tm) Tool.
Converts from special comments (@pre, @post,
@invariant) to assertion check code that is inserted
into the source-code.
OCL complaint


Supports universal and existential quantifiers in contract
expressions.
It seems to be a good project, but a dead one
21
jContractor




[Karaorman et al., 1999] jContractor: A Reflective Java
Library to Support Design by Contract.
Use of reflection to implement contract at runtime
Last release on 2003
Source code available at
http://jcontractor.sourceforge.net/
22
Contract4J



Uses Java 5 Annotations and/or a JavaBean-like
convention
Generates AspectJ code, however Balzer and
colleagues (2005) argues that aspects can’t implement
contracts…
Source code available at http://www.contract4j.org/
23
Java Modeling Language
24
[Leavens and Cheon, 2005] Design by
Contract with JML

JML is a formal behavioral interface specification
language for Java that contains the essential notations
used in DbC as a subset
25
[Leavens and Cheon, 2005] Design by
Contract with JML

JML uses Java’s notation in assertions that it is easier
for programmers to learn and less intimidating than
languages that use special purpose mathematical
notations.
26
[Leavens and Cheon, 2005] Design by
Contract with JML

In JML, specifications are simple annotation comments
[Leavens et al, 1999]



/*@ … @*/
//@
Unlike normal code comments, a formal specification
in JML is (usually) machine checkable, and so can help
with debugging.
27
JML Syntax [Leavens et al., 1998] [Leavens et
al, 1999] [Leavens and Cheon, 2005]

Precondition


Postcondition


\old(E)
Using private fields in specifications


\result
Previous expression value


/*@ invariant E @*/
Operation’s result


/*@ ensures E; @*/
Invariant


/*@ requires E; @*/
private /*@ spec_public @*/ Type property;
Fields not null

Private /*@ not_null @*/ Type property;
28
JML Syntax

Quantifiers

Iterating over all variables


Verifying if exist variables


(\forall T x; R(x); P(x))
(\exists T x; R(x); P(x))
Num of elements

\num_of
29
Special method annotations

Pure method:




/*@ pure *@/ ReturnType methodName()
A method is pure if it has no side-effects on the program’s
state
Only pure methods are allowed in assertions
Helper method



private /*@ helper @*/ ReturnType methodName()
However, in JML, constructors and methods declared with the
modifier helper are exempted from having to satisfy
invariants.
Such helper methods must be private
30
An Example
class Location {
/** The pathname of a file. */
private /*@ spec_public non_null @*/ String path;
/** Initializes this Location.
* @param fullpath the full pathname
* to the file.
*/
//@ requires fullpath != null;
//@ assignable path;
//@ ensures path.equals(fullpath);
public Location(String fullpath) {
path = fullpath;
}
31
An Example
/** Returns the associated file */
//@ ensures \result != null;
private File getFile() {
if (fileCache == null) {
fileCache = new File(path);
}
return fileCache;
}
32
An Example
/** Is the file readable? */
//@ ensures \result == getFile().canRead();
public /*@ pure @*/ boolean readable() {
return getFile().canRead();
}
/** Copies this location's file
* to the given location's file.
*/
/*@ requires loc != null;
@ ensures \result != null;
@ ensures \result.equals(modTime())
@ && loc.modTime().equals(modTime());
@*/
public Date copyTo(Location loc) throws IOException {… }
33
[Burdy et al., 2003] An overview of JML tools
and applications
JML Tools
34
[Cheon and Leavens, 2002] A Runtime Assertion
Checker for the Java Modeling Language (JML)

jmlc: JML Compiler, a.k.a. runtime assertion checker





“Compiles” the specification into a bytecode
It is slow
jmlrac runs programs compiled with jmlc
The most used tools
They don’t work with Java 5
35
[Flanagan et al., 2002] Extended static
checking for Java.




Extended Static Checking/Java (ESC/Java) developed
by Compaq
Helps a lot while programming
It is neither sound nor complete; that is, it neither
warns about all errors, nor does it warn only about
actual errors.
Eclipse plug-in didn’t work.
36
[Cheon and Leavens, 2002] A Simple and Practical
Approach to Unit Testing: The JML and JUnit Way




jmlunit is a simple and effective technique that
automates the generation of oracles for unit testing
classes from specifications
The developer must only provide the data
[Tan and Edwards, 2004] Experiences evaluating the
effectiveness of JML-JUnit testing
It doesn’t work with Java 5
37
[Raghavan, 2000] Design of a JML
documentation generator



jmldoc is a javadoc specification generator
It is very slow
They don’t work with Java 5
38
Conclusions



Design by Contract is a worth technique to assure
component quality
It is not easy to write postconditions
There are much research on JML, but it isn’t widely
accepted in industry:

“So far we haven't had much industrial use, primarily because
tool support isn't very good”
Gary T. Leavens


Some users: Java Smart Cards in Europe, Fulcrum
Microsystems, Apple's WebObjects frameworks, Kodak and
Compaq
Among the existing DbC tools for Java, JML is the most
suitable for use
39
References







Jézéquel, J. and Meyer, B. 1997. Design by Contract: The Lessons of Ariane.
Computer 30, 1 (Jan. 1997), 129-130.
Alvaro, A.; de Almeida, E.S.; de Lemos Meira, S.R., "Software Component
Certification: A Survey," Software Engineering and Advanced Applications, 2005.
31st EUROMICRO Conference on , vol., no.pp. 106- 113, 30-03 Aug. 2005
Meyer, B. 1992. Applying "Design by Contract". Computer 25, 10 (Oct. 1992), 4051.
Meyer, B. 1997. Object-oriented software construction (2nd ed.). Prentice-Hall,
Inc.
Balzer, S., Eugster, P. and Meyer, B. 2005. Can aspects implement contracts?. In
Proceedings of RISE Workshop (Rapid Integration of Software Engineering
techniques), Heraklion, Crete, Greece, September 2005, to appear as SpringerVerlag Lecture Notes in Computer Science, 2005.
Meyer, B., Mingins, C., and Schmidt, H. 1998. Providing Trusted Components to
the Industry. Computer 31, 5 (May. 1998), 104-105.
Kramer, R. 1998. iContract - The Java(tm) Design by Contract(tm) Tool. In
Proceedings of the Technology of Object-Oriented Languages and Systems
(August 03 - 07, 1998). TOOLS. IEEE Computer Society, Washington, DC, 295.
40
References





Karaorman, M., Hölzle, U., and Bruno, J. L. 1999. jContractor: A
Reflective Java Library to Support Design by Contract. In Proceedings of
the Second international Conference on Meta-Level Architectures and
Reflection (July 19 - 21, 1999). P. Cointe, Ed. Lecture Notes In Computer
Science, vol. 1616. Springer-Verlag, London, 175-196.
Leavens, G. T. and Cheon, Y. Design by Contract with JML, available at
ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmldbc.pdf
Firesmith, D. G. 1999. A Comparison of Defensive Development and
Design by Contract. In Proceedings of the Technology of Object-Oriented
Languages and Systems (August 01 - 05, 1999). TOOLS. IEEE Computer
Society, Washington, DC, 258.
G. T. Leavens, A. L. Baker, and C. Ruby. JML: A notation for detailed
design. In H. Kilov, B. Rumpe, and I. Simmonds, editors, Behavioral
Specifications of Businesses and Systems, pages 175-188. Kluwer
Academic Publishers, Boston, 1999.
Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary Design of
JML: A Behavioral Interface Specification Language for Java. Department
of Computer Science, Iowa State University, TR #98-06-rev28, June
1998
41
References




Meyer, B. 1992 Eiffel: the language. Prentice-Hall, Inc.
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan,
K., Leino, M. and Poll, E., An overview of JML tools and applications.
Workshop on Formal Methods for Industrial Critical Systems (FMICS),
2003.
Yoonsik Cheon and Gary T. Leavens. A Runtime Assertion Checker for the
Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun
(eds.), International Conference on Software Engineering Research and
Practice (SERP '02), Las Vegas, Nevada. CSREA Press, June 2002, pages
322-328.
Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to
Unit Testing: The JML and JUnit Way. In Boris Magnusson (ed.), ECOOP
2002 -- Object-Oriented Programming, 16th European Conference,
Malaga, Spain, June 2002, Proceedings. Volume 2374 of Lecture Notes in
Computer Science, Springer Verlag, 2002, pages 231-255.
42
References








Arun D. Raghavan. Design of a JML documentation generator. Technical Report 0012, Iowa State University, Department of Computer Science, July 2000.
Bolstad, M., "Design by contract: a simple technique for improving the quality of
software," Users Group Conference, 2004. Proceedings , vol., no.pp. 303- 307, 711 June 2004
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B.
Saxe, and Raymie Stata. Extended static checking for Java. In Proceedings of the
2002 ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI), volume 37(5) of SIGPLAN Notices, pages 234-245. ACM,
May 2002.
Ali Hamie. Towards Verifying Java Realizations of OCL-Constrained Design Models
Using JML. In 6th IASTED International Conference on Software Engineering and
Applications, MIT, Cambridge, USA, 2002.
Warmer, J. and Kleppe, A. 1999 The object constraint language: precise modeling
with UML. Addison-Wesley Longman Publishing Co., Inc.
Meyer, B. 1986. Design by Contract, Technical Report TR-EI-12/CO, Interactive
Software Engineering Inc.
Hoare, C. A. 1969. An axiomatic basis for computer programming. Commun. ACM
12, 10 (Oct. 1969), 576-580.
Szyperski, C. 2002 Component Software: Beyond Object-Oriented Programming.
2nd. Addison-Wesley Longman Publishing Co., Inc.
43