JVM w Coqu - odcinek i-ty

Referat o tym, co zwykle, czyli o moich przygodach z formalizacją bajtkodu Javy Coq-u.
W najbliższym odcinku:
* "właściwie to mam prawie wszystkie instrukcje  operujące wewnątrz ramki" ;),
* dowód własności programu z pętlą (suma 2*i-1 dla i:[1..n] = n*n),
* machanie rękami na temat uogólnienia techniki tego dowodu i zrobienia czegoś na kształt logiki Hoare'a dla bajtkodu,
* błędy w (mojej) specyfikacji znalezione w trakcie testowego dowodu oraz refaktoryzacja faktoryzacji.