Search

During the lifetime of a software product certain changes could be performed on its source code. After those changes a regression test should be performed, which is the most expensive part of the software development cycle. This paper focuses on programs written in a dynamic functional programming language Erlang, and discusses a mechanism that could select those test cases, which are affected by a change, i.e. altering the program on some point may have impact on the result/behaviour of those test cases. In the result of that analysis it is possible to reduce the number of necessary test cases, and after modifying the source code, just a subset of the test cases should be retested. The discussed approach introduces a behaviour dependency graph for Erlang programs to represent the dependencies in the source code. The impact of a change can be calculated by traversing the graph. [ABSTRACT FROM AUTHOR]

Tool support for refactoring provides guarantees for the preservation of the program semantics during program transformation. This paper explains how RefactorErl, a refactoring tool for the Erlang language helps the programmer raise the quality of Erlang code or make the code suitable for further changes and improvements. Many examples illustrate the seven transformations currently implemented in RefactorErl. The paper also discusses the problems the refactor tool has to face. [ABSTRACT FROM AUTHOR]

HypereiDoc is an XML based framework supporting distributed, multi-layered, version-controlled processing of epigraphical, papyrological or similar texts in a modern critical edition. Such studies are typically based on independent work of philologists using annotation systems like the Leiden Conventions. Current initiatives like TEI and Epidoc have definitive limitations both in expressional power and the way how individual results can form a cooperative product. The HypereiDoc framework provides XML schema definition for a set of annotation-based layers connected by an extensive reference system, validating and building tools, and an editor on-line visualizing the base text and the annotations. The framework makes scholars able to work on the same text in a cooperative and distributed way. Our framework has been successfully tested by philologists working on the Hypereides palimpsest. [ABSTRACT FROM AUTHOR]

We synthesise a systolic pass-through array for the computation of the greatest common divisor (GCD) of multiple precision integers. The synthesis method uses the conceptual similarity between the inductive structure of a systolic array (a head processor followed by an identical tail array) and the inductive decomposition of the argument by a functional program. By formal analysis, we identify the structure of the functions which can be realized by pass-through arrays. Then, by equational rewriting, we transform the expression of the list function which must be realized into an expression having the required structure. The resulting expression reveals the scalar function which must be implemented by each individual processor. [ABSTRACT FROM AUTHOR]

We introduce a new partial inversion technique for first-order functional programs. Our technique is simple, fully automatic, and (when it succeeds) returns a program that belongs to the same class of the original program, namely the class of inductively sequential programs (i.e., typical functional programs). To ease the definition, our method proceeds in a stepwise manner: normalization (introduction of let expressions), proper inversion, and removal of let expressions. Furthermore, it can easily be implemented. Therefore, it forms an appropriate basis for developing a practically applicable transformation tool. Preliminary experiments with a prototype implementation of the partial inverter demonstrates the usefulness and viability of our approach. [ABSTRACT FROM AUTHOR]

A datatype-generic function is a family of functions indexed by (the structure of) a type. Examples include equality tests, maps and pretty printers. Property based testing tools like QuickCheck and Gast support the definition of properties and test-data generators, and they check if a monomorphic property is satisfied by the test cases. Generic functions satisfy generic properties and this paper discusses specifying and testing such properties. It shows how generic properties and generators can be expressed, and explains three bugs we found and corrected in the Generic Haskell library. [ABSTRACT FROM AUTHOR]

This paper provides guaranteed bounds on worst-case execution times for a strict, purely functional programming notation. Our approach involves combining time information obtained using a low-level commercial analyser with a high-level source-derived model to give worst-case execution time information. We validate our results using concrete timing information obtained using machine code fragments executing on a Renesas M32C/85 microcontroller development board. Our results confirm experimentally that our worst-case execution time model is a good predictor of execution times. [ABSTRACT FROM AUTHOR]

We modify Clean's uniqueness type system in two ways. First, while Clean functions that are partially applied to a unique argument are necessarily unique (they cannot lose their uniqueness), we just require that they must be unique when applied. This ultimately makes subtyping redundant. Second, we extend the type system to allow for higher-rank types. To be able to do this, we explicitly associate type constraints (attribute inequalities) with type schemes. Consequently, types in our system are much more precise about constraint propagation. [ABSTRACT FROM AUTHOR]

Type error messages that are reported for incorrect functional programs can be difficult to understand. The reason for this is that most type inference algorithms proceed in a mechanical, syntax-directed way, and are unaware of inference techniques used by experts to explain type inconsistencies. We formulate type inference as a constraint problem, and analyze the collected constraints to improve the error messages (and, as a result, programming efficiency). A special data structure, the type graph, is used to detect global properties of a program, and furthermore enables us to uniformly describe a large collection of heuristics which embed expert knowledge in explaining type errors. Some of these also suggest corrections to the programmer. Our work has been fully implemented and is used in practical situations, showing that it scales up well. We include a number of statistics from actual use of the compiler showing us the frequency with which heuristics are used, and the kind and number of suggested corrections. [ABSTRACT FROM AUTHOR]

