One particular instance of reasoning about the semantic correctness of programs is to prove that two programs in fact are equivalent, where the notion of equivalence may be relativized w.r.t. the set of observations of interest to be made about the behavior of the code.
In general, proving equivalence is an intriguing problem. The tutorial at MOD 2015 gave a non-exhaustive overview over various techniques in the field. In a first lecture, the tutorial considered the most simple form of programs, namely, straight-line programs which are the basis of, e.g., grammar-based compression schemes.
The second and third lecture then considered document processors which transform structured input into (possibly unstructured) output. Even if these processors are finite-state, elaborate techniques from commutative algebra are required to obtain effective decision procedures.
Finally, the fourth lecture considered observational equivalence of programs in general. Based on a formulation as a hyper-safety property a framework was presented which allows to apply techniques from relational abstract interpretation to infer equivalences in non-trivial cases.
In order to provide a homogeneous presentation of original results, we concentrate in these lecture notes on formalisms where effective decision procedures can be provided, namely, on deterministic top-down tree transducers with and without structured output.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com