Abstract
The increasing complexity of software systems has led to the development of sophisticated
formal methodologies for verifying and correcting data and programs. In
general, establishing whether a program behaves correctly w.r.t. the original programmer’s
intention or checking the consistency and the correctness of a large set of data
are not trivial tasks as witnessed by many case studies which occur in the literature.
In this dissertation, we face two challenging problems of verification and correction.
Specifically, the verification and correction of declarative programs, and the
verification and correction of Web sites (i.e. large collections of semistructured data).
Firstly, we propose a general correction scheme for automatically correcting declarative,
rule-based programs which exploits a combination of bottom-up as well as topdown
inductive learning techniques. Our hybrid methodology is able to infer program
corrections that are hard, or even impossible, to obtain with a simpler, automatic
top-down or bottom-up learner. Moreover, the scheme will be also particularized to
some well-known declarative programming paradigm: that is, the functional logic and
the functional programming paradigm.
Secondly, we formalize 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. We provide a rule-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
detects both incorrect/forbidden patterns as well as lack of information, that is, incomplete/
missing Web pages. Useful information is gathered during the verification
process which can be used to repair the Web site. So, after a verification phase, one
can semi-automatically infer some possible corrections in order to fix the Web site.
The methodology is based on a novel rewriting-like technique, called partial rewriting,
in which the traditional pattern matching mechanism is replaced by a more suitable
technique (tree simulation) for recognizing patterns inside semistructured documents.