This thesis describes the design and implementation of the IPE, an interactive proof editor for first-order intuitionistic predicate calculus, developed at the University of Edinburgh during 1983-1986, by the author together with John Cartmell and Tatsuya Hagino. The IPE uses an attribute grammar to maintain the state of its proof tree as a context-sensitive structure. The interface allows free movement through the proof structure, and encourages a "proof-byexperimentation" approach, since no proof step is irrevocable. We describe how the IPE's proof rules can be derived from natural deduction rules for first-order intuitionistic logic, how these proof rules are encoded as an attribute grammar, and how the interface is constructed on top of the grammar. Further facilities for the manipulation of the IPE's proof structures are presented, including a notion of IPE-tactic for their automatic construction. We also describe an extension of the IPE to enable the construction and use of simply-structured collections of axioms and results, the main provision here being an interactive "theory browser" which looks for facts which match a selected problem.

Automated planning is a task to find a sequence of actions leading from an initial state to a desired goal state. There is a lot of formal models for planning problems modeling. The class of hierarchical formal models is one of them. In this thesis we will propose a hierarchical model, called GramPlan, based on attribute grammars. We will present some methods to reduce classical STRIPS formalism to GramPlan and we will prove the correctness of this reduction. Also we will present reduction of the FlowOpt workflow model to GramPlan and we will prove it's correctness. We will desing a couple of verification methods for attribute grammars and we will show these methods are equivalent. Powered by TCPDF (www.tcpdf.org)

Dieser Bericht präsentiert RACR-NET, eine Schnittstelle der Referenzattributgrammatik-gesteuerten Graphersetzungsbibliothek RACR für C#. RACR-NET ermöglicht die Nutzung der deklarativen, dynamischen Sprachspezifikations-, Instanziierungs- und Auswertungsmeachanismen der RACR Scheme-Bibliothek in der objektorientierten Programmierung. Dies umfasst insbesondere die automatische inkrementelle Auswertung attributbasierter semantischer Analysen und somit das automatische Cachen parametrisierter Funktionsmethoden. Graphersetzungen entsprechen hierbei Zustandsänderungen von Objektinstanzen und der Invalidierung abgeleiteter Berechnungen. Schwerpunkt dieses Berichts ist die objektorientierte Programmierschnittstelle von RACR-NET, dessen praktische Anwendung und Implementierung. Der Bericht ist ein Referenzhandbuch für RACR-NET Anwender und Entwickler.

Uma interface com o usuário é composta por duas "vias" de comunicação, uma que vai do usuário até o sistema e outra que vai do sistema até o usuário. Cada uma destas "vias" possui um formalismo que define a comunicação associado. Neste trabalho, estes formalismos são descritos com uma gramática de atributos. Esta gramática foi expandida de forma a permitir a definição dos elementos que compõe a interface do usuário, e da estrutura que irá controlar a seqüência de execução das tarefas oferecidas pelos sistemas de aplicação. Ao longo do trabalho são discutidas algumas técnicas de descrição do formalismo de comunicação entre interface e sistema, são abordados os estilos de interação e apresentada as expansões aplicadas sobre gramáticas de atributos. Um exemplo auxilia a compreensão do uso da linguagem proposta, e um protótipo permite a validação das definições. / A user interface is composed by two "ways" of communication, one from the user to the system and the other linking the system to the user. Each of these "ways" has it's own mechanism. In this work, these mechanisms are described through an attribute grammar. This grammar has been expanded to allow the definition of the structure of the interface elements and the control of the execution of the tasks that the application system implements. Through this work, technics that describe the communication between the interface and the system, interaction styles and the extensions made on attribute grammar are discussed. An example is given to explain the use of the proposed mechanism and a prototype validates ideas discussed.

Uma interface com o usuário é composta por duas "vias" de comunicação, uma que vai do usuário até o sistema e outra que vai do sistema até o usuário. Cada uma destas "vias" possui um formalismo que define a comunicação associado. Neste trabalho, estes formalismos são descritos com uma gramática de atributos. Esta gramática foi expandida de forma a permitir a definição dos elementos que compõe a interface do usuário, e da estrutura que irá controlar a seqüência de execução das tarefas oferecidas pelos sistemas de aplicação. Ao longo do trabalho são discutidas algumas técnicas de descrição do formalismo de comunicação entre interface e sistema, são abordados os estilos de interação e apresentada as expansões aplicadas sobre gramáticas de atributos. Um exemplo auxilia a compreensão do uso da linguagem proposta, e um protótipo permite a validação das definições. / A user interface is composed by two "ways" of communication, one from the user to the system and the other linking the system to the user. Each of these "ways" has it's own mechanism. In this work, these mechanisms are described through an attribute grammar. This grammar has been expanded to allow the definition of the structure of the interface elements and the control of the execution of the tasks that the application system implements. Through this work, technics that describe the communication between the interface and the system, interaction styles and the extensions made on attribute grammar are discussed. An example is given to explain the use of the proposed mechanism and a prototype validates ideas discussed.

