Traversal strategies à la Stratego (also à la Strafunski and ‘Scrap Your Boilerplate’) provide an exceptionally versatile and uniform means of querying and transforming deeply nested and heterogeneously structured data including terms in functional programming and rewriting, objects in OO programming, and XML documents in XML programming. However, the resulting traversal programs are prone to programming errors. We are specifically concerned with errors that go beyond conservative type errors; examples we examine include divergent traversals, prematurely terminated traversals, and traversals with dead code. Based on an inventory of possible programming errors we explore options of static typing and static analysis so that some categories of errors can be avoided. This exploration generates suggestions for improvements to strategy libraries as well as their underlying programming languages. Haskell is used for illustrations and specifications with sufficient explanations to make the presentation comprehensible to the non-specialist. The overall ideas are language-agnostic and they are summarized accordingly.

Spider diagrams are a visual language for expressing logical statements or constraints. Several sound and complete spider diagram systems have been developed and it has been shown that they are equivalent in expressive power to monadic first order logic with equality. However, these sound and complete spider diagram systems do not contain syntactic elements analogous to constants in first order predicate logic. We extend the spider diagram language to include constant spiders which represent specific individuals. Formal semantics are given for the extended diagram language. We prove that this extended system is equivalent in expressive power to the language of spider diagrams without constants and, hence, equivalent to monadic first order logic with equality.

The purpose of this study was to investigate the efficacy of audio-visual synchrony in podcasting and its possible pedagogical benefits. `Synchrony' in this study refers to the simultaneous playback of audio and video data streams, so that the transitions between presentation slides occur at ''lecturer chosen'' points in the audio commentary. Manufacturers of lecture recording software (e.g. ProfCast) would have us believe that the synchrony of image and audio should improve the learning experience. We have yet to see in the literature any empirical evidence to support this hypothesis. In our study, 90 participants in two groups undertook two electronic lectures (e-lectures) on two separate topics, the subject matter of neither was familiar to them beforehand. Each group experienced one ''synchronous'' presentation (e-lecture) of one of the topics, and one ''separate'' presentation (i.e. PowerPoint and audio files separately presented) of the other topic. Each group therefore experienced both ''synchronous'' and ''separate'' delivery and they were then given an MCQ test that assessed five levels of Bloom's taxonomy. Results show no differences in innate ability between the two groups but the evidence supported our primary hypothesis in that statistically significantly higher test scores were seen when participants viewed a synchronous e-lecture; these scores were accounted for by subjects' performance at three of the five levels of Bloom's taxonomy. Qualitative `attitude' survey results also displayed participant preference towards the synchronous over the asynchronous mode of delivery, and in spite of general acceptance of the proposed benefits of electronic proceedings, a majority preference towards traditional rather than electronic lectures. Despite this conservatism, this paper explores in more detail the potential benefits of podcasting via synchronous PowerPoint and voice.

Multimedia document authoring is a multifaceted activity, and authoring tools tend to concentrate on a restricted set of the activities involved in the creation of a multimedia artifact. In particular, a distinction may be drawn between the design and the implementation of a multimedia artifact. This paper presents a comparison of three different authoring paradigms, based on the common case study of a simple interactive animation. We present details of its implementation using the three different authoring tools, MCF, Fran and SMIL 2.0, and we discuss the conclusions that may be drawn from our comparison of the three approaches.

Spider diagrams are a visual language for expressing logical statements. In this paper we identify a well-known fragment of first-order predicate logic that we call MFOL=, equivalent in expressive power to the spider diagram language. The language MFOL= is monadic and includes equality but has no constants or function symbols. To show this equivalence, in one direction, for each diagram we construct a sentence in MFOL=, that expresses the same information. For the more challenging converse we prove that there exists a finite set of models for a sentence S that can be used to classify all the models for S. Using these classifying models we show that there is a diagram expressing the same information as S.

This paper presents a complete axiomatization for propositional interval temporal logic (PITL) with projection. The axiomatization is based on a tableau decision procedure for the logic, which in turn is founded upon a normal form for PITL formulae. The construction of the axiomatization provides a general mechanism for generating axiomatizations thus: given a normal form for a new connective, axioms can be generated for the connective from the tableau construction using that normal form. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

This paper explores a formalism for describing a wide class of multimedia document constraints. The formalism is based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical specification example. Then we present the temporal logic formalism that we use. This extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection like operator called filter and a new handling of interval length. A model theory and satisfaction relation is defined for the notation and a specification of the canonical example is presented.

This paper explores the idea of reactivity in multimedia, and proposes systems which can react to continuously-evolving behaviors as well as to more traditional discrete events. The idea is presented in a scenario as well as in a number of small programming examples. The illustrative examples are written in the Fran system. Fran provides a high-level programming model for animations, built in the Haskell functional programming language. Whilst we use Fran for illustration—and indeed we argue that the functional paradigm is a natural choice of host for such a system—we should stress that the notion of external behaviors within multimedia is independent of the programming environment chosen and could be incorporated into other systems such as SMIL.

