Automated Discovery Of Algebraic Specifications From Java Classes
Stc
Date: 2009-05-14
Time: 11:00
Room: BBL room 471
Speaker: Ingmar van der Steen
Title: Automated discovery of algebraic specifications from Java classes
Abstract
Developers can benefit from software-libraries to satisfy their needs on
functionality.
In their programs they can make calls to well-defined interfaces of this library
and don't have to care
about how some particular functionality is implemented. This black-box view on
software development
has payed off for the last decades. If we are adopting this view, it's vital
that we have a
good understanding about the behaviour of these libraries. The sometimes poorly
documented
descriptions generated using e.g. the Javadoc tool, should actually only be read
when we also have a formal description of it.
The type of formal descriptions we are going to cover are the so called
'algebraic
specifications'. These specifications typically don't have low-level references
to
program's state variables. You can regard them as black-box specifications which
could
still hold even if the implementation is changed and e.g. other state variables
are used.
These algebraic specifications are extracted from Java classes by dynamically
generating
method calls on instances of such a class. The resulting states are related to
each other
using different forms of equivalence
(observational,representational,referential). The
equations are then generalized to produce axioms which are finally presented to
the user
of the discovery-tool.
I will discuss the pipeline of such a tool and talk about the problems which are
introduced using a dynamic approach.
