Нужна помощь в понимании метода Овики-Гриза
Я (по ошибке) взял курс о проверке параллельных программ, и мы до сих пор рассматривали этот метод, называемый "метод Овики-Гриза". По-видимому, можно доказать различные результаты о программе, связав утверждение с каждым утверждением, и показать, что эти утверждения являются индуктивными и не мешают друг другу. Одно из наших заданий включает алгоритм быстрого взаимного исключения Лампорта, подробно описанный в этой статье:
В статье дано доказательство взаимного исключения в духе Овики-Гриза. Это выглядит абсолютно антиинтуитивно. Что я пытаюсь понять, так это как сформулировать эти утверждения? Когда вы знаете, что эти утверждения не слишком сильны (настолько сильны, что нарушают свободу вмешательства) и не слишком слабы (например, что-то тривиальное, например, тавтология с каждым утверждением)?
ура
1 ответ
Для начала и для понимания метода Овики-Гриса я настоятельно рекомендую проверить две главы об Овики-Грисе, которые можно найти в этом учебнике.
(Полный текст учебника также можно найти в виде черновика здесь в середине 2021 года, или вы можете отправить письмо профессору Моргану, чтобы запросить копию)
Когда вы пишете утверждение, а затем пытаетесь доказать локальную правильность, цитируя учебник, «каждое утверждение ... является постусловием для фрагмента непосредственно перед ним и предварительным условием для фрагмента (строки кода) сразу после.
Чтобы ответить на ваш вопрос, вы спрашиваете, как определить силу утверждения. Поскольку утверждение необходимо до и после каждой строки кода, оно будет варьироваться от чрезвычайно слабого до умеренно слабого. Таким образом, я предлагаю сначала попробовать умеренно слабое утверждение.
Когда вы доказываете локальную правильность, глобальные инварианты и глобальную правильность, если вы понимаете, что утверждения слишком сильны, вы можете вернуться к коду и ослабить их. И наоборот, если утверждения слишком слабые, вы можете попробовать настроить их, чтобы они были немного сильнее.
Вы знаете, что они - правильная сила, когда они поддерживают выполнение вашей программы, соблюдая условия Овицки-Гриса и удовлетворяя свойства безопасности и живучести.