Состоялась лекция, посвящённая различным конструкциям языка спецификации ACSL. Были рассмотрены вопросы:
- при описании требований к функции у одних и тех же переменных и областей памяти может быть разное состояние (значение);
- стандартные метки памяти (метки
Here
,Pre
,Post
), обычные метки Си; - в каком состоянии используется переменная в каждом из типов выражений ACSL (т.е. значение метки
Here
для тех или иных выражений); - как специфицировать произвольное состояние переменной (выражение
\at
), состояние при входе в функцию (выражение\old
); - требования к функции могут запрещать изменять ей некоторую память;
- если некоторая память не запрещена спецификацией к изменению и нет других ограничений, то эта память может быть изменена произвольно (т.е. по умолчанию всё разрешается);
- как специфицировать какую именно память разрешено изменять функции (конструкции
assigns
иloop assigns
); - что в спецификации памяти, разрешённой на изменение, используется lvalue;
- спецификация возможности разыменовывания указателя (конструкция
\valid
);