It is now almost universally acknowledged that the data language ACT-ONE associated with the formal description technique LOTOS is inappropriate for the purpose of OSI formal description. In response to this the LOTOS restandardisation activity plans to replace ACT-ONE with a functional language. Thus, compatibility between ACT-ONE and the replacement data language becomes an issue. In response to this, we present an experimental investigation of backward compatibility between ACT-ONE and the new LOTOS data language. Specifically, we investigate translating ACT-ONE data types into the functional language Miranda. Miranda has been chosen as it is a widely used functional programming language and it is close in form to the anticipated new data language. This work serves as a ``verification of concept'' for translating ACT-ONE to the E-LOTOS data language. It identifies the bounds on embedding ACT-ONE in a functional data language. In particular, it indicates what can be translated and what cannot be translated. In addition, the paper reveals pertinent issues which can inform the E-LOTOS work. For example, which constructs are needed in E-LOTOS in order to support the class of data type specifications typically made in the LOTOS setting? We conclude with a number of specific recommendations for the E-LOTOS data language.

This paper expands upon work begun in the author's paper 'A Logic for Miranda', Formal Aspects of Computing 1 (1989), in building a logic for the Miranda functional programming language. After summarising the work in that paper, a translation of Miranda definitions into logical formulas is presented, and illustrated by means of examples. This work expands upon the earlier paper in giving a complete treatment of sequences of equations, and by examining how to translate the local definitions introduced by where clauses. The status of the logic is then examined, and it is argued that the logic extends a natural operational semantics of Miranda, given by the translations of definitions into conditional equations. Finally it is shown how the logic can be implemented in the Isabelle proof tool. This paper has been accepted for publication in Formal Aspects of Computing.

In this paper we present the equivalence between TIM, a machine developed to implement lazy functional programming languages, and the set of Categorical Multi-Combinators, a rewriting system developed with similar aims. A Complete revision of UKC - Lab.Report 67 (Submitted to Journal of Functional Programming)

Implementations of functional programming languages can take a number of different forms, and many different machines have been developed for this purpose. This paper introduces another abstract machine, the Categorical Multi-Combinator Machine (CMCM). A thorough introduction to the machines is given, particularly as far as the discussion of the starting of computational information is concerned.

This chapter outlines perspectives on information technology (IT), including definitions of IT, and discusses the way these shape the WIL experience. A continuum model of cooperative education is introduced, followed by an exploration of its components and characteristics through a set of examples and a case study of various hybrid approaches to work-integrated learning in IT. Observing that IT encompasses a diversity of cooperative education models, the chapter concludes with a brief review of issues particular to cooperative education in IT.

We present a framework for making a refactoring tool extensible, allowing users to define refactorings from scratch using the concrete syntax of the language, as well as to describe complex refactorings in a domain-specific language for scripting. We demonstrate the approach in practice through a series of examples. The extension framework is built into Wrangler, a tool for refactoring Erlang programs, but we argue that the approach is equally applicable to tools for other languages.

Genetic programming has proven capable of evolving solutions to a wide variety of problems. However, the successes have largely been with programs without iteration or recursion; evolving recursive programs has turned out to be particularly challenging. The main obstacle to evolving recursive programs seems to be that they are particularly fragile to the application of search operators: a small change in a correct recursive program generally produces a completely wrong program. In this paper, we present a simple and general method that allows us to pass back and forth from a recursive program to an associated non-recursive program. Finding a recursive program can be reduced to evolving non-recursive programs followed by converting the optimum non-recursive program found to the associated optimum recursive program. This avoids the fragility problem above, as evolution does not search the space of recursive programs. We present promising experimental results on a test-bed of recursive problems.

Refactoring is the process of changing the design of a program without changing its behaviour. Many refactoring tools have been developed for various programming languages; their support for composite refactorings â?? refactorings that are composed from a number of primitive refactorings

Wrangler is a refactoring and code inspection tool for Erlang programs. Apart from providing a set of built-in refactorings and code inspection functionalities, Wrangler allows users to define refactorings, code inspections, and general program transformations for themselves to suit their particular needs. These are defined using a template-and rule-based program transformation and analysis framework built into Wrangler.

A QuickCheck property is a logical statement of aspects of the behaviour of a system. We report on how similar test cases in a test suite written in Erlang can be identified and then refactored into properties, giving a generalisation of the specification implicit in the test suite. Properties give more concise, easier to maintain test suites and better test coverage. A preliminary evaluation of the techniques in industry demonstrates feasibility as well as potential benefits.A QuickCheck property is a logical statement of aspects of the behaviour of a system. We report on how similar test cases in a test suite written in Erlang can be identified and then refactored into properties, giving a generalisation of the specification implicit in the test suite. Properties give more concise, easier to maintain test suites and better test coverage. A preliminary evaluation of the techniques in industry demonstrates feasibility as well as potential benefits

A well-known bad code smell in refactoring and software maintenance is the existence of code clones, which are code fragments that are identical or similar to one another. This paper describes an approach to incrementally detecting 'similar' code based on the notion of least-general common abstraction, or anti-unification, as well as a framework for user-controlled incremental elimination of code clones within the context of Erlang programs. The clone detection algorithm proposed in this paper achieves 100 precision, high recall rate, and is user-customisable regarding the granularity of the clone classes reported. By detecting and eliminating clones in an incremental way, we make it possible for the tool to be used in an interactive way even with large codebases. Both the clone detection and elimination functionalities are integrated with Wrangler, a tool for interactive refactoring of Erlang programs. We evaluate the approach with various case studies.

