作者：
Edwards, JonathanMIT
Comp Sci & Artificial Intelligence LAb Cambridge MA 02139 USA
Schematic tables are a new representation for conditionals. Roughly a cross between decision tables and data flow graphs, they represent computation and decision-making orthogonally. They unify the full range of condi...
详细信息
Schematic tables are a new representation for conditionals. Roughly a cross between decision tables and data flow graphs, they represent computation and decision-making orthogonally. They unify the full range of conditional constructs, from if statements through pattern matching to polymorphic predicate dispatch. Program logic is maintained in a declarative canonical form that enforces completeness and disjointness among choices. Schematic tables can be used either as a code specification/generation tool, or as a self-contained diagrammatic programming language. They give program logic the clarity of truth tables, and support high-level direct manipulation of that logic, avoiding much of the mental computation demanded by conventional conditionals.
Learning logical relations from examples expressed as first order facts has been studied extensively by the Inductive logicprogramming research. Learning with positive-only data may cause over generalization of examp...
详细信息
ISBN:
(纸本)9781424413638
Learning logical relations from examples expressed as first order facts has been studied extensively by the Inductive logicprogramming research. Learning with positive-only data may cause over generalization of examples leading to inconsistent resulting hypotheses. A learning heuristic inferring specific generalization of strings based on unique match sequences is shown to be capable of learning predicates with string arguments. This paper describes an inductive learner based on the idea of specific generalization of strings, and the given clauses are generalized by considering the background knowledge.
作者：
Edwards, JonathanMIT
Comp Sci & Artificial Intelligence LAb Cambridge MA 02139 USA
Schematic tables are a new representation for conditionals. Roughly a cross between decision tables and data flow graphs, they represent computation and decision-making orthogonally. They unify the full range of condi...
详细信息
ISBN:
(纸本)9781595937865
Schematic tables are a new representation for conditionals. Roughly a cross between decision tables and data flow graphs, they represent computation and decision-making orthogonally. They unify the full range of conditional constructs, from if statements through pattern matching to polymorphic predicate dispatch. Program logic is maintained in a declarative canonical form that enforces completeness and disjointness among choices. Schematic tables can be used either as a code specification/generation tool, or as a self-contained diagrammatic programming language. They give program logic the clarity of truth tables, and support high-level direct manipulation of that logic, avoiding much of the mental computation demanded by conventional conditionals.
What we call a "higher-order method" (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design pattern and notif...
详细信息
What we call a "higher-order method" (HOM) is a method that makes mandatory calls to other dynamically-dispatched methods. Examples include template methods as in the Template method design pattern and notify methods in the Observer pattern. HOMs are particularly difficult to reason about, because standard pre- and postcondition specifications cannot describe the mandatory calls. For reasoning about such methods, existing approaches use either higher-order logic or traces, but both are complex and verbose. We describe a simple, concise, and modular approach to specifying HOMs We show how to verify calls to HOMs and their code using first-order verification conditions, in a sound and modular way. Verification of client code that calls HOMs can take advantage of the client's knowledge about the mandatory calls to make strong conclusions. Our verification technique validates and explains traditional documentation practice for HOMs, which typically shows their code. However, specifications do not have to expose all of the code to clients, but only enough to determine how the HOM makes its mandatory calls.
When considering the past or the future, dear apprentice, be mindful of the present. If, while considering the past, you become caught in the past, lost in the past, or enslaved by the past, then you have forgotten yo...
详细信息
When considering the past or the future, dear apprentice, be mindful of the present. If, while considering the past, you become caught in the past, lost in the past, or enslaved by the past, then you have forgotten yourself in the present. If, while considering the future, you become caught in the future, lost in the future, or enslaved by the future, then you have forgotten yourself in the present. Conversely, when considering the past, if you do not become caught, lost, or enslaved by the past, then you have remained mindful of the present. And if, when considering the future, you do not become caught, lost, or enslaved in the future, then you have remained mindful of the present.
A dynamic language promotes ease of use through flexible typing, a focus on high-level programming, and by streamlining the edit-compile-debug cycle. Live languages go beyond dynamic languages with more ease of use fe...
详细信息
A dynamic language promotes ease of use through flexible typing, a focus on high-level programming, and by streamlining the edit-compile-debug cycle. Live languages go beyond dynamic languages with more ease of use features. A live language supports live programming that provides programmers with responsive and continuous feedback about how their edits affect program execution. A live language is also based on high-level constructs such as declarative rules so that programmers can write less code. A live language could also provide programmers with responsive semantic feedback to enable time-saving services such as code completion. This paper describes the design of a textual live language that is based on reactive data-flow values known as signals and dynamic inheritance. Our language, Super-Glue, supports live programming with responsive semantic feedback, which we demonstrate with a working prototype.
Many web-applications can be characterized as "relational". In this paper we introduce and evaluate WebRB, a visual domain-specific language for building such applications. WebRB addresses the limitations of...
详细信息
Many web-applications can be characterized as "relational". In this paper we introduce and evaluate WebRB, a visual domain-specific language for building such applications. WebRB addresses the limitations of the conventional "imperative-embedding" approach typically used to build relational web-applications. We describe the WebRB language, present extended examples of its use, and discuss the WebRB visual editor, libraries, and runtime. We then evaluate WebRB by comparing it to alternative approaches, and demonstrate its effectiveness in building relational web-applications.
A trace monitor observes an execution trace at runtime;when it recognises a specified sequence of events, the monitor runs extra code. In the aspect-oriented programming community, the idea originated as a generalisat...
详细信息
A trace monitor observes an execution trace at runtime;when it recognises a specified sequence of events, the monitor runs extra code. In the aspect-oriented programming community, the idea originated as a generalisation of the advice-trigger mechanism: instead of matching on single events (joinpoints), one matches on a sequence of events. The runtime verification community has been investigating similar mechanisms for a number of years, specifying the event patterns in terms of temporal logic, and applying the monitors to hardware and software. In recent years trace monitors have been adapted for use with mainstream object-oriented languages. In this setting, a crucial feature is to allow the programmer to quantify over groups of related objects when expressing the sequence of events to match. While many language proposals exist for allowing such features, until now no implementation had scalable performance: execution on all but very simple examples was infeasible. This paper rectifies that situation, by identifying two optimisations for generating feasible trace monitors from declarative specifications of the relevant event pattern. We restrict ourselves to optimisations that do not have a significant impact on compile-time: they only analyse the event pattern, and not the monitored code itself. The first optimisation is an important improvement over an earlier proposal in [2] to avoid space leaks. The second optimisation is a form of indexing for partial matches. Such indexing needs to be very carefully designed to avoid introducing new space leaks, and the resulting data structure is highly non-trivial.
A combinational module for scattered pattern matching tests whether the digits of a given pattern occur in the proper order and multiplicity within a given search string. We present a unifying high-level synthesis of ...
详细信息
We present UMLtoCSP, a tool for the formal verification of UML/OCL models. Given a UML class diagram annotated with OCL constraints, UMLtoCSP is able to automatically check several correctness properties, such as the ...
详细信息
ISBN:
(纸本)9781595938824
We present UMLtoCSP, a tool for the formal verification of UML/OCL models. Given a UML class diagram annotated with OCL constraints, UMLtoCSP is able to automatically check several correctness properties, such as the strong and weak satisfiability of the model or the lack of redundant constraints. The tool uses Constraint logicprogramming as the underlying formalism and the constraint solver ECLiPSe as the verification engine.
暂无评论