Automated Discovery Of Algebraic Specifications From Java Classes
Room: BBL room 471
Speaker: Ingmar van der Steen
Title: Automated discovery of algebraic specifications from Java classes
Developers can benefit from software-libraries to satisfy their needs on
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
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
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
specifications'. These specifications typically don't have low-level references
program's state variables. You can regard them as black-box specifications which
still hold even if the implementation is changed and e.g. other state variables
These algebraic specifications are extracted from Java classes by dynamically
method calls on instances of such a class. The resulting states are related to
using different forms of equivalence
equations are then generalized to produce axioms which are finally presented to
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.