Erlang processes run independently of each other, each using separate memory and communicating with each other by message passing. These processes, while executing different code, do so following a number of common patterns. By examining different examples of Erlang-style concurrency in client/server architectures, we identify the generic and specific parts of the code and extract the generic code to form a process skeleton. In Erlang, the most commonly used patterns have been implemented in library modules, commonly referred to as OTP behaviours. They contain the generic code framework for concurrency and error handling, simplifying the complexity of concurrent programming and protecting the developer from many common pitfalls.

This paper uses the inference of finite state machines from EUnit test suites for Erlang programs to make two contributions. First, we show that the inferred FSMs provide feedback on the adequacy of the test suite that is developed incrementally during the test-driven development of a system. This is novel because the feedback we give is independent of the implementation of the system. Secondly, we use FSM inference to develop QuickCheck properties for testing state-based systems. This has the effect of transforming a fixed set of tests into a property which can be tested using randomly generated data, substantially widening the coverage and scope of the tests.

Low coupling between modules and high cohesion inside each module are the key features of good software architecture. Systems written in modern programming languages generally start with some reasonably well-designed module structure; however with continuous feature additions, modifications and bug fixes, software modularity gradually deteriorates; and there is a need for incrementally improving modularity to avoid the situation when the structure of the system becomes too complex to maintain. We demonstrate how Wrangler, a general-purpose refactoring tool for Erlang, could be used to maintain and improve the modularity of programs written in Erlang without dramatically changing the existing module structure. We identify a set of ''modularity smells'' and show how they can be detected by Wrangler and removed by way of a variety of refactorings implemented in Wrangler. Validation of the approach and usefulness of the tool are demonstrated by case studies.

We report on how the Wrangler refactoring tool has been used to improve and transform test code for Erlang systems. This has been achieved through the removal of code clones, the identification of properties for property-based testing and the definition of testing-aware refactorings and test-framework-specific refactorings. While some of the observations are Erlang-specific, others apply to test code in general.

Refactoring is the transformation of program source code in a way that preserves the behaviour of the program. Many tools exist for automating a number of refactoring steps, but these tools are often poorly tested. We present an automated testing framework based on QuickCheck for testing refactoring tools written for the Erlang programming language.

Investigating the expressiveness of a diagrammatic logic provides insight into how its syntactic elements interact at the semantic level. Moreover, it allows for comparisons with other notations. Various expressiveness results for diagrammatic logics are known, such as the theorem that Shin's Venn-II system is equivalent to monadic first order logic. The techniques employed by Shin for Venn-II were adapted to allow the expressiveness of Euler diagrams to be investigated. We consider the expressiveness of spider diagrams of order (SDoO), which extend spider diagrams by including syntax that provides ordering information between elements. Fragments of SDoO are created by systematically removing each aspect of the syntax. We establish the relative expressiveness of the various fragments. In particular, one result establishes that spiders are syntactic sugar in any fragment that contains order, negation and shading. We also show that shading is syntactic sugar in any fragment containing negation and spiders. The existence of syntactic redundancy within the spider diagram of order logic is unsurprising however, we find it interesting that spiders or shading are redundant in fragments of the logic. Further expressiveness results are presented throughout the paper. The techniques we employ may well extend to related notations, such as the Euler/Venn logic of Swoboda et al. and Kent's constraint diagrams.

Refactoring is the process of changing the structure of a program while preserving its behaviour. This behaviour preservation is crucial so that refactorings do not introduce any bugs. Refactoring is aimed at increasing code quality, programming productivity and code reuse. Refactoring has been practised manually by programmers for as long as programs have been written; however, with the advent of refactoring tools, refactoring can be performed semi-automatically, allowing refactorings to be performed (and undone) easily. In this paper, we briefly describe a number of refactorings implemented in the Haskell Refactorer, HaRe. In addition to this, we also implement a simple expression processor to demonstrate how some of the refactorings implemented in HaRe can be used to aid programmers in developing Haskell software.

Duplicated code is a well known problem in software maintenance and refactoring. Code clones tend to increase program size and several studies have shown that duplicated code makes maintenance and code understanding more complex and time consuming. This paper presents a new technique for the detection and removal of duplicated Haskell code. The system is implemented within the refactoring framework of the Haskell Refactorer (HaRe), and uses an Abstract Syntax Tree (AST) based approach. Detection of duplicate code is automatic, while elimination is semi-automatic, with the user managing the clone removal. After presenting the system, an example is given to show how it works in practice.

