Specyfikacja części nieimienniczej systemów w języku OCL

Specyfikacja kontraktowa pozwala opisać  skutki wykonania metod. Ich wykonanie zwykle zmienia niewielki fragment systemu pozostawiając resztę bez zmian. Język JML posiada mechanizm służący do specyfikacji części niezmienniczej. OCL i niektóre inne języki kontraktowej specyfikacji takich środków nie posiadają.
W tym referacie przedstawimy rozszerzenie OCL umożliwiające specyfikację części niezmienniczej. W szczególności omówimy związane z tym zagadnienia specyficzne dla języka OCL, takie jak specyfikacja asocjacji i widoków.