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

Speaker(s)

Aleksy Schubert i Jacek Chrząszcz

Affiliation

Uniwersytet Warszawski

Date

Oct. 19, 2009, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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ą.

---