A well-known bad code smell in refactoring and software maintenance is duplicated code, that is the existence of code clones, which are code fragments that are identical or similar to one another. Unjustified code clones increase code size, make maintenance and comprehension more difficult, and also indicate design problems such as a lack of encapsulation or abstraction. This paper describes an approach to detecting `similar' code based on the notion of anti-unification, or least-general common abstraction. This mechanism is used for detecting code clones in Erlang programs, and is supplemented by a collection of refactorings to support user-controlled automatic clone removal. The similar code detection algorithm and refactorings are integrated within Wrangler, a tool developed at the University of Kent for interactive refactoring of Erlang programs. We conclude with a report on case studies and comparisons with other tools.

A well-known bad code smell in refactoring and software maintenance is duplicated code, or code clones. A code clone is a code fragment that is identical or similar to another. Unjustified code clones increase code size, make maintenance and comprehension more difficult, and also indicate design problems such as lack of encapsulation or abstraction. This paper proposes a token and AST based hybrid approach to automatically detecting code clones in Erlang/OTP programs, underlying a collection of refactorings to support user-controlled automatic clone removal, and examines their application in substantial case studies. Both the clone detector and the refactorings are integrated within Wrangler, the refactoring tool developed at Kent for Erlang/OTP.

This paper proposes a token and AST based hybrid approach to automatically detecting code clones in Erlang/OTP programs, underlying a collection of refactorings to support user-controlled automatic clone removal. Both the clone detector and the refactorings are integrated within Wrangler, the refactoring tool developed for Erlang/OTP.

Testing is the predominant way of establishing evidence that a program meets it requirements. When both test code and the application under test are written in the same programming language, a refactoring tool for this language should be able to refactor both application code and testing code together. However, testing frameworks normally come with particular programming idioms, such as their use of naming conventions, coding patterns, meta-programming techniques and the like. A refactoring tool needs to be aware of those programming idioms in order to refactor test code properly. Meanwhile the particularities of test code also suggest refactorings that are particularly applicable to test code. In this paper we present our experience of extending Wrangler, a refactoring tool for the Erlang programming language, so as to handle the three common testing frameworks for Erlang, as well as discussing the refactoring of test code in its own right.

Tool Support for Refactoring Functional Programs We demonstrate the Haskell Refactorer, HaRe, and the Erlang Refactorer, Wrangler, as examples of fully-functional refactoring tools for functional programming languages. HaRe and Wrangler are designed to handle multi-module projects in complete languages: Haskell 98 and Erlang/OTP. They are embedded in emacs (and gvim) and respect programmer layout styles. In discussing the construction of HaRe and Wrangler, we comment on the different challenges presented by Haskell and Erlang due to their differences in syntax, semantics and pragmatics. In particular, we examine the sorts of analysis that underlie our systems. Finally, drawing on our experience, we examine features common to functional refactorings, and contrast these with refactoring in the object-oriented domain.

In this paper we describe the formal verification of refactorings for untyped and typed lambda-calculi. This verification is performed in the proof assistant Isabelle/HOL. Refactorings are program transformations applied to improve the design of source code. Well-structured source code is easier and cheaper to maintain, and this motivates the use of refactoring. These transformations have been implemented as programmer tools and, as with other metaprogramming tools, it is desirable that implementations of refactorings are correct. For a refactoring to be correct the refactored program must be identical in behaviour to the original program. Since refactorings are source-to-source transformations, concrete program information matters: for example, names (of variables, procedures, etc) and program layout should also be preserved by refactoring. This is a particular characteristic of refactorings since general program transformations operate over machine representations of programs, rather than readable source code. The paper describes the formalisation adopted, and the alternatives explored. It also reflects on some of the difficulties of performing such formalisations, the interaction between refactoring and phases such as type-checking and parsing, and the generation of correct implementations from mechanised proofs.

Traversal strategies provide an established means of describing automated queries, analyses, transformations, and other non-trivial computations on deeply structured data (including, most notably, data representations of software artifacts such as programs). The resulting traversal programs are prone to programming errors. We are specifically concerned with errors that go beyond classic type errors, in particular: (i) divergence of traversal, (ii) unintentional extent of traversal into data, (iii) trivial traversal results, (iv) inapplicability of the constituents of a traversal program along traversal. We deliver a taxonomy of programming errors, and start attacking some of them by refinements of traversal programming.

A well-known bad code smell in refactoring and software maintenance is duplicated code, or code clones. A code clone is a code fragment that is identical or similar to another. Unjustified code clones increase code size, ake maintenance and comprehension more difficult, and also indicate design problems such as lack of encapsulation or abstraction. This paper proposes a token and AST based hybrid approach to automatically detecting code clones in Erlang/OTP programs, underlying a collection of refactorings to support user-controlled automatic clone removal, and examines their application in substantial case studies. Both the clone detector and the refactorings are integrated within Wrangler, the refactoring tool developed at Kent for Erlang/OTP.

The paper surveys how software tools such as refactoring systems can be validated, and introduces a new mechanism, namely the extraction of a refactoring engine for a functional programming language from an Isabelle/HOL theory in which it is verified. This research is a first step in a programme to construct certified programming tools from verified theories. We also provide some empirical evidence of how refactoring can be of significant benefit in reshaping automatically-generated program code for use in larger systems.

The spider diagram logic forms a fragment of the constraint diagram logic and was designed to be primarily used as a diagrammatic software specification tool. Our interest is in using the logical basis of spider diagrams and the existing known equivalences between certain logics, formal language theory classes and some automata to inform the development of diagrammatic logics. Such developments could have many advantages, one of which would be aiding software engineers who are familiar with formal languages and automata to more intuitively understand diagrammatic logics. In this paper we consider relationships between spider diagrams of order (an extension of spider diagrams) and the star-free subset of regular languages. We extend the concept of the language of a spider diagram to encompass languages over arbitrary alphabets. Furthermore, the product of spider diagrams is introduced. This operator is the diagrammatic analogue of language concatenation. We establish that star-free languages are definable by spider diagrams of order equipped with the product operator and, based on this relationship, spider diagrams of order are as expressive as first order monadic logic of order.

Wrangler is a refactoring tool for Erlang, implemented in Erlang. This paper reports the latest developments in Wrangler, which include improved user experience. the introduction of a number of data- and process-related refactorings, and also the implementation of an Eclipse plug-in which, together with Erlide, provides refactoring support for Erlang in Eclipse.

Wrangler is a refactoring tool for Erlang, implemented in Erlang. This paper reports the latest developments in Wrangler, which include the introduction of a number of data- and process-related refactorings, and also the implementation of an Eclipse plug-in which, together with Erlide, provides refactoring support for Erlang in Eclipse.

We present the Haskell Refactorer, HaRe, and the Erlang Refactorer, Wrangler, as examples of fully-functional refactoring tools for functional programming languages. HaRe and Wrangler are designed to handle multi-module projects in complete languages: Haskell 98 and Erlang/OTP. They are embedded in Emacs, (gVim and Eclipse) and respect programmer layout styles. In discussing the construction of HaRe and Wrangler, we comment on the different challenges presented by Haskell and Erlang due to their differences in syntax, semantics and pragmatics. In particular, we examine the sorts of analysis that underlie our systems.

Refactoring is a technique for improving the design of existing programs without changing their behaviour. Wrangler is a tool built at the University of Kent to support Erlang program refactoring; the Wrangler tool is written in Erlang. In this paper we present the use of a novel testing tool, Quviq QuickCheck, for testing the implementation of Wrangler. QuickCheck is a specification-based testing tool for Erlang. With QuickCheck, programs are tested by writing properties in a restricted logic, and using the tool these properties are tested in randomly generated test cases. This paper first gives overviews of Wrangler and Quviq QuickCheck, then discusses the various ways in which refactorings can be validated, and finally shows how QuickCheck can be used to test the correctness of refactorings in an efficient way.

We present a set of XML language extensions that bring notions from functional programming to web authors, extending the power of declarative modelling for the web. Our previous work discussed expressions and user-defined events. In this paper, we discuss how one may extend XML by adding definitions and parameterization; complex data and data types; and reactivity, events and continuous ''behaviours''. We consider these extensions in the light of World Wide Web Consortium standards, and illustrate their utility by a variety of use cases.

We describe refactoring for Erlang programs, and work in progress to build two tools to give machine support for refactoring systems written in Erlang. We comment on some of the peculiarities of refactoring Erlang programs, and describe in some detail a number of refactorings characteristic of Erlang.

Refactoring is about changing the design of existing code without changing its behaviour, but with the aim of making code easier to understand, modify, or reuse. Taking Haskell and Erlang as examples, we investigate the application of refactoring techniques to functional programs, and building tools for supporting interactive refactoring. Although both Haskell and Erlang are general-purpose functional programming languages, they have many differences in their language design and programming idioms. As a result, program refactoring in the two languages has much in common, but also considerable differences. This paper makes this comparison, and in particular looks in more detail at the refactorings applicable in each language, the program analysis required by typical refactorings, and at tool support for refactoring Haskell and Erlang programs.

Diagrammatic notations, such as the Unified Modeling Language (UML), are in common use in software development. They allow many aspects of software systems to be described diagrammatically, but typically they rely on textual notations for logical constraints. In contrast, spider diagrams provide a visual notation for expressing a natural class of set- theoretic statements in a diagrammatic form. In this paper we present a tableau system for spider diagrams, and describe an implementation of the system. In a software development context, the system allows users to explore the implications of design choices, and thus to validate specifications; beyond this, the tableau algorithm and system are of general interest to visual reasoners.

Many visual languages based on Euler diagrams have emerged for expressing relationships between sets. The expressive power of these languages varies, but the majority can only express statements involving unary relations and, sometimes, equality. We present a new visual language called Visual First Order Logic (VFOL) that was developed from work on constraint diagrams which are designed for software specification. VFOL is likely to be useful for software specification, because it is similar to constraint diagrams, and may also fit into a Z-like framework. We show that for every First Order Predicate Logic (FOPL) formula there exists a semantically equivalent VFOL diagram. The translation we give from FOPL to VFOL is natural and, as such, VFOL could also be used to teach FOPL, for example.

Software metrics have been used in software engineering as a mechanism for assessing code quality and for targeting software development activities, such as testing or refactoring, at areas of a program that will most benefit from them. Haskell has many tools for software engineering, such as testing, debugging and refactoring tools, but software metrics have mostly been neglected. The work presented in this paper identifies a collection of software metrics for use with Haskell programs. These metrics are subjected to statistical analysis to assess the correlation between their values and the number of bug fixing changes occurring during the development lifetime of two case study programs. In addition to this, the relationships between the metric values is also explored, showing how combinations of metrics can be used to improve the accuracy of the measurements.

Refactoring is a well-known technique for improving the design of existing programs without changing their external behaviour. HaRe is the refactoring tool we have built to support refactoring Haskell programs. Along with the development of HaRe, This formalisation process helps to clarify the meaning of refactorings, improves our confidence in the behaviour-preservation of refactorings, and reduces the need for testing. This paper gives an overview of HaRe, and shows our approach to the formalisation of refactorings.

Spider diagrams are a visual language for expressing logical statements. Spiders represent the existence of elements and contours denote sets. Several sound and complete spider diagram systems have been developed and it is known that the spider diagram language is equivalent in expressive power to monadic first order logic with equality. However, these sound and complete spider diagram systems do not contain syntactic elements analogous to constants in first order predicate logic. We extend the spider diagram language to include constant spiders which represent specific individuals and give formal semantics for the extended diagram language. We then prove that this extended system is equivalent in expressive power to the language of spider diagrams without constants.

Spider diagrams are a visual notation for expressing logical statements. In this paper we identify a well known fragment of first order predicate logic, that we call ESD, equivalent in expressive power to the spider diagram language. The language ESD is monadic and includes equality but has no constants or function symbols. To show this equivalence, in one direction, for each diagram we construct a sentence in ESD that expresses the same information. For the more challenging converse we show there exists a finite set of models for a sentence S that can be used to classify all the models for S. Using these classifying models we show that there is a diagram expressing the same information as S.

XML and its associated languages are emerging as powerful authoring tools for multimedia and hypermedia web content. Furthermore, intelligent presentation generation engines have begun to appear, as have models and platforms for adaptive presentations. However, XML-based models are limited by their lack of expressiveness in presentation and animation. As a result, authors of dynamic, adaptive web content must often use considerable amounts of script or code. The use of such script or code has two serious drawbacks. First, such code undermines the declarative description possible in the original presentation language, and second, the scripting/coding approach does not readily lend itself to authoring by non-programmers. In this paper we describe a set of XML language extensions, inspired by features from the functional programming world, which are designed to widen the class of reactive systems which could be described in languages such as SMIL. The features which we discuss extend the power of declarative modeling for the web by allowing the introduction of web media items which may dynamically react to continuously varying inputs, both in a continuous way and by triggering discrete, user-defined, events. The two extensions described herein are discussed in the context of SMIL Animation and SVG, but could be applied to many XML-based languages.

Refactoring is the process of improving the design of existing programs without changing their functionality. These notes cover refactoring in functional languages, using Haskell as the medium, and introducing the HaRe tool for refactoring in Haskell.

Refactorings are source-to-source program transformations which change program structure and organisation, but not program functionality. Documented in catalogues and supported by tools, refactoring provides the means to adapt and improve the design of existing code, and has thus enabled the trend towards modern agile software development processes. Refactoring has taken a prominent place in software development and maintenance, but most of this recent success has taken place in the OO and XP communities. In our project, we explore the prospects for Refactoring Functional Programs, taking Haskell as a concrete case-study. This paper discusses the variety of pragmatic and implementation issues raised by our work on the Haskell Refactorer. We briefly introduce the ideas behind refactoring, and a set of elementary functional refactorings. The core of the paper then outlines the main challenges that arise from our aim to produce practical tools for a decidedly non-toy language, summarizes our experience in trying to establish the necessary meta-programming infrastructure and gives an implementation overview of our current prototype refactoring tool. Using Haskell as our implementation language, we also offer some preliminary comments on Haskell programming-in-the-large.

Refactoring is the process of redesigning existing code without changing its functionality. Refactoring has recently come to prominence in the OO community. In this paper we explore the prospects for refactoring functional programs. Our paper centres on the case study of refactoring a 400 line Haskell program written by one of our students. The case study illustrates the type and variety of program manipulations involved in refactoring. Similarly to other program transformations, refactorings are based on program equivalences, and thus ultimately on language semantics. In the context of functional languages, refactorings can be based on existing theory and program analyses. However, the use of program transformations for program restructuring emphasises a different kind of transformation from the more traditional derivation or optimisation: characteristically, they often require wholesale changes to a collection of modules, and although they are best controlled by programmers, their application may require nontrivial semantic analyses. The paper also explores the background to refactoring, provides a taxonomy for describing refactorings and draws some conclusions about refactoring for functional programs.

The move towards a semantic web will produce an increasing number of presentations whose creation is based upon semantic queries. Intelligent presentation generation engines have already begun to appear, as have models and platforms for adaptive presentations. However, in many cases these models are constrained by the lack of expressiveness in current generation presentation and animation languages. Moreover, authors of dynamic, adaptive web content must often use considerable amounts of script or code, thus breaking the declarative description possible in the original presentation language. Furthermore, the scripting/coding approach does not lend itself to authoring by non-programmers. In this paper we describe a set of XML language extensions that bring tools from the functional programming world to web authors, extending the power of declarative modeling for the web. The extensions are described in the context of SMIL Animation and SVG, but could be applied to many XML-based languages.

This report contains the proceedings of the International Workshop on Functional and Declarative Programming in Education (FDPE 2002), held in Pittsburgh (USA) on October 7, 2002 as part pf PLI 2002 (Principles, Logics, and Implementations of high-level programming languages). Functional and declarative programming plays an increasingly important role in computing education at all levels. This workshop aimed at bringing together educators and others who are interested in exchanging ideas on how to use a functional or declarative programming style in the classroom. Previous workshops have been held in Paris (1999) and Southampton (1997). The technical program of the workshop included standard presentations as well as short talks or "tricks of the trade" presentations focusing on small but neat ides. The organizers reviewed all papers submitted in response to a call for papers. Following the review process and a lively email discussion, the organizers selected the papers contained in these proceedings for presentation at the workshop. The organizers would like to thank the organization team of PLI 2002 for hosting the workshop and Klaus Höppner for his help in the preparation of the proceedings.

We show how the Aldor type system can represent propositions of first-order logic, by means of the 'propositions as types' correspondence. The representation relies on type casts (using pretend) but can be viewed as a prototype implementation of a modified type system with type evaluation reported elsewhere [9]. The logic is used to provide an, axiomatisation of a number of familiar Aldor categories as well as a type of vectors

A number of combinations of reasoning and computer algebra systems have been proposed; in this paper we describe another, namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Alder - the Axiom Library Compiler and show that with some modifications we can use the dependent types of the system to model a logic, under the Curry-Howard isomorphism. We give a number of example applications of the logic we construct and explain a prototype implementation of a modified type-checking system written in Haskell.

This paper presents a taxonomy of possible synchronization relationships between pairs of items in multimedia documents. Several existing approaches to the synchronization of entire items are reviewed. We then discuss classes of synchronization based upon dynamic events or conditions occurring within media items and their internal structure. We present a taxonomy of seventy-two possible such relations, which are illustrated by numerous examples and which are formalized in the authors' temporal logic notation, Mexitl. The ideas are then applied to provide a description of the lip-synchronization problem.

Tableau Methods have been extensively investigated for standard (infinite) temporal logics and there has been some tableau work in the interval temporal logic setting. However, this work has not considered the important projection operator. This paper responds to this deficiency by defining just such a tableau algorithm which handles the projection operator.

This paper introduces a problem solving method for teaching functional programming, based on Polya's `How To Solve It', an introductory investigation of mathematical method. We first present the language independent version, and then show in particular how it applies to the development of programs in Haskell. The method is illustrated by a sequence of examples and a larger case study.

