The thesis presents a type system for a substantial fragment of XML query language Xcerpt. The system is descriptive; the types associated with Xcerpt constructs are sets of data terms and approximate the semantics of the constructs. A formalism of Type Definitions, related to XML schema languages, is adopted to specify such sets. The type system is presented as typing rules which provide a basis for type inference and type checking algorithms, used in a prototype implementation. Correctness of the type system wrt. the formal semantics of Xcerpt is proved and exactness of the result types inferred by the system is discussed. The usefulness of the approach is illustrated by example runs of the prototype on Xcerpt programs. Given a non-recursive Xcerpt program and types of data to be queried, the type system is able to infer a type of results of the program. If additionally a type specification of program results is given, the system is able to prove type correctness of a (possibly recursive) program. Type correctness means that the program produces results of the given type whenever it is applied to data of the given type. Non existence of a correctness proof suggests that the program may be incorrect. Under certain conditions (on the program and on the type specification), the program is actually incorrect whenever the proof attempt fails. / <p>Report code: LiU-TEK-LIC-2006:9</p>

This dissertation addresses two important problems in reusing intellectual properties (IPs) in the form of reusable design or verification components. The first problem is associated with fast and effective integration of reusable design components into a System-on-chip (SoC), so faster design turn-around time can be achieved, leading to faster time-to-market. The second problem has the same goals of faster product design cycle, but emphasizes on verification model reuse, rather than design component reuse. It specifically addresses reuse of reusable verification IPs to enable a "write once, use many times" verification strategy. This dissertation is accordingly divided into part I and part II which are related but describe the two problems and our solutions to them. These two related but distinctive problems faced by system design companies have been tackled through a unique approach which hither-to-fore only have been used in the software engineering domain. This approach is called metamodeling, which allows creating customized meta-language to describe the syntax and semantics for a modeling domain. It provides a way to create, transform and analyze domain specific languages, which are themselves described by metamodels, and the transformation and processing of models in such languages are also described by metamodels. This makes machine based interpretation and translation from these models an easier and formal task. In part I, we consider the problem of rapid system-level model integration of existing reusable components such that (i) the required architecture of the SoC can be expressed formally, (ii) automatic selection of components from an IP library to match the need of the system being integrated can be done, (iii) integrability of the components is provable, or checkable automatically, and (iv) structural and behavioral type systems for each component can be utilized through inferencing and matching techniques to ensure their compatibility. Our solutions include a component composition language, algorithms for component selection, type matching and inferencing algorithms, temporal property based behavioral typing, and finally a software system on top of an existing metamodeling environment. In part II, we use the same metamodeling environment to create a framework for modeling generative verification IPs. Our main contributions relate to INTEL's microprocessor verification environment, and our solution spans various abstraction levels (System, architectural, and microarchitecture) to perform verification. We provide a unified language that can be used to model verification IPs at all abstraction levels, and verification collaterals such as testbenches, simulators, and coverage monitors can be generated from these models, thereby enhancing reuse in verification. / Ph. D.

AspectFun是一個實驗性的剖面導向函式語言，它主要的特色在於具備能以靜態織入方式實現的多型剖面、高階剖面以及依據動態流程觸發的剖面。 本論文提出一個AspectFun語言的編譯器，其編譯過程分為四個主要步驟：語法結構轉換、剖面織入、剖面轉函式與整合動態流程判斷資訊。其中剖面織入是最複雜的步驟，必須仰賴可能是多型的型態資訊，選取適當的剖面整合到程式指定的切點處。這部份的織入工作，我們的編譯器是依據一套以靜態型態推論規則發展而來的轉譯規則，先將AspectFun程式轉譯成的剖面與函式整合在一起的中介格式，再翻譯為可執行的Haskell程式來完成。此外，本系統也是使用Haskell程式語言開發，並採用Monad技術將系統模組化，以達到最佳的可維護性、擴充性與閱讀性。本論文介紹系統的實作面，解釋AspectFun系統架構、語法、原理和實作帶來的貢獻以及限制。 / AspectFun is an experimental aspect-oriented functional language. Its main features include polymorphic aspects via static weaving, second-order aspects and control-flow triggered aspects. This thesis presents a type-directed compiler for AspectFun. Our compilation processes consists of four major steps: syntax de-sugaring, aspect weaving, translating aspects to normal functions, and integrating control flow information. The most complicated one is aspect weaving. Due to polymorphism in aspects, it is completely dependent on type information inferable from the aspects and the context they are used. We base our weaving step on a set of type-directed translation rules. In particular, the weaving step is further divided into two stages. First, an AspectFun program is translated into an intermediate form in which all aspects applicable at a context are chained together and integrated with context. Second, all aspects are translated into ordinary functions and any chain of aspects are transformed to a sequence of function calls in as an executable Haskell program. Moreover, the complier itself is implemented in Haskell. We fully utilize the monad mechanism of Haskell to modularize our compiler and achieve the goals of good maintainability, extensibility and readability.

Highly dynamic languages like Smalltalk do not have much static type information immediately available before the program runs. Static types can still be inferred by analysis tools, but historically, such analysis is only effective on smaller programs of at most a few tens of thousands of lines of code. This dissertation presents a new type inference algorithm, DDP, that is effective on larger programs with hundreds of thousands of lines of code. The approach of the algorithm borrows from the field of knowledge-based systems: it is a demand-driven algorithm that sometimes prunes subgoals. The algorithm is formally described, proven correct, and implemented. Experimental results show that the inferred types are usefully precise. A complete program understanding application, Chuck, has been developed that uses DDP type inferences. This work contributes the DDP algorithm itself, the most thorough semantics of Smalltalk to date, a new general approach for analysis algorithms, and experimental analysis of DDP including determination of useful parameter settings. It also contributes an implementation of DDP, a general analysis framework for Smalltalk, and a complete end-user application that uses DDP.