Presentations from Bergen University, Norway
by Magne Haveraaen, Adis Hodzic, Anya Helene Bagge, Karl Trygve Kalleberg
Moldable Programming
Swansea, June 30, 2005
Magne Haveraaen, Adis Hodzic, Anya Helene Bagge, Karl Trygve Kalleberg
There is a common understanding that current software is brittle:
it is difficult to develop, understand and modify.
Tools that help us work with software are still rudimentary, in spite
of the general ideas being known for decades.
What are the reasons for this?
The main reason is perhaps historical. Most major programming languages
and concepts were conceived before the central programming notions
were fully understood. This meets us everywhere, from arrays in C/C++
(being modelled on 1960's hardware implementation rather than being a
type) and a horrendous variation in parameter passing mechanisms
(motivated by efficiency concerns in the 1970's), to the mixup between
the notions of specification and implementation and the related
confusion between code reuse, typing disciplines and pointers in
object-oriented programming.
The way forward is then to reexamine our knowledge about programming,
and put all the notions we need together in such a way that we achieve
- a formal understanding of specification and programming concepts,
- a notation easy to analyse by tools and understand by humans,
- a specification and programming flexibility beyond the syntactic
confines we are locked in today,
and such that it all readily links up with the pragmatics of efficient,
well-behaved programs.
We will investigate our proposal for a new programming strategy in the
following steps:
1. Scrutinize the notion of an interface (signature) and see how this can
be made into a very precise, yet pragmatically extremely flexible,
vehicle for programming.
2. Provide a formal framework which clearly separates specifications
and programs, and then links programs as syntactic entities precisely
to semantics and resource usage (run-time and storage).
With this we bring together semantics and algorithmics.
3. Investigate tools which bring specifications and programs together
to aid program construction and reuse.
4. Propose notational concepts which makes all this manageable.
In summary:
From brittle programs to tough, moldable software.
Moldable signatures
Magne Haveraaen, University of Bergen, University of Wales Swansea
Interfaces (signatures) are one of the most fundamental concepts in
computer science.
- From a compiler/linker perspective, the interface contains all information
needed to match the call of a method to its body, thus being able to
separate method use from method implementation.
- From a software developer's viewpoint the interface is the place for
the contract between the user of a method and the implementor of the
method. The signature then becomes the means for introducing domain
specific concepts.
- From a theoretical (institution) perspective, signatures form an
index category for categories of specifications and for categories of
(possible) implementations / models, providing a framework for a link
between specification and implementation.
In this presentation we will investigate signatures from a pragmatic,
software engineering viewpoint.
Our first postulate is that the parameter passing modes that are
used in programming languages are of no help to programmers. They are
only historic artefacts, used to resolve semantic problems of
pathological cases of method (ab)use. Rather than exploring parameter
passing mechanisms we should rule out the pathological cases.
Our second postulate is that partiality is not about normal values and a
"value" called undefined, partiality is about not having to talk about
irrelevant cases. This perspective leads on to guarding as a natural
mechanism for specifications, and a varied bag of interchangeable
techniques (exceptions, preconditions, flags, etc.) for implementations.
Our third postulate is that we can relate a whole range of different
interface notations, such as functional / expression notation with a
single return value, procedural notation with possible multiple updatable
arguments, program notation with a list of files for input/output,
programs with user dialogues or on-screen data entry forms, such that
we freely may implement one and use another.
Our fourth postulate is that we should be able to move freely between
very strict typing disciplines (such as dependent types) and weak typing
disciplines (with explicit predicates to check the needed preconditions)
at no reimplementation cost.
We will sketch an attitude to signatures where all these postulates are
fulfilled, and show some of the benefits we achieve with this flexibility.
Using Programs as Institution Models
Adis Hodzic, University of Bergen
The concept of an institution provides a framework where signatures
index specification and (semantic) model categories. As such it is a
very valuable construct for understanding the relationship between
specification and meaning, and for investigating modular constructs.
However, important aspects of programming, such as run-time resource use,
memory requirements or syntactic complexity of program code falls outside
the model.
Here we sketch a framework for using syntactic programs as model category
in an institution. In this framework we can represent and study programs
as both syntactic and semantic entities.
Key concepts of programming such as data structures and algorithms,
and their resource requirements, become expressible in the same
framework as formal specification of the semantics of the algorithms.
Programming concepts, such as encapsulation and inheritance, can be
formally investigated in this context. It turns out that encapsulation
is fundamental in achieving the categorical properties we want of a
model class, reinforcing the modern view of the necessity of hiding the
internals of an implementation from its use.
With this notion of programs, we may also look at model class functors
as generic programming tools, allowing us, e.g., to see (functorial)
constructions on sets as program constructions. This opens up for taking
a wide range of well understood mathematical constructions as programs,
programs that have been verified by centuries of mathematics.
Weaves for Moldable Software
Karl Trygve Kalleberg, University of Bergen / Utrecht University
In the field of software engineering, we solve most non-trivial
problems by modeling them, then eventually expressing them in an executable
computer language. The stages of this development process are rarely
well connected, leading to discrepancies between the model and the
actual program. Most often, the program can not serve as the model,
since it contains large amounts of implementation complexity unrelated
to the original problem. While manipulation and analysis of the model may
be easy, similar activity on the program is practically never feasible.
In this talk, we discuss features of modern languages making
manipulation and analysis difficult, and sketch the weave, an extensible
notation supporting generation, analysis and manipulation of software,
as a piece in the puzzle of moldable software.
Program transformations for programming
Anya Helene Bagge, University of Bergen / Utrecht University
Program transformation is a tool for taking a program text and producing
a new program text, in a possibly different language. If the
transformation tool has sufficient expressive power, it will be able to
produce any kind of output for a given input. In this presentation we
are especially interested in program transformations as a support tool
for (domain-specific) programming.
In this respect program transformations can be seen as offering support
between that of using a standard compiler and the creation of a new
programming language with full compiler support. Here we will focus on
3 major issues related to extending programming languages with program
transformations.
1 The language specific aspect of the tool:
the tool must be able to analyse and manipulate the source programming
language in the same way as a compiler: parsing, program analysis,
basic transformations.
2 The tool giving methodological support:
the tool can enforce (safe) subsets of a language, provide alternate
typing disciplines, automatically insert and remove e.g. invariant
tests derived from formal specifications, and extend the language with
high level program constructs, e.g., moldable signatures, templates
and aspects.
3 Domain-related, user-configurable part of the tool:
the tool can be tailored to specific domains by user-defined notation
and transformation rules, e.g., in the form of algebraic specifications
of domain-specific libraries.
Our interest is on exploiting the relationship between specifications,
programs and program constructions to give us a powerful approach to
mold programs into form.