No description available.

In this thesis we will be concerned with a particular type of architecture for reasoning systems, known as meta-level architectures. After presenting the arguments for such architectures (chapter 1), we discuss a number of systems in the literature that provide an explicit meta-level architecture (chapter 2), and these systems are compared on the basis of a number of distinguishing characteristics. This leads to a classification of meta-level architectures (chapter 3). Within this classification we compare the different types of architectures, and argue that one of these types, called bilingual meta-level inference systems, has a number of advantages over the other types. We study the general structure of bilingual meta-level inference architectures (chapter 4), and we discuss the details of a system that we implemented which has this architecture (chapter 5). One of the problems that this type of system suffers from is the overhead that is incurred by the meta-level effort. We give a theoretical model of this problem, and we perform measurements which show that this problem is indeed a significant one (chapter 6). Chapter 7 discusses partial evaluation, the main technique available in the literature to reduce the meta-level overhead. This technique, although useful, suffers from a number of serious problems. We propose two further techniques, partial reflection and many-sorted logic (chapters 8 and 9), which can be used to reduce the problem of meta-level overhead without suffering from these problems.

Lors d'un développement logiciel, et plus particulièrement d'un développement d'applications embarquées avioniques, les activités de vérification représentent un coût élevé. Une des pistes prometteuses pour la réduction de ces coûts est l'utilisation de méthodes formelles. Ces méthodes s'appuient sur des fondements mathématiques et permettent d'effectuer des tâches de vérification à forte valeur ajoutée au cours du développement. Les méthodes formelles sont déjà utilisées dans l'industrie. Cependant, leur difficulté d'appréhension et la nécessité d'expertise pour leur mise en pratique sont un frein à leur utilisation massive. Parallèlement au problème des coûts liés à la vérification logicielle, vient se greffer la complexification des logiciels et du contexte de développement. L'Ingénierie Dirigée par les Modèles (IDM) permet de faire face à ces difficultés en proposant des modèles, ainsi que des activités pour en tirer profit. Le but des travaux présentés dans cette thèse est d'établir un lien entre les méthodes formelles et l'IDM afin de proposer à des utilisateurs non experts une approche de vérification formelle et automatique de programmes susceptible d'améliorer les processus de vérification actuels. Nous proposons de générer automatiquement sur le code source des annotations correspondant aux propriétés comportementales attendues du logiciel, et ce, à partir de son modèle de conception. Ces annotations peuvent ensuite être vérifiées par des outils de preuve déductive, afin de s'assurer que le comportement du code est conforme au modèle. Cette thèse CIFRE s'inscrit dans le cadre industriel d'Atos. Il est donc nécessaire de prendre en compte le contexte technique qui s'y rattache. Ainsi, nous utilisons le standard UML pour la modélisation, le langage C pour l'implémentation et l'outil Frama-C pour la preuve du code. Nous tenons également compte des contraintes du domaine du logiciel avionique dans lequel Atos est impliqué et notamment les contraintes liées à la certification. Les contributions de cette thèse sont la définition d'un sous-ensemble des machines à états UML dédié à la conception comportementale de logiciel avionique et conforme aux pratiques industrielles existantes, la définition d'un patron d'implémentation C, la définition de patrons de génération des propriétés comportementales sur le code à partir du modèle et enfin l'implémentation de l'approche dans un prototype compatible avec l'environnement de travail des utilisateurs potentiels en lien avec Atos. L'approche proposée est finalement évaluée par rapport à l'objectif de départ, par rapport aux attentes de la communauté du génie logiciel et par rapport aux travaux connexes.

Since programs are written in many languages and design documents are not maintained (if they ever existed), there is a need to extract the design and other information that the programs represent. To do this without writing a separate program for each language, a common representation of the symbol table and parse tree would be required.The purpose of the parse tree and symbol table will not be to generate object code but to provide a platform for analysis tools. In this way the tool designer develops only one version instead of separate versions for each language. The generic symbol table and generic parse tree may not be as detailed as those same structures in a specific compiler but the parse tree must include all structures for imperative languages. / Department of Computer Science

This study implemented an experimental introductory CS course for non-CS majors focusing on two pedagogic factors: 1) the use of a visual blocks programming language known as App Inventor for Android (AIA) and 2) the adoption of SBL as the main teaching methodology. Participants included 30 undergraduates enrolled in two introductory CS courses; the experimental course (CS116) and a traditional lecture oriented CS course. The Motivated Strategies for Learning Questionnaire (MSLQ) was implemented in both courses at several stages. Statistically significant differences were found in the Control of Learning Beliefs, Help Seeking, and Intrinsic Motivation scales, were CS116’s participants scored higher rates. In CS116, entry and exit interviews were conducted as well as a mind maps analysis. Their results showed a positive response to the pedagogic factors, positive attitudes towards CS, and an improvement in the understanding of CS. The majority of participants did very well and showed creativity with not one student failing the course. They found the experimental course to cultivate collaboration, creativity, and motivation to learn. The experimental approach was found have a positive effect on students’ motivation, achievement, and attitude towards CS. / Department of Computer Science

