A formal specification describes a problem to be solved on a high level - ideally, it specifies what has to be done, but not how. Such descriptive specifications facilitate the derivation of any of the possible solutions, whereas operational specifications suggest only particular ones. Formal derivations in this framework consist of semantics preserving transformations, i.e. steps that proceed from solutions to the initial specification to other, more defined, more operational, or more efficient ones. Thus, the resulting programs are correct by construction with respect to their initial specifications. This thesis contains a number of case studies aiming at the exploration of new territories in the area of program specification and transformation. /pubs/1992/159/''Improving recursive functions by inverting the order of evaluation'' gives a comprehensive survey of one particular transformation strategy (a larger conceptual step in a transformational development that can be described at a more abstract level). This strategy for recursive functions entails the derivation of equivalent functions that use in their recursive evaluations the same arguments in an inverted order. This is an important optimization strategy, in particular for tree-like recursive functions, that are often defined in such a way that several function calls need to be evaluated more than once. By evaluating the function in an inverted order, such multiple evaluations are eliminated. /pubs/1990/165/ ''Factorization of the factorial'', illustrates a number of the transformations in chapter 2, and also demonstrates the state of the art in recursion simplification transformations. Directed by a small set of simple and well-known heuristics, a previously unknown algorithm for computing factorials is derived. Also, a similar development is shown leading to a corresponding program for a simple pipeline architecture. /pubs/1991/162/ ''A note on similarity of specifications and reusability of transformational developments'', written together with http://www.informatik.uni-ulm.de/pm/mitarbeiter/helmuth.html , explores the possibilities of reuse of transformational developments. Although it has often been claimed that this could be done fully mechanically, the experience with a number of derivations in this chapter indicates that this claim is somewhat preposterous. Only by describing the transformation steps in a very abstract way (using just natural language) and by considering very general specifications, can the developments be reused. The central concept is similarity, and several definitions of this informal notion are given, each leading to a particular kind of reuse of derivations. Variants of a derivation of linear search lead to several interesting search algorithms, culminating in derivations by reuse of two complicated string matching algorithms. /pubs/1991/161/ ''Intersections of sets and bags of extended substructures - a class of problems'', generalizes the specification of pattern matching. It describes a class of problems that can be viewed as a generalization of pattern matching problems. The essence of pattern matching is considered to be the intersection of a particular set with a bag (multiset) of extended substructures of a structured object. The set contains the patterns, the extended substructures are possible occurrences, extended with labels that mark their positions in the original object. This leads to the first ideas on an (interesting) theory on (extended) substructures. It is shown how the abstract description of this class of problems lends itself to calculation in a BMF style. Also, clearly exhibiting the basic structure of such problems facilitates connecting them with various solution strategies. /pubs/1991/156/ ''Solving a combinatorial problem by transformation of abstract data types'', gives an application of techniques from the area of formal program development in a different area, viz. combinatorics. By describing a given combinatorial problem in terms of abstract data types with equivalences, and transforming those data types, a reduction to a known problem is obtained. Abstract data types proved to be a more suitable specification mechanism in this case than context free grammars, since arbitrary equivalences could be introduced on the data types.

Name: Twittie Senivongse Degree: PhD in Computer Science Evolution Transparency for Distributed Service Types Abstract Large software systems are never static as they exist in an environment that is subject to constant changes in both functionality and technology. Managing this evolution is one of the major challenges in the engineering of large-scale software systems. When a distributed service evolves its interface, other parties in its environment who need to continue using the service will themselves have to evolve correspondingly if the evolved service, although functionally compatible, is not type-compatible with the original one. The autonomous and decentralised nature of distributed components makes such an assumption impractical since the service provider and client systems may not agree on the evolution. It may not even be possible to track down and alter all client programs which are distributed over the network. The best way to tackle this problem is to provide 'evolution transparency' to give the affected components the illusion that the service does not change. This thesis presents an RM-ODP-based model that hides from clients details of changes occuring to distributed service types over time. By allowing type versioning , the model supports program compatibility by enabling a client program of one type version to access a service instance of another functionally compatible type version, even though the versions are not considered compatible by the supporting type system. The model manages a cross-version binding and maintains semantic information which is used to transform the client's invocation to the format recognised by the accessed service object. With a prototype implementation on ANSAware together with an analysis of its mechanism, the evolution transparency support proves useful; clients are given the flexibility to defer their own evolution, and type substitutability is also extended from syntactic to functional compatibility.

No description available.

No description available.