Uma interface com o usuário é composta por duas "vias" de comunicação, uma que vai do usuário até o sistema e outra que vai do sistema até o usuário. Cada uma destas "vias" possui um formalismo que define a comunicação associado. Neste trabalho, estes formalismos são descritos com uma gramática de atributos. Esta gramática foi expandida de forma a permitir a definição dos elementos que compõe a interface do usuário, e da estrutura que irá controlar a seqüência de execução das tarefas oferecidas pelos sistemas de aplicação. Ao longo do trabalho são discutidas algumas técnicas de descrição do formalismo de comunicação entre interface e sistema, são abordados os estilos de interação e apresentada as expansões aplicadas sobre gramáticas de atributos. Um exemplo auxilia a compreensão do uso da linguagem proposta, e um protótipo permite a validação das definições. / A user interface is composed by two "ways" of communication, one from the user to the system and the other linking the system to the user. Each of these "ways" has it's own mechanism. In this work, these mechanisms are described through an attribute grammar. This grammar has been expanded to allow the definition of the structure of the interface elements and the control of the execution of the tasks that the application system implements. Through this work, technics that describe the communication between the interface and the system, interaction styles and the extensions made on attribute grammar are discussed. An example is given to explain the use of the proposed mechanism and a prototype validates ideas discussed.

Over the past 10 years, several synthetic biology research groups have proposed tools and domain-specific languages to help with the design of artificial DNA molecules. Community standards for exchanging data between these tools, such as the Synthetic Biology Open Language (SBOL), have been developed. It is increasingly important to be able to perform in silico simulation before the time and cost consuming wet lab realization of the constructs, which, as technology advances, also become in themselves more complex. By extending the concept of describing genetic expression as a language, we propose to model relations between genotype and phenotype using formal language theory. We use attribute grammars (AGs) to extract context-dependent information from genetic constructs and compile them into mathematical models, possibly giving clues about their phenotypes. They may be used as a backbone for biological Domain-Specific Languages (DSLs) and we developed a methodology to design these AG based DSLs. We gave examples of languages in the field of synthetic biology to model genetic regulatory networks with Ordinary Differential Equations (ODEs) based on various rate laws or with discrete boolean network models. We implemented a demonstration of these concepts in GenoCAD, a Computer Assisted Design (CAD) software for synthetic biology. GenoCAD guides users from design to simulation. Users can either design constructs with the attribute grammars provided or define their own project-specific languages. Outputting the mathematical model of a genetic construct is performed by DNA compilation based on the attribute grammar specified; the design of new languages by users necessitated the generation on-the-fly of such attribute grammar based DNA compilers. We also considered the impact of our research and its potential dual-use issues. Indeed, after the design exploration is performed in silico, the next logical step is to synthesize the designed construct's DNA molecule to build the construct in vivo. We implemented an algorithm to identify sequences of concern of any length that are specific to Select Agents and Toxins, helping to ensure safer use of our methods. / Ph. D.

In recent years, the development of multi-core CPUs and GPUs with many cores has taken precedence over an increase in clock frequency. Therefore, writing parallel programs for multi-core and many-core systems becomes increasingly important. Due to the lack of inherently parallel language features in most programming languages, today many programs are written sequentially and then enhanced with special pragmas or framework calls hinting parallelizable parts of code. This hints are then used to modify and extend the code with parallel constructs in a preprocessing step. If it is crucial to optimize the run time of a program, the code generated by this step has to be inspected an manually tuned. To keep the original and the transformed code artifacts synchronized, an editor with a round-trip engineering (RTE) system can be used. RTE propagates changes made in the source artifacts to the generated artifacts and vice versa. One tool that can be used to expand pragmas to parallelized source code is the invasive software composition framework SkAT. SkAT-based tools use reference attribute grammars (RAGs) to compose code fragments according to a composition program written in Java. To facilitate the creation of SkAT-based tools, a minimal composition system framework SkAT/Minimal on to of the SkAT core contains mechanisms to enable the incremental building of such tools. The principle of island parsing is employed to be able to express just as much of a language as is necessary for composition. In this work, composition systems based on SkAT/Minimal are targeted. The task is split into two parts: first, approaches for RTE are analyzed and a concept for a RTE system is created. The focus lies on the analysis of features and requirements of existing RTE approaches and a thorough investigation of all relevant steps required to implement such a system for SkAT/Minimal. The second part of the task is the creation and evaluation of a prototypical implementation of the system.

This report presents RACR, a reference attribute grammar library for the programming language Scheme. RACR supports incremental attribute evaluation in the presence of abstract syntax tree rewrites. It provides a set of functions that can be used to specify abstract syntax tree schemes and their attribution and construct respective trees, query their attributes and node information and annotate and rewrite them. Thereby, both, reference attribute grammars and rewriting, are seamlessly integrated, such that rewrites can reuse attributes and attribute values change depending on performed rewrites – a technique we call Reference Attribute Grammar Controlled Rewriting. To reevaluate attributes influenced by abstract syntax tree rewrites, a demand-driven, incremental evaluation strategy, which incorporates the actual execution paths selected at runtime for control-flows within attribute equations, is used. To realize this strategy, a dynamic attribute dependency graph is constructed throughout attribute evaluation – a technique we call Dynamic Attribute Dependency Analyses. The report illustrates RACR's motivation, features, instantiation and usage. In particular its application programming interface is documented and exemplified. The report is a reference manual for RACR developers. Further, it presents RACR’s complete implementation and therefore provides a good foundation for readers interested into the details of reference attribute grammar controlled rewriting and dynamic attribute dependency analyses.

