Сейчас это задание формулируется так: "Какое требуется минимальное число точек сечения, чтобы доказать частичную корректность любой программы, имеющей указанные особенности. Ответ кратко обосновать." Может показаться, что спрашивается следующее. Введем ряд обозначений:
- p(P) - предикат, истинный на тех и только тех программах Р, которые "имеют указанные особенности"';
- n(P, pre, post) - функция, обозначающая для программы P и предусловия pre и постусловия post множество количеств точек сечения при доказательстве {pre}P{post}, n(P, pre, post) = {k1, k1+1, k1+2, ... } для некоторого k1;
- n(P) - функция от программы P, возвращающая множество чисел, такая, что n(P) = \inter_{pre,post} n(P, pre, post); т.е. это все числа, которые есть во всех n(P, pre, post) вне зависимости от pre и post (множество чисел, начиная с минимального числа точек сечения при фиксированной программе P), т.е. n(P) = {k2, k2+1, k2+2, ...} для некоторого k2.
Итак, может показаться, что в задаче по p надо привести n = \min \inter_{P : p(P)} n(P) , т.е. минимальное число точек сечения, которого хватит для каждой программы, обладающей p. Вычислить это число довольно непросто. На самом деле в задании требуется по p привести n = \min \union_{P : p(P)} n(P). Поэтому в экзамене формулировка этого задания будет изменена следующим образом: "Какое требуется минимальное число точек сечения, чтобы доказать частичную корректность хотя бы одной программы, имеющей указанные особенности. Ответ кратко обосновать.".
Комментариев нет:
Отправить комментарий