|
Descripción
|
|
|---|---|
| In order to improve the quality of software products, various techniques can be used within the software development life cycle. A topic that has received significant interest in recent years has been the technique of program validation via static and/or dynamic checking of user.provider assertions. Such assertions can be considered a (partial) program specification in the form of annotations in the source code. Together with analysis tools, they allow detecting incorrect program behaviors, studying resource consumption, and reasoning about various other properties of the program. This approach has proven quite useful in the domain of Logic Programming, where on of the richest designs and implementations of a combination of assertion language and analysis tools can be found in the Ciao System. On of the features of this system is the support of higher-order. Higher-order logic programming extends the expressiveness of conventional first-order logic programming, both syntactical and semantically. While quite useful in practice, higher-order also poses challenges in analysis and verification. This thesis contributes to solving the problem of analysis, checking, and specification of higer-order logic programs. It proposes a higher-order extension of the traditional Ciao assertion language and of the CiaoPPP run-time verification mechanisms. We explore different alternatives for checking, highlighting the benefits and drawbacks of each of them. We also present a prototype implementation, based on the current language extension mechanism of Ciao, and some early experimental results. We expect this first approach to the problem to serve as a basis for the design and development of more sophisticated checking and analysis tools of high-order programs. | |
|
Internacional
|
No |
|
ISBN
|
|
|
Tipo de Tesis
|
Master |
|
Calificación
|
Sobresaliente cum laude |
|
Fecha
|
23/07/2013 |