Catálogo de publicaciones - libros

In these lecture notes we present a novel toolkit to program web applications that have dynamic, complex behavior based on interconnect forms. This toolkit is the iDataToolkit. We demonstrate that it allows programmers to create web applications on a level of abstraction that is comparable with ‘ordinary’ functional style programs. By this we mean that programmers can develop data structures and functions in the usual way. From the data structures the iDataToolkit is able to generate forms that can be used in a web application. It does this by making use of advanced programming concepts such as generic programming. The programmer need not be aware of this.

Although computer systems penetrate all facets of society, the software running those systems may contain many errors. Producing high quality software appears to be difficult and very expensive. Even determining the quality of software is not easy. Testing is by far the most used way to estimate the quality of software. Testing itself is not easy and time consuming.

In order to reduce the costs and increase the quality and speed of testing, testing should be automated itself. An automatical specification based test tool generates test data, executes the associated tests, and makes a fully automatically verdict based on a formal specification. Advantages of this approach are that one specifies properties instead of instances of these properties, test data are derived automatically instead of manually, the tests performed are always up to date with the current specification, and automatic testing is fast and accurate.

We will show that functions in a functional programming language can be used very well to model properties. One branch of the automatic test system handles logical properties relating function arguments and results of a single function call. The other branch of handles specifications of systems with an internal state.

These notes present an introduction into array-based programming from a functional, i.e., side-effect-free perspective.

The first part focuses on promoting arrays as predominant, stateless data structure. This leads to a programming style that favors compositions of generic array operations that manipulate entire arrays over specifications that are made in an element-wise fashion. An algebraicly consistent set of such operations is defined and several examples are given demonstrating the expressiveness of the proposed set of operations.

The second part shows how such a set of array operations can be defined within the first-order functional array language . It does not only discuss the language design issues involved but it also tackles implementation issues that are crucial for achieving acceptable runtimes from such genericly specified array operations.

This chapter describes Hume: a functionally-based language for programming with bounded resource usage, including time and space properties. The purpose of the Hume language design is to explore the expressibility/costability spectrum in resource-constrained systems, such as real-time embedded or control systems. It is unusual in being based on a combination of -calculus and finite state machine notions, rather than the more usual propositional logic, or flat finite-state-machine models. The use of a strict, purely functional programming notation allows the construction of a strong cost model for expressions, which can then be embedded into a simple cost model for processes.

In this chapter, we introduce Hume, describe the Hume Abstract Machine implementation, and show how a high-level cost model can be constructed that relates costs from the abstract machine to Hume source programs. We illustrate our approach with an example adapted from the literature: a simple vending machine controller.

We propose a novel, comonadic approach to dataflow (stream-based) computation. This is based on the observation that both general and causal stream functions can be characterized as coKleisli arrows of comonads and on the intuition that comonads in general must be a good means to structure context-dependent computation. In particular, we develop a generic comonadic interpreter of languages for context-dependent computation and instantiate it for stream-based computation. We also discuss distributive laws of a comonad over a monad as a means to structure combinations of effectful and context-dependent computation. We apply the latter to analyse clocked dataflow (partial stream based) computation.

In a pure functional language a series of values computed from one another can be considered as different states of the same “abstract object”. For this abstract object temporal properties (e.g. invariants) can be formulated and proved. This paper explains how to define and prove certain kinds of temporal properties of programs written in the pure functional language Clean. Sparkle, a theorem prover designed for Clean, is applied as a tool. Since Sparkle is not capable of handling temporal logical properties, its original version has been extended to support object abstraction, certain temporal properties and a new form of theorems which includes hypotheses. The resulting system is called Sparkle-T. The examples presented in this paper illustrate how object abstraction and the definition and proof of temporal properties can be carried out in Sparkle-T. Furthermore, some novel features of the Sparkle-T system are demonstrated as well.

When developing safety critical applications, the programmer might want to be able to his or her code correct. The integration of a proof system and a programming language of industrial strength can be fairly useful in this respect, like in the case of, for instance, the B method [1], the Java Modelling Language [5] or the functional programming languages Erlang [3,7,9,24] and Clean [11,23,25]. This paper presents the concept of subtype marks, a concept that establishes still closer links between a programming language and a proof system by letting the programmer encode certain important properties of programs within the type system of the language. Subtype marks are introduced here as part of a simple functional language. This language can be regarded as a small subset of Clean.

Functional programming has inherent parallel features. This situation can be exploited by building different language constructs for parallel and distributed programming. Earlier we designed two languages for skeleton based distributed functional programming on a cluster. The two languages have different expressive power and abstraction levels. Our distributed functional computation is based on a multiparadigm-oriented environment with several different layers. On the highest level D-Clean coordination language primitives are applied in order to define the distribution of the pure functional computation subtasks over a PC cluster. This distribution is made according to a predefined computational scheme, which is an algorithmic skeleton, parameterized by functions, types and data. The D-Clean programs are transformed into D-Box, a lower level description language including the computational nodes implemented in the lazy functional language Clean. The computational nodes are distributed over the cluster and they communicate using the middleware services. This paper presents skeleton based functional and distributed programming using the D-Clean and D-Box languages. The main goal is to illustrate the appropriateness and applicability of the previously introduced languages for distributed evaluation of the functional programs on clusters. Here, therefore, we design distributed functional computational skeletons and we have provided a set of known algorithmic skeletons implemented as D-Clean schemes and a set of D-Box programs.