Abstract Interpretation Assignment
This assignment comprises a number of exercises of equal weight.
The general rule is: Motivate your answers
The full assignment is available as a PDF download
What, how and when to submit
Details can be found here
In whatever fashion you hand things in make sure things are clear and
readable and on time.
Experiences from last year
For some of these exercises it is handy to reuse some of the Galois Insertions
I defined in the slides. You may reuse these at will, and do not have to prove
Exercise 4.11 seems a bit unclear with all the indices/variables called n.
The way to read the definition of Y (capital upsilon) is that if you are
given two ascending chains x and y, that are equal for the first Y(x)
elements, then Y(x) = Y(y).
In Mini Project 4.1 it is not clear what should be the ordering on lists.
A natural choice is x \subseteq y if and only if x is a prefix of y.
However, you do not really need this ordering, since you only have to complete
the specification, not give a proof that it is a Galois Connection/Insertion.
Still, a few examples to convince yourself that you are not too far off the mark
can be helpful.
- 07 Jun 2005