Efektywna implementacja operatora @pre/old i jej weryfikacja

Speaker(s)

Piotr Kosiuczenko

Date

Nov. 30, 2009, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---