In recent years, the development of multi-core CPUs and GPUs with many cores has taken precedence over an increase in clock frequency. Therefore, writing parallel programs for multi-core and many-core systems becomes increasingly important. Due to the lack of inherently parallel language features in most programming languages, today many programs are written sequentially and then enhanced with special pragmas or framework calls hinting parallelizable parts of code. This hints are then used to modify and extend the code with parallel constructs in a preprocessing step. If it is crucial to optimize the run time of a program, the code generated by this step has to be inspected an manually tuned. To keep the original and the transformed code artifacts synchronized, an editor with a round-trip engineering (RTE) system can be used. RTE propagates changes made in the source artifacts to the generated artifacts and vice versa. One tool that can be used to expand pragmas to parallelized source code is the invasive software composition framework SkAT. SkAT-based tools use reference attribute grammars (RAGs) to compose code fragments according to a composition program written in Java. To facilitate the creation of SkAT-based tools, a minimal composition system framework SkAT/Minimal on to of the SkAT core contains mechanisms to enable the incremental building of such tools. The principle of island parsing is employed to be able to express just as much of a language as is necessary for composition. In this work, composition systems based on SkAT/Minimal are targeted. The task is split into two parts: first, approaches for RTE are analyzed and a concept for a RTE system is created. The focus lies on the analysis of features and requirements of existing RTE approaches and a thorough investigation of all relevant steps required to implement such a system for SkAT/Minimal. The second part of the task is the creation and evaluation of a prototypical implementation of the system.:1 Introduction 1 1.1 Motivation 1 1.2 Scope 2 1.3 Contributions 2 1.4 Organization 2 2 Background 5 2.1 Fundamentals 6 2.1.1 Syntax Trees 6 2.1.2 Parsing and Unparsing 6 2.2 Attribute Grammars 9 2.2.1 Reference Attribute Grammars 10 2.2.2 Reference Attribute Grammars in SkAT 10 2.3 Composition Systems 12 2.3.1 Software Composition Systems 13 2.3.2 Invasive Software Composition 13 2.3.3 SkAT 15 2.3.4 Template-based Code Generation 16 2.4 Round-trip Engineering 17 2.4.1 Motivation For Round-trip Engineering 17 2.4.2 Concepts of RTE 18 3 Analysis of RTE Approaches 19 3.1 Automatic Round-trip Engineering 19 3.2 RTE In Aspect Weaving Systems 21 3.2.1 CST Graftings 21 3.2.2 Update Propagation in Aspect Weaving Systems 22 3.3 RTE in Invasive Software Composition Systems 23 3.3.1 Tracing Composition Program Execution 23 3.3.2 Backpropagation of Changes 24 3.3.3 Implementation in the Reuseware Framework 26 3.4 Managing Fragments in RTE 27 3.5 Evaluation of RTE Approaches 28 4 Tracing in SkAT 31 4.1 Requirements 31 4.1.1 Objectives 32 4.1.2 Functional and Nonfunctional Requirements 32 4.2 Concept 33 4.3 Implementation 34 5 Building an RTE-editor Prototype 37 5.1 Prerequisites 37 5.2 Requirements 39 5.3 Concept 40 5.3.1 AST Interface 41 5.3.2 Composer Interface 41 5.3.3 Generating the Output 41 5.3.4 The Prototype Skeleton 42 5.4 Implementation 43 6 Designing an RTE-editor 49 6.1 Replay 50 6.2 AST Modifications 50 6.2.1 Modification Types 51 6.2.2 Detecting Modification Types 52 6.3 Origin Inference 53 6.3.1 Inference for Updated Elements 53 6.3.2 Inference for Deleted Elements 54 6.3.3 Inference for Inserted Elements 54 6.4 Gap Edit Problem 54 6.4.1 Inference in SkAT 57 6.4.2 Multiple Source Fragments 57 6.5 Applying Modifications 58 6.5.1 Propagating Terminal Updates 60 6.5.2 Propagating Non-terminal Updates 61 6.5.3 Propagating Deletions 62 6.5.4 Propagating Insertions 62 6.5.5 Propagating Composed Modifications 62 6.6 Adapting SkAT Composition Programs 63 7 Evaluation and Outlook on Future Works 65 7.1 Fragment Versioning 65 7.2 Composition Program DSL 66 7.3 Structured Editors 68 7.4 SkAT RTE System 68 Appendices 71 List of Figures 73 List of Listings 75 List of Abbreviations 77 Bibliography 79 CD Content 83