1,721,044 research outputs found
A Rewriting-Based Framework for Web Sites Verification
No full textIn this paper, we develop a framework for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. First, we provide a rewriting-based, formal specification language which allows us to define syntactic as well as semantic properties of the Web site. Then, we formalize a verification technique which obtains the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete information and/or missing pages. Our methodology is based on a novel rewriting-based technique, called partial rewriting, in which the traditional pattern matching mechanism is replaced by tree simulation, a suitable technique for recognizing patterns inside semistructured documents. The framework has been implemented in the prototype Web verification system Verdi which is publicly available
Semantic Verification of Web System Contents
No full textIn this paper, we present a rule-based specification language to define and automatically check semantic as well as syntactic constraints over the informative content of a Web system. The language is inspired by the GVERDI language and significantly extends it by integrating ontology reasoning into the specification rules and by adding new syntactic constructs. The resulting language increases the expressiveness of the original one and enables a more sophisticated treatment of the semantic information related to the contents of the Web system
A fold/unfold transformation framework for rewrite theories extended to CCT
No full textMany transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we present a fold/unfold-based transformation framework for rewriting logic theories which is based on narrowing. For the best of our knowledge, this is the first fold/unfold transformation framework which allows one to deal with functions, rules, equations, sorts, and algebraic laws (such as commutativity and associativity).
We provide correctness results for the transformation system w.r.t.
the semantics of ground reducts.
Moreover, we show how our transformation technique can be naturally
applied to implement a Code Carrying Theory (CCT) system.
CCT is an approach for securing delivery of code from a producer to a consumer
where only a certificate (usually in the form of assertions and proofs)
is transmitted from the producer to the consumer who can check its validity and
then extract executable code from it. Within our framework, the certificate
consists of a sequence of transformation steps which can be applied to
a given consumer specification in order to automatically synthesize safe
code in agreement with the original requirements.
We also provide an implementation of the program transformation framework
in the high--performance, rewriting logic language Maude
which, by means of
an experimental evaluation of the system,
highlights the potentiality of our approach
Narrowing-Driven Partial Evaluation of Functional Logic Programs
No full textLanguages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the resolution principle of logic languages. Formal methods of transformation of functional logic programs can be based on this well-established operational semantics. In this paper, we present a partial evaluation scheme for functional logic languages based on an automatic unfolding algorithm which builds narrowing trees. We study the semantic properties of the transformation and the conditions under which the technique terminates, is sound and complete, and is also generally applicable to a wide class of programs. We illustrate our method with several examples and discuss the relation with Supercompilation and Partial Evaluation. To the best of our knowledge, this is the first formal approach to partial evaluation of functional logic programs. © Springer-Verlag Berlin Heidelberg 1996
VERDI: an Automated Tool for Web sites Verification
No full textVERDI is a system for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are actually fulfilled. It provides a rule-based, formal specification language which allows us to define syntactic/semantic properties of the Web site as well as a verification facility which computes the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete/missing Web pages
Specification and Verification of Web Applications in Rewriting Logic
No full textThis paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through a communicating
protocol abstracting HTTP. The proposed framework includes a scripting language that is powerful enough to model the dynamics of complex Web
applications by encompassing the main features of the most popular Web scripting languages (e.g. PHP, ASP, Java Servlets). We also provide a
detailed characterization of browser actions (e.g. forward/backward navigation, page refresh, and new win- dow/tab openings) via rewrite rules,
and show how our models can be naturally model-checked by using the Linear Temporal Logic of Rewriting (LTLR), which is a Linear Temporal Logic
specifically designed for model-checking rewrite theories. Our formalization is particularly suit- able for verification purposes, since it allows
one to perform in-depth analyses of many subtle aspects related to Web interaction. Finally, the framework has been completely implemented in Maude,
and we report on some successful experiments that we conducted by using the Maude LTLR model-checker
A Unifying View of Functional and Logic Program Specialization
No full textWe give a general introduction to the particular problems associated with the partial evaluation of functional logic programs, explain the relationship with similar techniques for functional and logic languages, and show that it is useful to transfer the technology of narrowing into a technique for driving specialization in integrated languages
Abstract Correction of First-Order Functional Programs
No full textDEBUSSY is an (abstract) declarative diagnosis tool for functional programs which are written in OBJ style. The tool does not require the user to either provide error symptoms in advance or answer any question concerning program correctness. In this paper, we formalize an inductive learning methodology for repairing program bugs in OBJ-like programs, which is based on the so-called example-guided unfolding (Bostrom and Idestam-Alquist, 1999). Correct programs are synthesized by unfolding and removing rules of the faulty program. Rules to be unfolded (deleted) are selected according to the examples, which can be automatically generated as an outcome by the DEBUSSY diagnoser. © 2003 Published by Elsevier Science B.V.
Abstract Correction; Abstract Interpretation; First Order Functional Programs; Inductive Learning; Program Transformatio
- …
