Oct. 18: A new
project distribution is available. The old one has DOS CRLF in it.
Oct. 12: Homework due in class on Oct. 19th
·
Consider a theory with the axioms \forall p.pAB = pB and \forall
p.pBC = pD. I write tA for the application of the unary function A to the term
t. Derive a closure operation for this theory, following the model used in
lecture. Prove that the extension of congruence closure with this operation is
complete. Hint: the conjunction of literals xA=yA and xD
<> yD is not satisfiable, and your algorithm
should discover that.
·
Give an example of a theory consisting only of unary
functions and equality axioms as above (with only only
quantified variable) for which the procedure discussed in class for deriving a
closure operation (based on constructing rules that add nodes to the EDAG),
obtains a closure operation that is not guaranteed to terminate.
Sep 28: The project
instructions are online.
Sep 24: Homework due in class on Oct 5th
·
Give another example on a non-convex theory (other than sel/upd and integer arithmetic)
·
Show that if all the axioms of the theory are of the form \forall x.f1(f2(…(fn(x))) =
g1(g2(…(gm(x))), along with the usual equality and congruence axioms, then the
theory is convex. The unary function symbols may appear several times in an
axiom like the above.
·
Is this still true if we also allow disequalities
in the axioms?
Sep 9: Homework due in class on Sep 13th
·
Prove the soundness and completeness of VCGen
(statements on slide 64 of lecture notes for lecture 2). A sketch of the proof
is enough, with a statement of the precise statement to be proved. Focus on
loops.
Sep. 3: I need volunteers for the
following lectures:
·
JML specification language and ESC-java. I envision this as a
half-lecture, half-demo of ESC Java