Time has always been a parameter to minimize in computer programs. It is the stuff that measures our patience as we wait for results. However, for a number of problems, we seek to model a notion of time that can be used to regulate the rate at which things happen. Audio processing is one of these problem areas. It has seen the development of many languages and environments with each one having to adopt a suitable notion of time to support such things as accurately timed events and interactivity while remaining efficient. In this thesis I will investigate the forms of simulated time within audio processing environments. To this end, I will define a set of properties that shape the construction of a model of time simulated on a computer. We can see these properties in the design of languages and environments that support the scheduling of events. With that in mind, I will provide a survey of the use of time in a number of computer languages and paradigms. The reach of this survey will not be exhaustive but will instead try to investigate different ideas with an emphasis on languages for audio processing. I will also put some of these ideas into practice by presenting two separate audio processing frameworks each with their own model of time.

Several tools have been developed for the authoring of intensional (context-sensitive) documents; for example. IHTML (Intensional HTML), IML (Intensional Markup Language). and ISE (Intensional Sequential Evaluator). However, at present, it is still very difficult to author intensional markup documents. To ease this difficulty. this thesis presents two new intensional authoring tools. IMP (Intensional Macro Processor) and ICC (Intensional C Compiler). IMP is a powerful yet easy to use macro processor embedded with a JavaScript engine. ICC in turn is an intensional extension to ANSI C. Several applications of IMP and ICC such as WIMPAS. intensional spreadsheet and CGI programming in ICC are discussed in this thesis to illustrate how IMP and ICC facilitate intensional authoring.

In an orthogonally persistent programming system, data is treated in a manner independent of its persistence. This gives simpler semantics, allows the programmer to ignore details of long-term data storage and enables type checking protection mechanisms to operate over the entire lifetime of the data. The ultimate goal of persistent programming language research is to reduce the costs of producing software. The work presented in this thesis seeks to improve programmer productivity in the following ways: • by reducing the amount of code that has to be written to construct an application; • by increasing the reliability of the code written; and • by improving the programmer’s understanding of the persistent environment in which applications are constructed. Two programming techniques that may be used to pursue these goals in a persistent environment are type-safe linguistic reflection and hyper-programming. The first provides a mechanism by which the programmer can write generators that, when executed, produce new program representations. This allows the specification of programs that are highly generic yet depend in non-trivial ways on the types of the data on which they operate. Genericity promotes software reuse which in turn reduces the amount of new code that has to be written. Hyper-programming allows a source program to contain links to data items in the persistent store. This improves program reliability by allowing certain program checking to be performed earlier than is otherwise possible. It also reduces the amount of code written by permitting direct links to data in the place of textual descriptions. Both techniques contribute to the understanding of the persistent environment through supporting the implementation of store browsing tools and allowing source representations to be associated with all executable programs in the persistent store. This thesis describes in detail the structure of type-safe linguistic reflection and hyper-programming, their benefits in the persistent context, and a suite of programming tools that support reflective programming and hyper-programming. These tools may be used in conjunction to allow reflection over hyper-program representations. The implementation of the tools is described.

Parallel processing can provide the huge computational resources that are required to solve todays grand challenges, at a fraction of the cost of developing sequential machines of equal power. However, even with such attractive benefits the parallel software industry is still very small compared to its sequential counterpart. This has been attributed to the lack of an accepted parallel model of computation, therefore leading to software which is architecture dependent with unpredictable performance. The Bulk Synchronous Parallel (BSP) model provides a solution to these problems and can be compared to the Von Neumann model of sequential computation. In this thesis we investigate the issues involved in providing a modular programming environment based on the BSP model. Using our results we present Opal, a BSP programming language that has been designed for parallel programming-in-the-large. While other BSP languages and libraries have been developed, none of them provide support for libraries of parallel algorithms. A library mechanism must be introduced into BSP without destroying the existing cost model. We examine such issues and show that the active library mechanism of Opal leads to algorithms which still have predictable performance. If algorithms are to retain acceptable levels of performance across a range of machines then they must be able to adapt to the architecture that they are executing on. Such adaptive algorithms require support from the programming language, an issue that has been addressed in Opal. To demonstrate the Opal language and its modular features we present a number of example algorithms. Using an Opal compiler that has been developed we show that we can accurately predict the performance of these algorithms. The thesis concludes that by using Opal it is possible to program the BSP model in a modular fashion that follows good software engineering principles. This enables large scale parallel software to be developed that is architecture independent, has predictable performance and is adaptive to the target architecture.

The problems of semantics and translation for concurrent programming languages are studied in this thesis. A structural operational approach is introduced to specify the semantics of parallelism and communication. Using this approach, semantics for the concurrent programming languages CSP (Hoare's Communicating Sequential Processes), multitasking and exception handling in Ada, Brinch-Hansen's Edison and CCS (Milner's Calculus of Communicating Systems) are defined and some of their properties are studied. An operational translation theory for concurrent programming languages is given. The concept of the correctness of a translation is formalised, the problem of composing transitions is studied and a composition theorem is proved. A set of sufficient conditions for proving the correctness of a translation is given. A syntax-directed translation from CSP to CCS is given and proved correct. Through this example the proof techniques of this approach is demonstrated. Finally, as an application of operational semantics and translation, a proposal for implementing multitasking in Ada is given via a two-step syntax-directed translation.