Transcript Objectifier - Wiki - Universidade do Minho

Objectification of Formal Specifications
António Miguel Cruz
([email protected])
1st PURe Workshop – 13,14 September 2004
Tel.: +351.22.6053360 ; Fax.: +351.22.6053361; E-Mail: [email protected] ; URL: http://www.sidereus.pt
sidereus
Rigorous Solutions for Software Systems
Company Profile
www.sidereus.pt
Company Profile
Univ. do Minho & INESC Braga startup company (1997)
Mixed solutions for different kinds of activities, supported by a strong technological knowhow in the following domains: Data Quality and Migration, Customer Relationship
Management (CRM), Business Intelligence (BI) and Knowledge Management (KM)
Scientific, tecnhological and industry know-how
Offer focused on Microsoft technology
Highly competitive quality/price ratios
Full client partnerhships covering analysis,
design, implementation and maintenance
phases
Software
Reuse (1995)
Data
Quality (2001)
Knowledge
Management (2005)
R&D activities with both national (Univ. do Minho, Fac. Eng. do Porto)
and international (AAlborg University Esbjerg, Dept of Computer
Science and Engineering - Dinamarca, Universidade de Bristol - U.K.)
universities and leadership of Portuguese participations in European
projects co-financed by the Portuguese Government and EU.
Fully engaged with projects associated with the initiative Portugal
Digital which includes, among others, all the cidades e regiões
digitais projects.
Rigorous Solutions for Software Systems
Company Profile
References
•
•
•
•
•
•
•
CRM
– ANIVEC – Associação Nacional das
Indústrias de Vestuário e Confecção
– LUSAMATEX – Máquinas Texteis
CRM Retail (works with PDA’s and GPRS
communications)
– EXCEDER/FIMA-UNILEVER
– EXCEDER/SOGRAPE
CRM, Reclamation Management, Process
Management and Document Management
– C. M. Maia (Maia Digital)
– C. M. Porto (Porto Digital)
Temporal Databases
– SONAE e OPTIMUS
CD-ROM da Rev. Constitucional
– Ed. Notícias e Microsoft
Healthcare Information Systems, Decision
Support Systems, Data Quality and Data
Migration
– Novabase
E-Learning and Knowledge Management
– AEP, GESTLUZ
sidereus
www.sidereus.pt
Rigorous Solutions for Software Systems
Company Profile
sidereus
www.sidereus.pt
Partnerships
•
Industry
–
E-Learning
•
•
•
Technology
–
Geo-referenciation and mobility
•
–
–
EuroTux Informática S.A.
Methods
•
–
Imediata - Sistemas Multimedia S.A.
System Administration
•
–
ParadigmaXis - Arquitectura e Engenharia de Software S.A.
Quiosques multimédia
•
Dept. Informatica, Univ. Minho, Formal Methods Group
Technologies
•
•
AEP - Associação Empresarial Portuguesa
GESTLUZ - Consultores de Gestão, Lda.
Microsoft (Portugal)
Research & Development
–
Methodologies and Prototyping
•
•
–
Departamento de Informática, Universidade do Minho
University of Bristol (UK) Computer Science Departement
Fuzzy Systems
•
Laboratory for Knowledge Technology, Department of Computer Science and
Engineering, AAlborg University Esbjerg (Denmark) Department of Computer Science
and Engineering
sidereus
Rigorous Solutions for Software Systems
Company Profile
Consortia
•
IKF (Eureka!2235)
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
NOMOS SISTEMA S.p.A. (Milano - Italy)
O.GROUP TECHNOLOGY S.p.A. (Milano - Italy)
ACSEs.r.l. (Milano - Italy)
ELSAG BANKLAB S.p.A. (Roma - Italy)
SELESTA AUDITING s.r.l. (Milano - Italy)
LADSEB-CNR (Padova - Italy)
UNIVERSITA' DI MILANO (Milano - Italy)
UNIVERSITA' DEL SANNIO (Benevento - Italy)
SIDEREUS - Sistemas de Informação e Consultoria
Informática S.A. (Porto - Portugal)
University of Minho (Portugal) Informatics
Departement
ParadigmaXis - Arquitectura e Engenharia de Software
S.A.
AEP - Associação Empresarial Portuguesa
GESTLUZ - Consultores de Gestão, Lda.
APPLAI Ltd (Altrincham - Cheshire UK)
XHP Consulting Ltd (Stroud - UK)
MATH-TECH Aps (Copenhagen - Denmark)
ARTEMA MEC A/S (Albertslund - Denmark)
ADAPTIVE COMPUTER SYSTEMS (Copenhagen Denmark)
ML CONSULTING AND COMPUTING Ltd (Budapest Hungary)
MORPHOLOGIC Ltd (Budapest - Hungary)
TECHNICAL UNIVERSITY OF BUDAPEST - Dept. of
Meas. and Inf. Systems (Budapest - Hungary)
BUDAPEST UNIVERSITY OF ECONOMIC SCIENCE Tech. Transfer Center (Budapest - Hungary)
POLITEHNICA UNIVERSITY OF BUCHAREST - ACPC
(Bucharest - Romania)
OLISOFTROM srl (Bucharest - Romania)
A&C INTERNATIONAL S.A. (Bucharest - Romania)
NATIONAL AGENCY FOR COMMUNICATION AND
INFORMATION (Bucharest - Romania)
www.sidereus.pt
•
ForTia (Formal Techniques Industrial
Association)
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
–
Adelard, London, UK
Alstom Transport, Saint Ouen, France
ATS, Chennai, India
ATX Software, Linda-a-Velha, Portugal
Banverket, Borlänge, Sweden
Chess, Haarlem, Netherlands
Clearsy, Aix-en-Provence, France
Escher Technologies, Aldershot, UK
Formal Systems, Oxford, UK
France Télécom, Lannion, France
IFAD, Odense, Denmark
Industrilogik L4i, Stockholm, Sweden
Institute of System Programming, Russian Academy of
Sciences, Moscow, Russia
INTECS, Pisa, Italy
JFITS, Tokyo, Japan
Kestrel Institute, Palo Alto, USA
Luxoft, Moscow, Russia
Maconomy, Copenhagen, Denmark
Niklas Holsti (new company to be announced), Espoo,
Finland
Nokia, Helsinki, Finland
ORA, Ottawa, Canada
OTE, Pisa, Italy
Praxis Critical Systems plc, Bath, UK
Qinetiq, Farnborough, UK
Railway Technical Research Institute, Tokyo, Japan
SIDEREUS, Porto, Portugal
Siemens Research, Munich, Germany
SRA, Tokyo, Japan
Systransis, Luzern, Switerland
Terma Space Division, Birkerød, Denmark
TriReme International Ltd., Stockport, UK
Trusted Logic, Sophia Antipolis, France
West Consulting, Delft, Netherlands
Rigorous Solutions for Software Systems
Company Profile
Products and Solutions
BackOffice CRM – Customer Relationship
Management
BackOffice SGR – Reclamation and
Suggestion Management
BackOffice RTL – CRM for Distribution and
Retail
BackOffice DOC – Document and Quality
Processes Management
BackOffice IKF – Knowledge Management
and E-Learning
sidereus
www.sidereus.pt
Objectification of Formal
Specifications
PURe Project
Program Understanding and Re-engineering – Calculi and Applications
António Miguel Cruz
[email protected]
PURe Workshop – 13, 14 September 2004
Universidade do Minho
Objectification of Formal
Specifications
• Introduction
• Related Work (reverse engineering / OO
reengineering)
• Example
• Objectification Criteria
• The Objectifier
• Conclusions and Future Work
Introduction
• Problems:
– Legacy code maintenance (aiding in
Knowledge recovery).
– Legacy code restructuring.
– OO Implementation of a purelly
functional specification.
Introduction
Introduction
ISO/IEC 13817-1
• Why VDM ?
– VDM-SL is a systematic method for
formal specification of software
systems (ISO standard since 1996).
– VDM++ is an object oriented
extension of VDM-SL.
– Both VDM-SL and VDM++ can be
“animated” using the IFAD VDM
Tools.
Related Work
• Methodology for converting conventional
code onto object oriented code
[GKM95,GK96,BG97,GW98].
Converts procedural code onto object oriented code
provided that the target programming language is an
extention of the original non-object-oriented language.
The transformation process takes place at source code
level and it reuses the original code introducing the
minimum alterations possible.
The work is based on an expert knowledge of the
system.
Related Work
• Methodology for reverse engineering
existing procedural code based on a
diagramatic representation of the original
system [CA93].
This methodology is based on the diagramatic
representation of the system using a reversed object
oriented analysis done by experts with knowledge
about the original system.
The diagrams are the basis for the formal specification
of the system.
Related Work
• Reverse engineering of C code, using
Formal Methods [GC93,GC96a,GC96b].
This methodology makes use of predicate logic for
creating an abstraction of the system based on its logic
properties.
The process was initially based on the weakest
precondition [GC93], but was then altered to work with
the strongest postcondition [GC96a].
In [GC93], a method for identifying objects within the
logic abstraction of the system, is also addressed.
Related Work
• Program Slicing [Ste99].
Program slicing is traditionally used for debugging.
It has the following variants:
• Static Slicing / Dynamic Slicing
• Forward Slicing / Backward Slicing
• Intraprocedural Slicing / Interprocedural Slicing
Related Work
• Program Slicing [Ste99].
Related Work
• Program Slicing [Ste99].
Related Work
• Program Slicing [Ste99].
Related Work
• Program Slicing [BBL93b].
Program slicing is also used for code restructuring
towards the object oriented paradigm.
It can be used to transform a program in a given
language to an object oriented version of the same
language, or it can be used to extract knowledge from
the original program.
Related Work
• Specification (using predicate logic) of a
compiler/decompiler between a pseudohigh level programming language and
assembly code of a simplified virtual
machine [Bow93].
• Reverse engineering of code with pointers
[GC97].
• Code compilation/decompilation and its
reverse engineering to the Z++ notation
[BB92a,BB92b,BBL93a,BBL93b,BL91].
Related Work
• Knowledge recovery from ER-diagrams
and SQL-DDL scripts to formal supports
(Sets and VDM-SL) [OC93,NSO99].
Methodology and tool for abstracting ER-diagrams to
the Sets notation.
Methodology and tool for reversing SQL-DDL scripts to
VDM-SL, and assisting in the application of abstraction
rules.
Example
Purelly functional specification of Folder
Elem
Stack
Folder
Example
Purelly functional specification of Folder
push
Elem
top
empty
Stack
isEmpty
pop
Boolean
Example
Purelly functional specification of Folder
retiraFolha
viraFolhaTras
novoFolder
leFolha
Elem
Folder
viraFolhaFrente
insereFolha
Example
Identification of Classes to create.
(Identifying the respectives states)
class_Stack
class_Folder
Example
Distribute types and functions definitions
over the created classes
Example
Infer methods from the existing functions
Example
Separate the algebraic purelly functional
core from the Object Oriented API
Objectification Phases
• Identify classes (states) to create.
• Distribute types over the classes.
• Distribute functions.
• Infer methods.
• Create the classes separating the
functional core from the OO API.
Objectification Criteria
One needs to define criteria to:
• Identify the types that are going to be
“promoted” to Class.
• Which types are defined within each class.
• Which functions are created within each class.
• How to create methods...
Objectification Criteria
Direct dependence relation:
• When a given data type t is defined in function of a
data type t’, i.e. when a functor F exists, such that
t = F(t’), is said that t directly depends from t’, or
that t’ participates in the construction of t, and such
fact is denoted by
Objectification Criteria
Other definitions:
• Sets Pt and Rt:
Objectification Criteria
Promotion criteria:
• promotableToClass(t) predicate:
Objectification Criteria
Criteria to assign datatypes to classes:
• Datatypes to be defined in the context of class Ct are:
Objectification Criteria
Criteria to assign functions to classes:
• Functions to be defined in the context of class Ct are:
Another example
Purelly functional specification of a
simplified integer expressions system
Expr
Term
Expr ◄ Term
Term ◄ Expr
Another example
Purelly functional specification of a
simplified integer expressions system
Var  Value
evalExpr
Value
Expr
compare
wellFormedExpr
Boolean
Purelly functional specification of a
simplified integer expressions system
Another example
Another example
Purelly functional specification of a
simplified integer expressions system
Var  Value
evalExpr
Value
Expr
compare
wellFormedExpr
*
f
Boolean
Another example
Purelly functional specification of a
simplified integer expressions system
Another example
Purelly functional specification of a
simplified integer expressions system
S-Alg
Class-Expr-Alg
Class-Expr-Obj
Function Combination
• Each resulting class API produced by the
objectification process can be enhanced
with operations that combine a state
updating function and a state reading
function.
• There are two modes of function
combination:
– Execute the function that reads the state
before the function that updates the state
(or the two functions in parallel).
– Execute the function that updates the
state before the function that reads the
state.
Function Combination
Ex.:
Function Combination
The Objectifier
Development status:
• VDM-SL running prototype.
• It takes a VDM-SL (abstract syntax)
expression of a functional specification
and produces a list of VDM++ (abstract
syntax) expressions of classes.
The Objectifier
VDM-SL
(AS)
Objectify
VDM++
(AS)
The Objectifier
VDM-SL
Definitions
Objectify
VDM++
Class+
The Objectifier
VDM-SL
Definitions
synthesize-vdmpp
eval-defs
Attributes
VDM++
Class+
The Objectifier
Classes
synAllClasses
attributes
VDM-SL
Definitions
finalClasses
VDM++
Class+
conjectureClasses
Type Functions
attributes
attributes
Attributes
ClassFunctions
The Objectifier - example
The Objectifier - example
[
Conclusions
• Existing objectification methods are
based on direct code restructuring.
• With a different approach, the method
presented here uses, as a base of work,
an algebraic purelly functional
specification.
Conclusions
• The objectifier works on the functional
specification, identifying classes
(concepts) that are close to the business
process served by the system in
question.
Conclusions
• Each class (concept) identified gives origin to
two VDM++ classes:
– A purelly functional algebraic class that
conserves the datatypes and the functions of the
original specification.
– A class that descends from the first one,
animating its “services” through the maintenance
of an internal state, and adding to it a methods
API for a OO usage.
Conclusions
• The objectification criteria used
guarantees that:
– There are no stateless classes (concepts,
seen as a pair of VDM++ classes, -Alg and –
Obj).
– A class has allways a means of updating its
state, or descends from one that has.
Future Work
• Further develope the prototype.
• Re-implement the Objectifier using Haskell,
SDF and Strafunski [vdBvDH+01,Vis03,LV03].
• Allow the use of modules (or even modules with
state) in the original VDM-SL specifications.
• Prototype a Deobjectifier.
References
References
References
Thank you!
Miguel Cruz [email protected]
Rigorous Solutions for
Software Systems
E-Mail: [email protected] ; URL: http://www.sidereus.pt