Nie jesteś zalogowany |
JVM w Coqu - odcinek i-ty
- Prelegent(ci)
- Patryk Czarnik
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 7 maja 2012 10:15
- Pokój
- p. 4790
- Seminarium
- Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji
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.
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.
