 |
 |
 |
 |
 |
 |
 |
|
|
|
|
|
|
|
Recent advances in Computerized Numeric Control (CNC) have allowed the manufacturing of products with high quality standards. Since CNC programs consist of a series of assembler-like instructions, several high-level languages, such as AutoLISP, have been proposed in order to raise the programming abstraction level. Unfortunately, the lack of formality in these languages prevents the verification of programs. In this work, we propose the use of Haskell in CNC programming. Haskell is a modern pure functional language permitting formal verification and presenting advanced features such as lazy evaluation, higher order, etc. These features will allow us to cope with infinite data structures, to apply heuristics to CNC programs in order to optimize them, etc. |
The development of modern routers require a significant effort to be designed, built, and verified. While hardware routers are faster, they are difficult to configure and mantain. Software routers, on the other hand, are slower but can easily be configured and mantained. Recently, a modular architecture and software toolkit for building routers and other packet processors has been introduced: the system Click. It includes a specification language with features for declaring and connecting router elements and for designing abstractions. We propose the use of a declarative multi-paradigm language, Curry, to specify routers. Since Curry is a fully declarative language, router specifications can be transformed, optimized, verified, etc., by using a number of existing formal techniques. Moreover, we will show that the features of Curry are particularly useful to design router components with a high-level of abstraction. Our first experiments point out that the proposed methodology is both useful and practical... |
There are very few approaches to measure the execution costs of lazy functional (logic) programs. The use of a lazy execution mechanism implies that the complexity of an evaluation depends on its context, i.e., the evaluation of the same expression may have different costs depending on the degree of evaluation require by the different contexts where it appears. We have develop a novel approach to complexity analysis of functional (logic) programs. We focus on the construction of equations which compute the time-complexity of expressions. In contrast to previous approaches, it is simple, precise -i.e., it computes exact costs rather than upper/lower bounds-, and fully automatic. |
The PRISMA architecture includes different aspects that are able to specify the whole structure and behaviour of complex systems. Here you can find the implementation of the distribution aspect. |
Program slicing is a well-known technique to extract the program statements that (potentially) affect the values computed at some point of interest. In this work, we introduce a novel slicing method for XML documents. Essentially, given an XML document (which is valid w.r.t. some DTD), we produce a new XML document (a slice) that contains the relevant information in the original XML document according to some criterion. Furthermore, we also output a new DTD such that the computed slice is valid w.r.t. this DTD. A prototype implementation of the XML slicer has been undertaken. |
| Filtering HTML Documents |
|
Nowadays, Internet is the main source of information for millions of people and enterprises. However, the information in Internet has not been classified yet and, consequently, the search for information is one of the most important tasks and processes performed by users and systems. In particular, for WWW human users the search for information is the main (time-consuming) task performed. In order to face this problem both the industrial and the academic communities have developed many methods and tools to index and search web pages. The most extended solution is the use of search engines such as Google and Yahoo; however, while current search engines can be a suitable solution to find a particular webpage, they are useless to find the relevant information in such a page. Hence, once a webpage is found, the user must search on it in order to verify if the information needed is in there. This is a problem which until now has not been satisfactorily solved and, thus, there is not an extended solution. In this project we develop a tool able to automatically extract from a webpage the information (text, images, etc.) related to a filtering criterium without the use of semantic specifications or lexicons and without the need of offline parsing or compilation processes. |
 More Information... |
Algorithmic debugging is a semi-automatic debugging technique which
is based on the answers of an oracle (usually the programmer) to a
series of questions generated automatically by the algorithmic
debugger. The technique typically traverses a record of the
execution---the so-called execution tree---which only
captures the declarative aspects of the execution and hides
operational details. In this work we overview and compare the most
important algorithmic debuggers of different programming paradigms.
In the study we analyze the most important features incorporated by
current algorithmic debuggers, and we identify some features not
supported yet by any debugger. We then compare all the debuggers
giving rise to a map of the state of the practice in algorithmic
debugging. |
This work presents the nofib-buggy suite: a
collection of benchmarks written in Haskell. The suite is an
extension of the well-known \emph{nofib} suite but with the
peculiarity that all the programs in the new suite are buggy. This
characteristic makes the benchmarks useful to test and compare
debugging methods. We describe the kind of bugs used in the
suite, and how they have been distributed. It is also explained how
to download, use and contribute to the nofib-buggy suite. |
SOC is a program slicer for CSP specifications. In order to increase the precision of program slicing, SOC uses a new data structure called Context-sensitive Synchronized Control Flow Graph (CSCFG). Given a CSP specification, SOC generates its associated CSCFG and produces from it two different kinds of slices; which correspond to two different static analyses. |
CSP2PN is a tool that automatically builds a Petri net which produces the same sequences of observable events that a given CSP specification. In CSP terminology, these sequences are the so-called traces. In Petri nets they correspond to transition firing sequences. The transformation algorithm uses an instrumentation of the standard CSP's operational semantics as defined by A.W. Roscoe to explore all posible computations of a specification. The semantics is deterministic because the rule applied in every step is predetermined by the initial configuration. Therefore, the algorithm can execute the semantics several times to iteratively explore all computations and hence, generate the whole Petri net. |
Copyrights are held variously by the authors or publishers. In general, these papers are provided for direct use in scholarship and education. If you are contemplating other uses, such as republication, you must obtain appropriate permissions. If you wish to cite any of the published work, please look up the formal publication, and use that version. The preprints in this area are as accurate as I can make them, but they are not authoritative copies of the published versions.
|
Copyrights are held variously by the authors or publishers. In general, these papers are provided for direct use in scholarship and education. If you are contemplating other uses, such as republication, you must obtain appropriate permissions. If you wish to cite any of the published work, please look up the formal publication, and use that version. The preprints in this area are as accurate as I can make them, but they are not authoritative copies of the published versions.
El aspecto de distribución de PRISMA VIII Jornadas Ingeniería del Software y Bases de Datos (JISBD'03), Alicante (Spain). Available: Abstract / PDF / BibTeX entry
|
|
