Tracechecks are a formalism based on linear temporal logic (LTL) with variable bindings and pointcuts of the aspect-oriented language AspectJ for the purpose of verification. We demonstrate how trace-checks can be use...
详细信息
ISBN:
(纸本)3540376577
Tracechecks are a formalism based on linear temporal logic (LTL) with variable bindings and pointcuts of the aspect-oriented language AspectJ for the purpose of verification. We demonstrate how trace-checks can be used to model temporal assertions. these assertions reason about the dynamic control flow of an application. they can be used to formally define the semantic interface of classes. We explain in detail how we make use of AspectJ pointcuts to derive a formal model of an existing application and use LTL to express temporal assertions over this model. We developed a reference implementation withthe abc compiler showing that the tool can be applied in practice and is memory-efficient. In addition we show how trace-checks can be deployed as Java5 annotations, yielding a system which is fully compliant with any Java compiler and hiding any peculiarities of aspect-oriented programming from the user. through annotations, the tracecheck specifications become a semantic part of an interface. Consumers of such a component can then take advantage of the contained annotations by applying our tool and have their use of this component automatically checked at runtime for compliance withthe intent of the component provider.
We present a spreadsheet approach to simplifying the process of managing, programming, and interacting with sensor networks and visualizing, archiving and retrieving sensor data. An excel spreadsheet prototype has bee...
详细信息
We present a spreadsheet approach to simplifying the process of managing, programming, and interacting with sensor networks and visualizing, archiving and retrieving sensor data. An excel spreadsheet prototype has been built to demonstrate the idea. this environment provides excel users, who are already familiar with spreadsheet applications, a convenient and powerful tool for programming and data analysis. We discuss the architecture of this prototype and our experience in implementing the tool. We show two different classes of sensor-net applications built using this platform. We also present performance data on the scalability of the tool with respect to data rate and number of data streams
the new generic scheme CFLP(D) has been recently proposed in [14] as a logical and semantic framework for lazy Constraint functionallogicprogramming over a parametrically given constraint domain D. Further, [15] pre...
详细信息
the proceedings contain 24 papers. the special focus in this conference is on functionalprogramming and logicprogramming. the topics include: A scalable architecture for proof-carrying code;parameterized logic progr...
ISBN:
(纸本)3540417397
the proceedings contain 24 papers. the special focus in this conference is on functionalprogramming and logicprogramming. the topics include: A scalable architecture for proof-carrying code;parameterized logic programs where computing meets learning;proving syntactic properties of exceptions in an ordered logical framework;a higher-order colon translation;compiling lazy functional programs based on the spineless tagless G-machine for the java virtual machine;a higher-order logicprogramming language with constraints;an effective bottom-up semantics for first-order linear logic programs;a framework for goal-directed bottom-up evaluation of functionallogic programs;theoretical foundations for the declarative debugging of lazy functionallogic programs;adding linear constrains over real numbers to curry;a complete selection function for lazy conditional narrowing;an abstract machine based system for a lazy narrowing calculus;incremental learning of functionallogic programs;a general type inference framework for hindley/milner style systems;monadic encapsulation with stack of regions;well-typed logic programs are not wrong;a framework for analysis of typed logic programs;abstract compilation for sharing analysis;a practical partial evaluator for a multi-paradigm declarative language;a simple take on typed abstract syntax in ML-like languages;a simply typed context calculus with first-class environments and refining the barendregt cube using parameters.
In this paper, a functional vector generation method to maximize the data path coverage of a combinational circuit is introduced. We present a new gate model based on sensitization requirements for transition propagat...
详细信息
ISBN:
(纸本)0769520936
In this paper, a functional vector generation method to maximize the data path coverage of a combinational circuit is introduced. We present a new gate model based on sensitization requirements for transition propagation, and introduce a new methodology to obtain functional vectors of maximum coverage based on Mixed Integer Linear programming (MILP). Performance comparison and results based on a large set of MCNC'91 [1] benchmark circuits are given. Experimental results show significant speedups over a greedy SAT method.
WASH makes server-side Web programming as easy as programming a stand-alone application with an XHTML-based GUI. Starting from an interaction graph model of the application where nodes model web pages and edges corres...
详细信息
ISBN:
(纸本)3540285407
WASH makes server-side Web programming as easy as programming a stand-alone application with an XHTML-based GUI. Starting from an interaction graph model of the application where nodes model web pages and edges correspond to form submissions, each node is implemented by a WASH function and the edges correspond to function invocation. Nodes can be decomposed further into "pagelets", which are XHTML fragments bundled with associated logic. We give an introduction to the concepts of WASH programming withthis methodology and advocate the design of interactive web functionality in terms of such pagelets. the two components of a pagelet may be specified monolithically or in separation. Pagelets may also be composed up to an entire WASH page. the development of a web-based logging application serves as a running example.
this paper introduces potentially-infinite list comprehensions into evolutionary computation. List comprehensions are programming constructs based on Zermelo-Fraenkel (ZF) set theory and are used in modern functional ...
详细信息
ISBN:
(纸本)1889335231
this paper introduces potentially-infinite list comprehensions into evolutionary computation. List comprehensions are programming constructs based on Zermelo-Fraenkel (ZF) set theory and are used in modern functional languages to define sets concisely. We present a flew, higher-order, polymorphic and strongly-typed Genetic programming (GP) system, ZF-GP, that evolves potentially-infinite list comprehensions. the resulting language has a highly-focussed search space that is smaller than is typical in evolutionary computation. Experiments demonstrate that the ZF-GP system can evolve list comprehension solutions to formula-fitting problems more efficiently than random search.
In this paper we propose a type-based framework for using logicprogramming for XML processing. We transform XML documents into terms and DTDs into regular types. We implemented a standard type inference algorithm for...
详细信息
ISBN:
(纸本)3540003894
In this paper we propose a type-based framework for using logicprogramming for XML processing. We transform XML documents into terms and DTDs into regular types. We implemented a standard type inference algorithm for logic programs and use the types corresponding to the DTDs as additional type declarations for logic programs for XML processing. Due to the correctness of the type inference this makes it possible to use logic programs as an implicitly typed processing language for XML with static type (in this case DTDs) validation. As far as we know this is the first work adding type validation at compile time to the use of logicprogramming for XML processing.
暂无评论