Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

Ответ( с консультации ):

Если у нас одна точка сечения(а это возможно), то она может располагаться в одном из трёх мест: в начале цикла, перед проверкой выхода из цикла, в конце цикла(перед очередной итерацией); в первом случае потребуется доказывать 5 условий в методе индуктивных утверждений; во втором случае потребуется доказывать тоже 5 условий; в третьем случае потребуется доказывать 8 условий. Получается минимум - 5 условий, максимум - 8 условий.

А12. Каково минимальное и максимальное число утверждений, которые необходимо доказать при использовании лишь одной точки сечения в рамках доказательства полной корректности заданной функции P (она задана на языке Си)? Ответ обосновать. Если одной точки сечения недостаточно, обосновать это.

Пример:

int P(int x) {
int y1 = x, y2 = x;
do {
if (y1 > y2 + y2) {
y2++;
}
y1 += y2;
} while (y1 < y2);
return y1 + y2;
}

А13. Доказать или опровергнуть теорему о частичной или полной корректности. Заглавными буквами обозначены программы, строчными - формулы.

Пример: верно ли, что для любых a, b если {a}P{b}, то {b}P{a} ?

Ответ: неверно; контрпример: a = false, b любое, P не зацикливается хотя бы на данных, для которых выполнено b. {false}P{b} = true, {b}P{false} = false.

А14. Дано выражение. Может ли оно быть оценочной функцией и, если может, то при каких условиях? Свой ответ кратко аргументируйте по определению.

Пример: выражение: x (x - очередь из целых чисел)

Ответ: да при следующих условиях: фундированное множество - множество очередей из натуральных чисел + 0, отношение частичного порядка - x <= y <=> длина x <= длина y. Множество будет фундированным, т.к. любая очередь >= пустой очереди, чья длина равна 0.

«Теоретические» задания

Б1. Дать определение термина в одном-двух предложениях. Определение должно пояснять смысл термина.

Пример: частичная корректность.

Ответ: это отношение на программах и парах формул: {a}P{b} т.и т.т.,к. на всех входных данных, удовлетворяющих a, если P на них завершается, то для них и результата программы выполнено b.

Б2. Приведите одно отличие и одно сходство данных двух понятий.

Пример: полная корректность и частичная корректность.

Ответ: отличие - первое всегда ложно на тех данных из предусловия, на которых программа зацикливается, а второе истинно; сходство - это всё отношения на программах и парах формул.

Инструмент PVS и язык ACSL

«Практические» задания

А1. Каково минимальное количество листовых вершин в дереве доказательства следующей теоремы (не используя prop, assert и grind) ?

Пример: (A IMPLIES B AND C) AND A IMPLIES B

Ответ: 2, нужно использовать минимум один сплит, который разделит второй AND

Рецепт: http://goo.gl/SwbJd

А2. Приведите PVS теорему, в которой бы встречался указанный кусок доказательства (последовательность команд PVS, все команды завершаются результативно).

Пример: (skosimp) (assert)

Ответ:

axiom_name: LEMMA (FORALL (x : int) : (FORALL (y : int) : (x - y >= 0 AND x + y >= 0 IMPLIES x >= 0)))

А3. Можно ли использовать PVS для приведенной цели? Если можно, напишите одно предложение, как.

Пример: формальная спецификация функциональных свойств программ.

Ответ: можно, теории PVS - и есть формальные спецификации функциональных свойств программ.

А4. Перепишите на языке PVS аксиому с языка RSL.

Пример: axiom forall x : X, y : Y :- f(x) + f(y) > 0 => f(x) = 2*f(y) /\ f(x+y) > f(x)

Ответ (наверное):

theory_name: THEORY

BEGIN

X : TYPE;

Y : TYPE;

f : [X, Y -> int]

axiom_name: AXIOM (FORALL (x: X, y: Y): (f(x)+f(y)>0) IMPLIES (f(x)=2*f(y) AND f(x+y)>f(x)))

END theory_name

А5. Задание на дерево доказательства PVS.

Пример: Приведите пример теоремы на PVS, в дереве доказательства которой будет не менее 2 листовых вершин. Ответ обосновать.

Ответ: (A IMPLIES B AND C) AND A IMPLIES B

Обоснование выше в A1.

А6. Сформулируйте на PVS любую одну из теорем для данной программы на языке Си, снабженной спецификацией на ACSL. Теоремы строятся для доказательства полной корректности реализации относительно спецификации согласно методам Флойда.

Пример:

/*@ ensures if (x < 0) \result == 0; else \result == x/2; */
int P(int x) {
int y1 = x, y2 = 0;
if (x < 0) {
return 0;
} else {
/*@ loop variant y1; */
while (y1 > y2) {
y1 --; y2++;
}
return y1;
}
}

Ответ: FORALL (x:int) : (x<0 IMPLIES (IF (x<0) THEN 0=0 ELSE 0=div(x/2)))

Нас просят сформулировать любую из теорем, которая понадобится для доказательства полной корректности. Здесь y1 выбрана в качестве оценочной функции. Можно записать теорему о том, что она убывает.

Рецепт: выбрали здесь самую простую ветку(когда x<0), написали путь от START до HALT по этой ветке, в консеквенте записали постусловие, вместо \result подставили 0. В антецеденте (предусловие /\ x<0), предусловия нет => предусловие=true. Получили что получили.

А7. Сформулировать на ACSL контракт функции, описанной в задании.

Пример: максимум массива, сигнатура функции int max(int *values, int length);

Ответ:

./*@

requires length > 0;

requires \valid_range(values, 0, length - 1);;

assigns \nothing; ←- не обязательно это писать

ensures \forall int i; 0 <= i <= length-1 ==> \result >= values[i];

ensures \exists int e; 0 <= e <= length-1 && \result == values[e];

*/

Рецепт: взботнуть ACSL. Контракт состоит (как минимум) из предусловий (\requires) и постусловий (\ensures). Суть такова, что если выполняются предусловия, то должны выполнятся и постусловия. В предусловия вносится все, наиболее адекватно отвечающее функции. В постусловиях обычно описывается результат функции и ограничения результата (например, может понадобиться сказать, что результат не переполняется)

А8. Удовлетворяет ли заданная реализация на языке Си своему контракту? Ответ обосновать.

Пример:

/*@
requires x > 3 && y > 0;
ensures \result > 1;
*/
int P(int x, int y) {
if (x < y+1) {
return y - x;
} else {
return x;
}
}

Ответ: Нет. Положим x=y=5 (requires выполнено). Тогда 5 < 5 + 1 -> return 5-5 = 0, /result = 0 < 1 (ensures не выполнено)

Рецепт: Видно пристальным взглядом

«Теоретические» задания

Б1. Что делает указанная команда PVS ?

Пример: split

Ответ: Splitting eliminates any top-level conjunction разбивает конъюнкцию в консеквенте на несколько подцелей доказательства, каждая соответствует своему конъюнкту; аналогично с дизъюнкцией в антецеденте.

Рецепт: Ботать список команд в шапке PVS

Б2. Напишите два сходства приведенных двух понятий.

Пример: антецедент и консеквент.

Ответ:

1. Термины схемы доказательства PVS.

2. Логические утверждения (формулы)

Рецепт: Ботать термины PVS

16

Характеристики

Список файлов ответов (шпаргалок)