In lazy functional programming modularity is often achieved by using intermediate data structures to combine separate parts of a program. Each intermediate data structure is produced by one part and consumed by another one. Deforestation optimises a functional program by transformation into a program which does not produce such intermediate data structures. In this thesis we present a new method for deforestation, which combines a known method,short cut deforestation, with a new analysis that is based on type inference. Short cut deforestation eliminates an intermediate list by a single, local transformation. In return, short cut deforestation expects both producer and consumer of the intermediate list in a certain form. Whereas the required form of the consumer is generally considered desirable in a well-structured program anyway, the required form of the producer is only a crutch to enable deforestation. Hence only the list-producing functions of the standard libraries were defined in the desired form and short cut deforestation has been confined to compositions of these functions. Here, we present an algorithm which transforms an arbitrary producer into the required form. Starting from the observation that short cut deforestation is based on a parametricity theorem of the second-order typed lambda-calculus, we show how the construction of the required form can be reduced to a type inference problem. Typability for the second-order typed lambda-calculus is undecidable, but we only need to solve a partial type inference problem. For this problem we develop an algorithm based on the well-known Hindley-Milner type inference algorithm. The transformation of a producer often requires inlining of some function definitions. Type inference even indicates which function definitions need to be inlined. However, only limited inlining across module boundaries is practically feasible. Therefore, we extend the previously developed algorithm to split a function definition into a worker definition and a wrapper definition. We only need to inline the small wrapper definition, which transfers all information required for deforestation. The flexibility of type inference allows us to remove intermediate lists which original short cut deforestation cannot remove, even with hand-crafted producers. In contrast to most previous work on deforestation, we give a detailed proof of completeness and semantic correctness of our transformation.

No description available.

Wireless networks allow communication between multiple devices (nodes) without the use of wires. Range in such networks is often limited restricting the use of networks to small offices and homes; however, it is possible to use nodes to forward packets for others thereby extending the communication range of individual nodes. Networks employing such forwarding are called Multi-Hop Ad Hoc Networks (MANETS) Discovering routes in MANETS is a challenging task given that the topology is flat and node addresses reveal nothing about their place in the network. In addition, nodes may move or leave changing the network topology quickly. Existing approaches to discovering locations involve either broadcast dissemination or broadcast route discovery throughout the entire network. The reliance on the use of techniques that use broadcast schemes restricts the size of network that the techniques are applicable to. Routing in large scale ad hoc networks is therefore achieved by the use of geographical forwarding. Each node is required to know its location and that of its neighbours so that it may use this information for forward packets. The next hop chosen is the neighbour that is closest to the destination and a number of techniques are used to handle scenarios here the network has areas void of nodes. Use of such geographical routing techniques requires knowledge of the destination's location. This is provided by location servers and the literature proposes a number of methods of providing them. Unfortunately many of the schemes are limited by using a proportion of the network that increases with size, thereby immediately limiting the scalability. Only one technique is surveyed that provides high scalability but it has a number of limitations in terms of handling node mobility and failure. Ad hoc networks have limited capacity and so the inspiration for a technique to address these shortcomings comes from observations of nature. Birds and ants are able to organise themselves without direct communication through the observation of their environment and their peers. They provide an emergent intelligence based on individual actions rather than group collaboration. This thesis attempts to discover whether software agents can mimic this by creating a group of agents to store location information in a specific location. Instead of requiring central co-ordination, the agents observe one another and make individual decisions to create an emergent intelligence that causes them to resist mobility and node failures. The new technique is called a Self Organising Location Server (SOLS) and is compared against existing approaches to location servers. Most existing techniques do not scale well whereas SOLS uses a new idea of a home location. The use of this idea and the self organising behaviour of the agents that store the information results in significant benefits in performance. SOLS significantly out performs Terminode home region, the only other scalable approach surveyed. SOLS is able to tolerate much higher node failure rates than expected in likely implementations of large scale ad hoc networks. In addition, SOLS successfully mitigates node mobility which is likely to be encountered in an ad hoc network.

No description available.

No description available.

Genetic Programming (GP) is a technique which uses an evolutionary metaphor to automatically generate computer programs. Although GP proclaims to evolve computer programs, historically it has been used to produce code which more closely resembles mathematical formulae than the well structured programs that modern programmers aim to produce. The objective of this thesis is to explore the use of GP in generating high-level imperative programs and to present some novel techniques to progress this aim. A novel set of extensions to Montana’s Strongly Typed Genetic Programming system are presented that provide a mechanism for constraining the structure of program trees. It is demonstrated that these constraints are sufficient to evolve programs with a naturally imperative structure and to support the use of many common high-level imperative language constructs such as loops. Further simple algorithm modifications are made to support additional constructs, such as variable declarations that create new limited-scope variables. Six non-trivial problems, including sorting and the general even parity problem, are used to experimentally compare the performance of the systems and configurations proposed. Software metrics are widely used in the software engineering process for many purposes, but are largely unused in GP. A detailed analysis of evolved programs is presented using seven different metrics, including cyclomatic complexity and Halstead’s program effort. The relationship between these metrics and a program’s fitness and evaluation time is explored. It is discovered that these metrics are poorly suited for application to improve GP performance, but other potential uses are proposed.