This paper describes our experiences in devising a lightweight, informal methodology for problem solving in introductory, university level, computer science. We first describe the original context of the experiment and the background to the methodology. We then give the details of the steps of the Problem Solving Cycle - Understanding, Designing, Writing and Reviewing - and the lessons we learned about our teaching from devising the material. We also present practical examples of how it has been applied in a variety of units in our programme.

This paper explores a formalism for describing a wide class of multimedia document constraints. The formalism is based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical document example. Then we present the temporal logic formalism that we use. This formalism extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection-like operator called filter and a new handling of interval length. A model theory and satisfaction relation is defined for the notation and a specification of the canonical example is presented.

This paper gives an implementation of an interval temporal logic in a constructive type theory, using the Alf proof system. After explaining the constructive approach, its relevance to interval temporal logic and potential applications of our work, we explain the fundamentals of the Alf system. We then present the implementation of the logic and give a number of examples of its use. We conclude by exploring how the work can be extended in the future.

This paper discusses our experience in using a functional language in topics across the computer science curriculum. After examining the arguments for taking a functional approach, we look in detail at four case studies from different areas: programming language semantics, machine architectures, graphics and formal languages.

This paper describes our experience in formalising arguments about the Miranda functional programming language in Isabelle. After explaining some of the problems of reasoning about Miranda, we explain our two different approaches to encoding Miranda in Isabelle. We conclude by discussing some shorter examples and a case study of reasoning about hardware.