This paper presents a method that facilitates formal reasoning about the correctness of programs. In this method, properties of programs (e.g. pre- and postconditions of functions) are described in terms of type invariants. Subtype marks are annotations attached to types and denote type invariants. A large amount of program properties expressed with subtype marks are verifiable fully automatically by an appropriate type system; the rest can be proven with a proof system. In this paper an eager pure functional language with a type system supporting subtype marks is briefly described. By assigning an interpretation to subtype marks, a concept of program correctness is introduced. The soundness of the presented type system is investigated. [ABSTRACT FROM AUTHOR]

Compiling indexing operations on n-dimensional arrays into efficiently executable code is a challenging task. This paper focuses on the reduction of offset computations as they typically occur when transforming index vectors into offsets for linearized representations of ndimensional arrays. We present a high-level optimization to that effect which is generally applicable, even in the presence of statically unknown rank (n). Our experiments show run-time improvements between a factor of 2 and 16 on a set of real-world benchmarks. [ABSTRACT FROM AUTHOR]

We present a low-level coordination language for Haskell which can be used as an implementation language for parallel Haskell extensions. It has been developed in the context of the latest Eden implementation (based on the Glasgow-Haskell-Compiler, GHC, version 6) and it is thus referred to as the "EDen Implementation language", EDI. EDI provides a small set of directly implemented primitive operations for basic thread control, system information, and communication. We explore the expressiveness and performance of both Eden and its low-level implementation language EDI in comparison. It turns out that hardly any differences in performance can be observed. The main advantage of EDI in comparison to Eden is more accurate control of parallel execution. Our long-term goals are maintenance and structured implementation of Eden and a solid low-level implementation language, which can be used for other parallel Haskells as well. [ABSTRACT FROM AUTHOR]

Dependent type theory has several practical applications in the fields of theorem proving, program verification and programming language design. Ivor is a Haskell library designed to allow easy extending and embedding of a type theory based theorem prover in a Haskell application. In this paper, I give an overview of the library and show how it can be used to embed theorem proving technology in an implementation of a simple functional programming language; by using type theory as a core representation, we can construct and evaluate terms and prove correctness properties of those terms within the same framework, ensuring consistency of the implementation and the theorem prover. [ABSTRACT FROM AUTHOR]

Assertions test expected properties of run-time values without disrupting the normal computation of a program. Here we present a library for enriching programs in the lazy language Haskell with assertions. Expected properties are written in an expressive pattern logic that combines pattern matching with logical operations and predicates. The presented assertions are lazy: they do not force evaluation but only examine what is evaluated by other parts of the program. They are also prompt: assertion failure is reported as early as possible, before a faulty value is used by the main computation. [ABSTRACT FROM AUTHOR]

The iData Toolkit is a purely functional toolkit for the Clean programming language to create highly dynamic, interactive, thin client web applications on a high level of abstraction. Its main building block is the iData element. With this element the programming effort of the application programmer is reduced significantly because it takes care of state handling, rendering, user interaction, and storage management automatically. In this paper we show that it can be used for even more tasks: handle destructively shared model data, perform version management, and state consistency management. This can be done entirely on top of the iData Toolkit. The toolkit comes with a new programming paradigm. We illustrate the extended power of the toolkit and programming paradigm by a case study of a conference management system. [ABSTRACT FROM AUTHOR]

This paper describes the HW-Hume level of the novel Hume language. HW-Hume is the simplest subset of Hume that we have identified. It provides strong formal properties but posseses limited abstraction capabilities. In this paper, we introduce HW-Hume, show some simple example programs, describe an efficient software implementation, and demonstrate how important properties can be exposed as part of an integrated formally-based verification approach. [ABSTRACT FROM AUTHOR]

In parallel functional languages, like Eden, lazy and strict evaluation are commonly mixed. Thus, the parallel performance of these languages depends on the strategy used to fix the degrees of laziness/ strictness. By using an implementation of Eden's operational semantics, we analyze the influence of alternative evaluation models on Eden skeletons performance. In particular, we assess the performance of different implementations of a skeleton that uses stream-based communications. [ABSTRACT FROM AUTHOR]

Shape-generic programming and high run time performance do match if generic source code is systematically specialised into nongeneric executable code. However, as soon as we drop the assumption of whole-world knowledge or refrain from specialisation for other reasons, compiled generic code is substantially less efficient. Limited effectiveness of code optimisation techniques due to the inherent lack of knowledge about the structural properties of arrays can be identified as the single most important source of inefficiency. However, in many cases partial structural information or structural relationships between arrays would actually suffice for optimisation. We propose symbolic array attributes as a uniform scheme to infer and to represent partial and relational structural information in shape-generic array code. By reusing the regular language to express structural properties in intermediate code, existing optimisations benefit from symbolic array attributes with little or no alteration. In fact, program optimisation and identification of structural properties cross-fertilise each other. We outline our approach in the context of the functional array language SaC and demonstrate its effectiveness by a small case study. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]