作者:
Kim, Ju-WhanNam, Tek-JinCIDR Lab
Department of Industrial Design KAIST 291 Daehak-ro Yuseong-gu Daejeon 305-701 Korea Republic of
Prototyping of gestural interactions in the early phase of design is one of the most challenging tasks for designers without advanced programming skills. Relating users' input from gesture-based sensor values requ...
详细信息
This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees ...
详细信息
This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-driven synthesis algorithm for HDT transformations. Our central insight is to reduce the problem of synthesizing tree transformers to the synthesis of list transformations that are applied to the paths of the tree. The synthesis problem over lists is solved using a new algorithm that combines SMT solving and decision tree learning. We have implemented our technique in a system called HADES and show that HADES can automatically synthesize a variety of interesting transformations collected from online forums.
programming error messages have proven to be notoriously problematic for novices who are learning to program. Although recent efforts have focused on improving message wording, these have been criticized for attemptin...
详细信息
ISBN:
(纸本)9781450389761
programming error messages have proven to be notoriously problematic for novices who are learning to program. Although recent efforts have focused on improving message wording, these have been criticized for attempting to improve usability without first understanding and addressing readability. To date, there has been no research dedicated to the readability of programming error messages and how this could be assessed. In this paper we examine human-based assessments of programming error message readability and make two important contributions. First, we conduct an experiment using the top twenty most-frequent error messages in three popular programminglanguages (Python, Java, and C), revealing that human notions of readability are highly subjective and dependent on both programming experience and language familiarity. Both novices and experts agreed more about which messages are more readable, but disagreed more about which messages are not readable. Second, we leverage the data from this experiment to uncover several key factors that seem to affect message readability: message length, message tone, and use of jargon. We discuss how these factors can help guide future efforts to design a readability metric for programming error messages.
Access to the variety of resources offered by computer networks is often complicated by the diversity of interfaces and protocols encountered. To overcome this diversity, a command-and-response language interface to a...
详细信息
ISBN:
(纸本)0818608420
Access to the variety of resources offered by computer networks is often complicated by the diversity of interfaces and protocols encountered. To overcome this diversity, a command-and-response language interface to a network of heterogeneous systems is proposed. A brief account of previous work in command languages and system interfaces motivates the study of a prototype of the proposed interface. The design, implementation, and lessons learned through the successful realization of the prototype are presented.
CST is a programminglanguage based on Smalltalk-802 that supports concurrency using locks, asynchronous messages, and distributed objects. In this paper, we describe CST: the language and its implementation. Example ...
ISBN:
(纸本)9780897913065
CST is a programminglanguage based on Smalltalk-802 that supports concurrency using locks, asynchronous messages, and distributed objects. In this paper, we describe CST: the language and its implementation. Example programs and initial programming experience with CST are described. Our implementation of CST generates native code for the J-machine, a fine-grained concurrent computer. Some compiler optimizations developed in conjunction with that implementation are also described.
We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with t...
详细信息
We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.
Previous attempts at garbage collection in uncooperative environments have generally used conservative or mostly-conservative approaches. We describe a technique for doing fully type-accurate garbage collection in an ...
详细信息
Previous attempts at garbage collection in uncooperative environments have generally used conservative or mostly-conservative approaches. We describe a technique for doing fully type-accurate garbage collection in an uncooperative environment, using a "shadow stack" to link structs of pointer-containing variables, together with the data or code needed to trace them. We have implemented this in the Mercury compiler, which generates C code, and present preliminary performance data on the overheads of this technique. We also show how this technique can be extended to handle multithreaded applications.
Building distributed systems is particularly difficult because of the asynchronous, heterogeneous, and failure-prone environment where these systems must run. Tools for building distributed systems must strike a compr...
详细信息
Building distributed systems is particularly difficult because of the asynchronous, heterogeneous, and failure-prone environment where these systems must run. Tools for building distributed systems must strike a compromise between reducing programmer effort and increasing system efficiency. We present Mace, a C++ language extension and source-to-source compiler that translates a concise but expressive distributed system specification into a C++ implementation. Mace overcomes the limitations of low-level languages by providing a unified framework for networking and event handling, and the limitations of high-level languages by allowing programmers to write program components in a controlled and structured manner in C++. By imposing structure and restrictions on how applications can be written, Mace supports debugging at a higher level, including support for efficient model checking and causal-path debugging. Because Mace programs compile to C++, programmers can use existing C++ tools, including optimizers, profilers, and debuggers to analyze their systems.
This paper discusses the implementation model for supporting Ada 95 controlled types in the GNAT compiler [1]. After reviewing the semantics of controlled types, we outline the associated implementation problems and d...
详细信息
We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock tha...
详细信息
We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential shape analysis on each thread. We show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. Based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from Windows device drivers.
暂无评论