Transcript A Survey on Java Meta Languages

A Survey on Java Modeling
Languages
Gergely Kovásznai,
Wolfgang Schreiner,
Gábor Kusper,
Gábor Guta,
János Sztrik,
Eszterházy Károly College
Johannes Kepler University
Eszterházy Károly College
Johannes Kepler University
University of Debrecen
Goal






A specification language is used to express the
concepts of the programmer on a high level
using pre-conditions and post-conditions,
also called contracts,
and invariants.
The surveyed meta languages have also tools which
can detect whether the Java implementation
breaks or not the high level description.
So we can see the clauses of the high level design as
syntactical or semantical constraints.
Goal
Motivation: Design Patterns &
OODesign Principles
Semantical constraint – Assertion
Syntactical constraint
outside Java
Syntactical constraint
inside Java
Previous work




Austro – Hungarian Joint Research Project:
Introducing Syntactical Constraints in ObjectOriented Programming Supporting Design Pattern
Principles
Wolfgang Schreiner: A JML Specification of the
Design Pattern "Proxy". RISC-Technical report, April
2009.
Gergely Kovasznai: Java Framework Implementing
Design Patterns by the Use of JML and
Contract4J. RISC-Technical report, 2009.
Wolfgang Schreiner: Supporting the Design Pattern
"Object Structures as Plain Values". RISCTechnical report, September 2009.
Java 1.4: Assert

Syntax:

assert Test ;
 where Test is a boolean expression. When the
system runs the assertion, it evaluates Test
and if it is false throws an AssertionError with
no detail message.

The second form of the assertion statement is:

assert Test : ErrorMessage ;
Java 1.4: Assert
Example:
public real division(int a, int b){
assert b!=0;
…
}
 We cannot divide by zero.
 We can test this in runtime by an assert.

Java 1.4: Assert
To enable assertions use the
-enableassertions, or -ea, switch.
 To disable assertions use the
-disableassertions, or -da, switch.
 java –ea HelloWorld

Goal
Motivation: Design Patterns &
OODesign Principles
Semantical constraint – Assertion
Syntactical constraint
outside Java
Syntactical constraint
inside Java
JML: “Java Modeling Language”
JML is a behavioral interface
specification language.
 In JML one can specify for each class

its interface, which consists of the names
and static information found in Java
declarations,
 its behavior, which tells how the module
acts when used.

JML Example
public class BankAccount {
//@ invariant 0<=balance
private short balance;
/*@ requires amount>=0;
ensures balance== \old(balance-amount)&&
\result==balance;
@*/
public int debit(int amount) {
...
}
}
JML as a Contract Language

Precondition:
requires <predicate>
 Postcondition:
ensures <predicate>
 Invariant:
invariant <predicate>
 A predicate may contain:




Java literals
method calls, field references
Java operators
\forall, \exists, \max, \min, \sum, \result, \old etc.
JML Example
public class IntMathOps {
/*@ public normal_behavior
@ requires y >= 0;
@ assignable \nothing;
@ ensures 0 <= \result
@ && \result * \result <= y
@ && ((0 <= (\result + 1) * (\result + 1))
@ ==> y < (\result + 1) * (\result + 1));
@*/
public static int isqrt(int y)
{
return (int) Math.sqrt(y);
}
}
JML Assert
Assert: Specifies a predicate that should
hold at some point in the code:
assert <predicate>
 Example:
for(n=0; n<a.length; n++)
if (a[n] == null) break;
//@ assert(\forall int i; 0<=i && i<n;
a[i]!=null);

JML Tools
ESC/Java2 does static analysis
 Iowa State’s JML release:

jml BankAccount.java
 jmlc BankAccount.java
jmlrac BankAccount
 jmldoc BankAccount.java

OpenJML
 JMLEclipse

More JML tools

http://www.eecs.ucf.edu/~leavens/JML/
Contract4J

Based on Aspect4J, Aspect Oriented
Programming
Contract4J






For each class and interface with a contract use:
@Contract
Precondition:
@Pre(<predicate>)
Postcondition:
@Post(<predicate>)
Invariant:
@Invar(<predicate>)
Predicate:




Java literals
method calls, field references
Java operators
$this, $return, $old, $args[n] etc.
Contract4J Example
@Contract
@Invar("$this.balance > = 0.0")
interface BankAccount {
@Post("$return >= 0.0")
float getBalance();
@Pre("amount >= 0.0")
@Post("$this.balance == $old($this.balance)+amount
&& $return == $this.balance")
float deposit(float amount);
}
Contract4J Tools

Contract4J for Eclipse
Goal
Motivation: Design Patterns &
OODesign Principles
Semantical constraint – Assertion
Syntactical constraint
outside Java
Syntactical constraint
inside Java
An OO Design Principle from GOF
Program to an interface,
not an implementation.
This means in practice the following:
A client of a class may know only the
interface of its abstract ancestor.
 ,i.e., if the class has more services the
client cannot call them, i.e., the ancestor
is should be closed.

Closed class in Contract4J
New constraint: closed class.
 Def: A child of a closed class may not
have public methods.

Closed class in Contract4J
@Invar("!Tool.hasPublicMethod($this.getClass())")
public abstract class
Decorator<R, A> implements IComponent<R, A> {...}
…
class Tool{
public static boolean hasPublicMethod(Class c){
Method[] ms = c.getDeclaredMethods();
for(Method m : ms){
int modifiers = m.getModifiers();
if (Modifier.isPublic(modifiers)) return true;
}
return false;
}
}
Goal
Motivation: Design Patterns &
OODesign Principles
Semantical constraint – Assertion
Syntactical constraint
outside Java
Syntactical constraint
inside Java
Other Java Meta Languages

Modern Jass, is a design by contract
tool that works with the latest versions of
Java and is closely related to JML.
Modern Jass
@Invariant - define an invariant.
 @Pre/@Post - Pre/Post-conditions
 @SpecCase - A full method specification
 @Also - A container for multiple
specifications
 @NonNull - A flyweight annotation to
state that a reference is not null

Modern Jass
1: package foo;
2: import jass.modern.*;
3: public class Bar {
4: @Pre("args.length % 2 == 0")
5: public static void main(String[] args){
6:
System.out.println("Hello,„ +
args.length);
7: } }
Modern Jass
Compiling / Validating contracts:
 javac -cp .:jass.modern.core20070519.jar foo/Bar.java
 Running:
 java -javaagent:jass.modern.core20070519.jar foo.Bar

Thank you for your attention!
The side of our joint project:
www.risc.uni-linz.ac.at/projects/syntactical