After introducing Martin-Lof's type theory, the paper introduces the rules proposed by various authors for adding subset types to the system, and the justification given for their addition. These justifications are examined, and it is argued that by a combination of lazy evaluation and transformation using the Axiom of Choice that subsets need not be added to the system to make it usable.

Refactoring is the process of changing the design of a program without changing what it does. While it is possible to refactor a program by hand, tool support is considered invaluable as it allows large-scale refactorings to be performed easily. However, most refactoring tools are black boxes, supporting a fixed set of `core' refactorings. This paper reports the framework built into Wrangler â?? a refactoring and code inspection tool for Erlang programs

Refactoring is the process changing the design of a program without changing its behaviour. Many refactoring tools have been developed for various programming languages; while these told support primitive, atomic refactorings, support for composite refactorings â?? refactorings that are composed from a number of primitive refactorings

In this paper we show how the 'similar code' detection facilities of Wrangler, combined with its portfolio of refactorings, allow test code to be shrunk dramatically, under the guidance of the test engineer. This is illustrated by a sequence of refactorings of a test suite taken from an Erlang project at Ericsson AB.

This work is a continuation of previous, published joint work towards a set of XML language extensions that bring tools from the functional programming world to web authors, extending the power of declarative modeling for the web. Our previous work concentrated on two aspects, expressions and user-defined events, and deliberately left aside other questions regarding data types, encapsulation and so forth. Work addressed here includes the addition of various facilities to XML languages including definitions and parameterization; complex data and data types; reactivity, events and continuous ''behaviours''. We have considered these extensions in the light of existing and emerging World Wide Web Consortium standards.

Refactoring is the process of redesigning existing code without changing its functionality. Refactoring has recently come to prominence in the OO community. In this paper we explore the prospects for refactoring functional programs. Our paper centres on the case study of refactoring a 400 line Haskell program written by one of our students. The case study illustrates the type and variety of program manipulations involved in refactoring. Similarly to other program transformations, refactorings are based on program equivalences, and thus ultimately on language semantics. In the context of functional languages, refactorings can be based on existing theory and program analyses. However, the use of program transformations for program restructuring emphasises a different kind of transformation from the more traditional derivation or optimisation: characteristically, they often require wholesale changes to a collection of modules, and although they are best controlled by programmers, their application may require nontrivial semantic analyses. The paper also explores the background to refactoring, provides a taxonomy for describing refactorings and draws some conclusions about refactoring for functional programs.

This paper presents a complete axiomatisation for propositional interval temporal logic (PITL) with projection. The axiomatisation is based on a tableau procedure for the logic, which in turn is founded upon a normal form for PITL formluae. The construction of the axiomatisation is modular, in the sense that given a normal form for a new connective, axioms can be generated for the connective from the tableau construction. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

The paper begins with definitions of regular expressions, and how strings are matched to them; this also gives our first Haskell treatment also. After describing the abstract data type of sets we define non-deterministic finite automata, and their implementation in Haskell. We then show how to build an NFA corresponding to each regular expression, and how such a machine can be optimised, first by transforming it into a deterministic machine, and then by minimising the state space of the DFA. We conclude with a discussion of regular definitions, and show how recognisers for strings matching regular definitions can be built.

As part of a project to include reasoning capabilities in the Aldor computer algebra system it is necessary to modify the type checking algorithm in Aldor. This paper reports on work to write Aldor abstract syntax trees as elements of Haskell data types, and to implement a prototype modified type checker for Aldor in Haskell.

This paper gives a formal description of (at least a part of) the type system of Aldor, the extension language of the computer algebra system AXIOM. In the process of doing this a critique of the design of the system emerges.

A number of combinations of theorem proving and computer algebra systems have been proposed; in this paper we describe another, namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Aldor -- the Axiom Library Compiler -- and show that with some modifications we can use the dependent types of the system to model a logic, under the Curry-Howard isomorphism. We give a number of example applications of the logic we construct.

This paper uses the Functional Reactive Animation system, Fran, to give a simulation of a simple two floor lift (or elevator). We introduce those aspects of Fran relevant to the simulation, thus making the paper self-contained. We show how to extend the design to one for a lift with an arbitrary number of floors, and we conclude the paper with a discussion of how the Fran simulation can be verified in an informal temporal logic.

In this paper we present a complete tableau method for interval temporal logic including the projection operator. Central to our strategy is the identification of normal forms for all the operators of our logic. In effect, these normal forms give inductive definitions of the ITL operators. Then, in the style of Wolper, we define a tableau decision procedure to check satisfiability of our logic. For simplicity of presentation we work in the propositional setting.

This paper explores a formalism for describing a wide class of multimedia document constraints, based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical specification example. Then we present the temporal logic formalism that we use. This extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection-like operator called filter and a new handling of interval length. A model theory, logic and satisfaction relation are defined for the notation, a specification of the canonical example is presented, and a proof system for the logic is introduced.

This paper explores how certain ideas in object oriented languages have their correspondents in functional languages. In particular we look at the analogue of the iterators of the C++ standard template library. We also give an example of the use of constructor classes which feature in Haskell 1.3 and Gofer.

Constructive type theories, such as that of Martin-Lof, allow program construction and verification to take place within a single system: proofs may be read as programs and propositions as types. However, parts of proofs may be seen to be irrelevant from a computational viewpoint. We show how a form of abstract interpretation may be used to detect computational redundancy in a functional language based upon Martin-Lof's type theory. Thus, without making any alteration to the system of type theory itself, we present an automatic way of discovering and removing such redundancy. We also note that the strong normalisation property of type theory means that proofs of correctness of the abstract interpretation are simpler, being based upon a set-theoretic rather than a domain-theoretic semantics. Keywords: Type theory, functional programming, computational redundancy, abstract interpretation.

This paper explains the use of the functional programming language Miranda as a vehicle for describing the semantics of imperative programming languages. In particular we give a Miranda denotational description of a substantial subset of a Pascal-like language, describing a number of variants of the semantics, including parameter passing by value-result, dynamic binding of values to names and a simple semantics of jumps. We also give an executable operational semantics of our basic language, as well as a compiler for this language into a simple stack machine, which is itself modelled in Miranda.

In these notes Miranda is used as a vehicle to introduce regular expressions, pattern matching, and their implementations by means of non-deterministic and deterministic automata. As part of the material, we give an implementation of the ideas, contained in a set of files. References to this material are scattered through the text. The files can be obtained by following the instructions in medskip noindent tt http://www.ukc.ac.uk/computer_science/Miranda_craft/regExp.html medskip noindent This material is based on the treatment of the subject in `the Dragon book', but provides full implementations rather than their pseudo-code versions of the algorithms. The material gives an illustration of many of the features of Miranda, including polymorphism (the states of an NFA can be represented by objects of any type); modularisation (the system is split across a number of modules); higher-order functions (used in finding limits of processes, for example) and other features.

The functional programming language Haskell is examined from the point of view of proving programs correct. Particular features explored include the data type definition facilities, classes, the behaviour of patterns and guards and the monad approach to IO in the Glasgow Haskell compiler.

In this paper we present a model of interactive programs in a purely functional style. We exploit lazy evaluation in the modelling of streams as lazy lists. We show how programs may be constructed in an ad hoc way, and then present a small set of interactions and combinators which form the basis for a disciplined approach to writing such programs. One of the difficulties of the ad hoc approach is that the way in which input and output are interleaved by the functions can be unpredictable. In the second half of the paper we use traces, i.e. partial histories of behaviour, to explain the interleaving of input and output, and give a formal explanation of our combinators. We argue that this justifies our claim that the combinators have the intuitively expected behaviour, and finally contrast our approach with another.