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

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