Translation of a Subset of RSL into Java

(1)

Translation of a Subset of RSL into Java

Ulrik Hjarnaa Supervisors:

Anne Elisabeth Haxthausen (DTU)

Hans Bruun (DTU)

Computer Science and Engineering Informatics and Mathematical Modelling

Technical University of Denmark

Translation of a Subset of RSL into Java – p.1/35

(2)

Agenda

◆ Introduction & objectives

◆ Translation of RSL into Java

n Discussion of specific constructs

n Discussion of generel issues

◆ Process of developing a translator

n Design of a translator

n Development process

n Implementation & test

◆ Conclusion

(3)

Agenda

◆ Introduction & objectives

n Design of a translator

◆ Conclusion

(4)

Introduction

◆ There exists a number of formal methods for designing and specifying software

◆ There exists a number of programming languages for implementing software

◆ Typically a step of a formal method for software development is implementing a specification in the accompanying notation in a programming language

◆ Parts of a speficication language is implemented in the same way in a programming language

◆ This work focusses on:

n The specification language RSL which is part of RAISE

n The programming language Java

(5)

Introduction

(6)

Introduction

(7)

Introduction

(8)

Introduction

(9)

Introduction

(10)

Introduction

(11)

Objectives

Objectives:

◆ Define a translation of subset of RSL into Java

◆ Develop a tool for translating a subset of RSL into Java, (translator)

Requirements of translation:

◆ The translation from RSL into Java must be semantically equivalent to the specification in RSL

◆ In the Java translated from the specification it should be possible to recognize the specification

Requirements of translator:

◆ The translator must translate a subset of RSL into Java according to the translation defined

◆ The translator must provide extensibility

(12)

Objectives

Objectives:

(13)

Objectives

Objectives:

(14)

Objectives

Objectives:

(15)

Objectives

Objectives:

(16)

Objectives

Objectives:

(17)

Objectives

Objectives:

(18)

Objectives

Objectives:

(19)

Objectives

Objectives:

(20)

Agenda

◆ Introduction

◆ Translation of RSL into Java

n Design of translator

◆ Conclusion

(21)

Translation of RSL into Java

◆ Translation of types & type definitions

◆ Translation of value expressions & value definitions Types & type definitions:

◆ Translation of built–in types

◆ Translation of complex types

◆ Translation of type definitions

(22)

Translation of RSL into Java

◆ Translation of types & type definitions

◆ Translation of value expressions & value definitions Types & type definitions:

◆ Translation of built–in types

◆ Translation of complex types

◆ Translation of type definitions

(23)

Built–in types

◆ The built–in types are: Bool, Nat, Int, Real, Char, Text

◆ These built–in types must be represented in some way in Java

◆ Two possibilities were considered:

n Primitive types and library classes in Java

n A collection of classes implemented RSL Java

Bool ^boolean or ^Boolean Int ^int or ^Integer

Nat No translation.

Real ^double or ^Double Char ^char or Character

Text ^String

(24)

Built–in types

Text ^String

(25)

Built–in types

Text ^String

(26)

Built–in types

Bool ^boolean or ^Boolean Int int or ^Integer

Real double or ^Double Char ^char or ^Character

Text ^String

(27)

Built–in types

Text ^String

(28)

Built–in types

Text ^String

(29)

Complex types

◆ The complex types considered here are: list, set, and map

◆ These types may in RSL be of infinite size and non–deterministic

◆ In Java there exists a number of interfaces and classes for representing: Lists, sets and maps

◆ To represent the RSL lists, sets, maps in Java a number of interfaces and classes has been implemented

RSL Java

t^? RSLListDefault<T>, where ^T is the translation of ^t t-set RSLSetDefault<T>, where ^T is the translation of ^t.

t¹ ^→^m t² RSLMapDefault<T1 , T2>, where T¹ is the translation of t¹ and T² is the translation of t².

(30)

Complex types

RSL Java

(31)

Complex types

RSL Java

(32)

Complex types

RSL Java

(33)

Complex types

RSL Java

(34)

Type definition

◆ Type definitions in RSL is a way to create new types either abstract or based on existing or other defined types

◆ In Java there is only one way to create new types and that is through classes and interfaces

◆ Therefore translation of type definitions in RSL involve creation of one or more classes in Java

(35)

Type definition

(36)

Type definition

(37)

Variant definitions

RSL:

type t¹ == a¹ | . . .| aⁿ Java:

public abstract class T1 {

public abstract boolean equals ( Object o ) ; public abstract S t r i n g t o S t r i n g ( ) ;

}

public class A1 extends T1 { . . . } ...

public class Aⁿ extends T1 { . . . }

(38)

Variant definitions, constant

