Weryfikacja skompilowanych klas Javy w oparciu o specyfikację w BML - studium przypadku

Prelegent(ci)

Aleksy Schubert i Jacek Chrząszcz

Afiliacja

Uniwersytet Warszawski

Termin

19 października 2009 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

W ramach zakończonego niedawno projektu Mobius powstało szereg narzędzi do specyfikacji i weryfikacji własności programów w Javie. Jednym z narzędzi jest generator obligacji dowodowych BMLVCGen, który na podstawie pliku ze skompilowaną klasą Javy wzbogaconą o binarne specyfikacje w języku BML generuje formuły w Coqu. Z prawdziwości tych formuł wynika poprawność pliku klasowego względem jego specyfikacji. Przedstawimy nasze przygody z dowodzeniem takich formuł wygenerowanych dla prostej klasy o nazwie Bill, zawierającej jedną metodę abstrakcyjną i jedną konkretną.

---