Efektywna implementacja operatora @pre/old i jej weryfikacja

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.