Efektywna implementacja operatora @pre/old i jej weryfikacja

Prelegent(ci)

Piotr Kosiuczenko

Termin

30 listopada 2009 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Referat dotyczy implementacji operatorów zwracających wartość parametru sprzed wykonania operacji takich jak @pre w języku OCL oraz \old w językach JML i Spec#. Dotychczasowe implementacje nie gwarantowały żadnych ograniczeń czasowych, a nawet własności zatrzymywania się programu. Z drugiej strony sztucznie ograniczały dopuszczalne wyrażenia języka specyfikacji. Zaproponowany ostatnio algorytm unika tych problemów. W referacie przedstawiona zostanie jego aspektowo zorientowana implementacja, formalizacja oraz dowód poprawności.

---