RSL:

type t == a Java:

public class A extends T {

public boolean equals ( Object o ) { i f ( o instanceof A)

return true ; else

return false ; }

public S t r i n g t o S t r i n g ( ) { return "A" ;

} }

(39)

Variant definitions, record constructor, RSL

RSL:

type t = a(t²)

(40)

Variant definitions, record constructor, Java

public class A extends T { public T2 _v1 ;

public A ( T2 _v1 ) { this . _v1 = _v1 ; }

public boolean equals ( Object o ) { i f ( o instanceof A) {

i f ( ! _v1 . equals ( ( ( T²) o ) . _v1 ) ) { return false ;

}

return true ; }

public S t r i n g t o S t r i n g ( ) { return "A( " + _v1 + " ) " ; } }

(41)

Variant definitions, destructors and reconstructors

RSL:

type t¹ == a(get_t : t² ↔ replace_t), Java:

public class A extends T1 { private T² _v1 ;

public A( T2 _v1 ) { this . _v1 = _v1 ; }

public T² g e t _ t ( ) { return _v1 ;

}

public T¹ r e p l a c e _ t ( T² _n1 ) { return new A( _n1 ) ;

} }

(42)

Example of variant definition, RSL

typeCollection == empty | add(Elem, Collection), Elem

(43)

Example of variant definition, Java 1

public abstract class C o l l e c t i o n { public abstract S t r i n g t o S t r i n g ( ) ;

public abstract boolean equals ( Object o ) ; }

public class empty extends C o l l e c t i o n { public boolean equals ( Object o ) {

i f ( o instanceof empty ) return true ;

else

return false ; } ;

public S t r i n g t o S t r i n g ( ) { return " empty " ;

}

} Translation of a Subset of RSL into Java – p.17/35

(44)

Example of variant definition, Java 2

public class add extends C o l l e c t i o n { private Elem _v1 ;

private C o l l e c t i o n _v2 ;

public add ( Elem _v1 , C o l l e c t i o n _v2 ) { this . _v1 = _v1 ;

this . _v2 = _v2 ; }

(45)

Example of variant definition, Java 3

public boolean equals ( Object o ) { i f ( o instanceof empty ) {

i f ( ! ( this . _v1 . equals ( ( ( add ) o ) . _v1 ) ) ) { return false ;

}

i f ( ! ( this . _v2 . equals ( ( ( add ) o ) . _v1 ) ) ) { return false ;

}

return true ; }

/∗ t o S t r i n g method omitted ∗/ }

public class Elem { }

(46)

Translation of value definitions and value expressions

◆ RSL have value expressions, Java have expressions, statements, and blocks

◆ In Java blocks consist of a collection of statements

◆ In Java there is one statement, an expression statement, which wraps an expression as a statement

◆ If a block is needed but the translation of an RSL value expression is a Java expression. The Java expression can be wrapped in an expression statement which again can be wrapped in a block

◆ If an expression is needed but the translation of an RSL value expression is a Java statement. The translation of the RSL value expression is to put the Java statement into an auxiliary method and then insert an application expression of the auxiliary method in the translation

(47)

Translation of value definitions and value expressions

(48)

Translation of value definitions and value expressions

(49)

Translation of value definitions and value expressions

(50)

Translation of value definitions and value expressions

(51)

Explicit function definition

An explicit function definition has the form:

single_typing formal_function_application ^≡

value_expression ^[pre_condition^] Limitations:

◆ Only id applications are considered

◆ Pre conditions disallowed

◆ Product type expression are not allowed in the result description RSL:

id : type_expr¹ ^× . . . ^× type_exprⁿ ^→ type_exprⁿ⁺¹ id(binding¹,. . . ,bindingⁿ) ≡ value_expr

Java:

public [ s t a t i c ] Tⁿ+1 Id ( T1 b1 ,. . . ,Tⁿ bⁿ ) V

(52)

if–then–else expression

RSL:

if a then elseb

endc Java:

i f (A) { B

}

else { C }

(53)

Example of an explicit function definition, RSL

listSum : Int^∗ ^→ Int listSum(il) ^≡

if il = hi then else0

hd il ⁺ listSum(tl il) end

(54)

Example of an explicit function definition, Java

public s t a t i c i n t listSum ( RSLList < Integer > i l ) { i n t _v0 = 0 ;

i f ( i l . equals (new RSLListDefault < Integer > ( ) ) ) { i n t _v1 = 0 ;

_v1 = 0 ; _v0 = _v1 }

else {

i n t _v1 = 0 ;

_v1 = i l . hd ( ) + listSum ( i l . t l ( ) ) ; _v0 = _v1

}

return _v0 ; }

(55)

Agenda

◆ Introduction

◆ Process of developing a translator

n Design of Translator

n Implementation & Test

◆ Conclusion

(56)

Developing a translator

◆ Complex task

◆ Decomposed into:

n Parsing the source language into a data structure which can be used in a program, a translator.

n Do the actual translation by creating a new data structure

n Unparsing the new data structure into the target language Modules:

◆ Front End

◆ Translation Module

◆ Back End

◆ Control Module

(57)

Developing a translator

◆ Complex task

◆ Decomposed into:

n Parsing the source language into a data structure which can be used in a program, a translator.

n Do the actual translation by creating a new data structure

n Unparsing the new data structure into the target language Modules:

◆ Front End

◆ Translation Module

◆ Back End

◆ Control Module

(58)

Front End

◆ Tool vs. not tool

◆ Developing a lexer and parser from scratch represent a complex task in itself

◆ A number of tools considered: Gentle, Lex & Yacc, SableCC, Javacc, and ANTLR

◆ ANTLR was chosen

(59)

Translation Module

The task of the translation module consist of two parts:

◆ Decorating the tree received from the front end

◆ Creating a new tree from the tree received The two task solved using two strategies:

◆ Decorating the tree is done using that the tree implements the visitor design pattern

◆ Creating the tree is done using a bootstrapping process.

Bootstrapping:

◆ Allows for incremental development

◆ Allows for expressing the module in RSL

(60)

Translation Module

Bootstrapping:

(61)

Translation Module

Bootstrapping:

(62)

Back End & Control Module

◆ The Back End is implemented using the visitor design pattern

◆ The Control Module is a module binding the other modules together

(63)

Modular design

Overview

BasicClass

Class LISTSUM.rsl

RSLParser RSLLexer

RSLAST

LISTSUM SchemeDef

Translator

JavaAST

LISTSUM

CompilationUnit

StringJavaVisitor LISTSUM.java

(64)

Bootstrapping

Bootstrapping step 1

(65)

Bootstrapping

Front End

RSL₀ RSLAST₀

Java

(66)

Bootstrapping

Translation Module

RSLAST₀ JavaAST

Java

(67)

Bootstrapping

Back End

JavaAST Java

Java

(68)

Bootstrapping

Combining the three parts

P RSL₀

P RSLAST₀

P JavaAST

P RSL₀ RSLAST₀ Java

Java

RSLAST₀ JavaAST

Java

JavaAST Java

Java

(69)

Bootstrapping

Result, the first version of the translator

RSL₀ Java

Java

(70)

Bootstrapping

Bootstrapping step 2

(71)

Bootstrapping

New development in step 2

RSLAST₁ JavaAST

RSL₀

(72)

Bootstrapping

Translating the new translation module

RSL₀ Java

Java RSLAST₁ JavaAST

RSL₀

RSLAST₁ JavaAST

Java

(73)

Bootstrapping

Combining the new translation module with the other parts

P RSL₁

P RSLAST₁

P JavaAST

P RSL₁ RSLAST₁ Java

Java

RSLAST₁ JavaAST

Java

JavaAST Java

Java

(74)

Bootstrapping

Result, the second version of the translator

RSL₁ Java

Java

(75)

Implementation & Test

Translator implemented in a number of packages:

◆ translator

◆ translator.javaast

◆ translator.lib

◆ translator.rslast

◆ translator.rsllib

◆ translator.syntacticanalyzer Testing:

◆ Using different strategies for the different modules

◆ The fact that the translated module is able to translate it self is a good indicator that it works

(76)

Agenda

◆ Introduction

n Design of Translator

n Implementation & Test

◆ Conclusion

(77)

Conclusion

The objectives were:

◆ To define a translation of a subset of RSL into Java

◆ To develop a tool, translator, for translating from RSL into Java according to a subset of the defined translation

Requirements of the translation:

◆ The translation into Java must be semantically equivalent to the specification in RSL

◆ In the Java translated from a specification it should be possible to recognize the specification

Requirements of the translator:

◆ The translator should translate a subset of RSL into Java according to the translation defined

◆ The translator should provide extensibility

(78)

Conclusion

(79)

Conclusion

(80)

Conclusion, Using the tool for creating new tools

New development

RSLAST RSLAST

RSL

(81)

Conclusion, Using the tool for creating new tools

Tranlation using existing translator

RSL Java

Java

RSLAST RSLAST

RSL

RSLAST RSLAST

Java

Tool developed

Translator

Executable Tool

(82)

Conclusion, Using the tool for creating new tools

Combining existing parts and the translated part

RSL RSLAST

Java

RSLAST RSLAST

Java

RSLAST RSL

Java RSL Visitor Tool developed

Front end