Евгений Корныхин - Формальная спецификация программ (Евгений Корныхин - Формальная спецификация программ.pdf), страница 10

Эта функция позволяет создать дочерний процесс. Если дочерний процесс создан успешно, возвращается его идентификатор. В противном случае функция возвращает -1.Решение:12345type P r o c e s s e s = Nat -set∼value f o r k : P r o c e s s e s → P r o c e s s e s × Intf o r k ( ps ) as ( ps2 , pid )post pid = −1 ∧ ps2 = ps∨ pid ≥ 0 ∧ pid ∈/ ps ∧ ps2 = ps ∪ { pid }Обратите внимание:1) поскольку в требованиях говорится только об идентификаторах,то только эта часть отражается в модели типа Processes. Для этоймодели выбрано множество, т.к.

все идентификаторы должны бытьразными;2) эту функцию нельзя определить в эксплицитном виде с использованием выбранной модели состояния (типа Processes), т.к. нельзясразу зафиксировать алгоритм генерации идентификаторов дочерних процессов (надо оставить свободу выбора этого алгоритма);2.5. Инварианты состояния753) в случае неуспешного создания процесса таблица процессов не меняется (явно это в требованиях не описано, но такое свойство имеетместо);4) поскольку ничего не известно о детерминированности алгоритмагенерации идентификаторов дочерних процессов, то использованонетотальное определение.2.1.6Написать спецификацию функции библиотеки POSIX intfork(). Эта функция позволяет создать дочерний процесс. Если дочерний процесс создан успешно, возвращается его идентификатор.

В противном случае функция возвращает -1. После создания сегменты кода,данных и стека обоих процессов идентичны. Совпадают и счетчики инструкции. Необработанные сигналы родительского процесса в дочернийне наследуются. Считать, что для получения идентификатора текущегопроцесса есть функция int getpid().Решение:1234567type Segment , S i g n a ltype P r o c e s s : :code : Segment ,data : Segment ,s t a c k : Segment ,i n s t r _ p n t r : Nat ,signals : Signal *89type P r o c e s s e s = Nat → P r o c e s s10∼11value g e t p i d : P r o c e s s e s → Int12∼131415161718192021value f o r k : P r o c e s s e s → P r o c e s s e s × Intf o r k ( ps ) as ( ps2 , pid )post pid = −1 ∧ ps2 = ps∨ pid ≥ 0 ∧ pid ∈/ dom ps ∧ ps2 \ { pid } = ps ∧l e t parent_id = g e t p i d ( ps ) , c h i l d = ps2 ( pid ) ,p a r e n t = ps ( parent_id ) incode ( c h i l d ) = code ( p a r e n t ) ∧data ( c h i l d ) = data ( p a r e n t ) ∧stack ( c h i l d ) = stack ( parent ) ∧76Глава 2.

Контрактные спецификацииinstr_pntr ( c h i l d ) = instr_pntr ( parent ) ∧signals ( child ) = ⟨⟩222324endОбратите внимание:1) по сравнению с предыдущей задачей модель типа Processes полностью изменилась (хотя требования лишь добавлялись), этот моментпоказывает важную особенность моделе-ориентированных спецификаций в отличие от алгебраических: модели типов могут меняться существенным образом при добавлении новых требований;2) на использование явного let для введения «читабельных» имен выражениям и повышения «читабельности» всего пост-выражения.2.1.7Написать спецификацию функции библиотеки POSIX intgetpid().

Эта функция позволяет получить идентификатор процесса,вызвавшего эта функцию.Решение:1234type P r o c e s s e s = Nat -set∼value g e t p i d : P r o c e s s e s → Int × P r o c e s s e sg e t p i d ( ps ) as ( pid , ps2 )post pid ≥ 0 ∧ pid ∈ ps ∧ ps2 = psОбратите внимание, что1) данная модель не позволяет дать алгоритм вычисления функцииgetpid (поэтому используется неявная спецификация), но позволяеттем не менее задать те свойства, которые перечислены в постановкезадачи;2) хоть модель и довольно простая, но она наглядная и позволяет еечитать и делать выводы относительно функции getpid даже тому,кто не знает POSIX;3) пост-выражение можно эквивалентным образом сократить до такого: pid ∈ ps ∧ ps = ps2, поскольку в ps входят только натуральныечисла.Глава 3Инструмент DafnyИнструмент Dafny1 позволяет задать и верифицировать функциональность «классов». «Объект» «класса» содержит состояние, согласованность которых должны поддерживать методы класса.

Методам можно указать предусловие (requires) и постусловие (ensures). Если написанотело метода (некая реализация программного контракта), Dafny пытается автоматически доказать выполнение контракта реализацией методов.Если это не удается сделать, Dafny выдает сообщение об ошибке. Реализация метода осуществляется на языке инструмента Dafny императивного стиля. Dafny пытается доказать, что реализация завершаетсяна данных, удовлетворяющих предусловию. Для этого он требует указания инварианта цикла (invariant) и условия завершимости (decreases).Условия завершимости нужно указывать и для рекурсивных функций.Более подробно об инструменте можно прочитать в статьях на сайтеhttp://research.microsoft.com/en-us/projects/dafny/.Вам предлагается выполнить ряд упражнений не столько с цельюосвоения инструмента Dafny, сколько для выработки навыка написанияпрограммных контрактов и других аннотаций для верификации кода.Если Dafny успешно всё доказал, значит спецификация составлена правильно.

Если что-то Dafny не смог доказать, значит либо не полностьюописаны программные контракты/инварианты, либо они слишком сложные для автоматического доказательства (для подсказок инструментуDafny надо писать т.н. ghost methodы). Задачи подобраны таким образом, что возможно их решить, не прибегая к ghost methodам.

Кроме того,предлагаемые здесь задачи не предполагают спецификации операций спамятью.1название инструмента является смесью букв слов dynamic frames7778Глава 3. Инструмент DAFNYЕсли не удается понять, почему Dafny не может доказать то или иноесвойство, попробуйте подобавлять assert в разные точки реализации спредполагаемыми тождественно верными выражениями. Если Dafny сообщит о невыполнении одного из assert, то надо проанализировать причину этого и в результате понять, где ошибка.Dafny можно установить в виде дополнения среды разработки VisualStudio 2010, можно запускать в виде утилиты командной строки (но перед этим надо не забыть установить решатель Z3 версии 2.15), но проще всего пользоваться инструментом Dafny из браузера.

Для этого надозайти на сайт http://rise4fun.com/dafny/, написать текст методов и аннотаций и нажать кнопку ask dafny. Если Dafny сообщит о ряде проблем,можно нажать на строчку с проблемой и место проблемы будет подсвечено.ЗадачиВосстановить инвариант цикла3.1.1 (http://rise4fun.com/Dafny/t3F) Автор хотел реализовать умножение двух чисел. Напишите инвариант цикла и найдите (и исправьте)ошибку в реализации.method fi(x: int, y : int) returns (z: int)requires x >= 0 && y >= 0;ensures z == x * y;{var i := 0;while (i < y)invariant ...........;{i := i + 1;z := z + x;}}793.1.2 (http://rise4fun.com/Dafny/yqQ) Автор хотел реализовать умножение двух чисел.

Напишите инвариант цикла и найдите (и исправьте)ошибку в реализации.method fi(x: int, y : int) returns (z: int)requires x >= 0 && y >= 0;ensures z == x * y;{var i := y;while (i > 0)invariant ...........;{i := i - 1;z := z + x;}}3.1.3(http://rise4fun.com/Dafny/4Xe)method sqrt(x : nat) returns (s : int)ensures s*s <= x < (s+1)*(s+1);{s := 0;while ((s+1)*(s+1) <= x)invariant ........;{s := s + 1;}}3.1.4(http://rise4fun.com/Dafny/poC)method search(a : array<int>, key : int) returns (b: bool)requires ....;ensures b <==> exists i :: 0 <= i < a.Length && a[i] == key;{var n := a.Length - 1;if (n < 0)80Глава 3. Инструмент DAFNY{return false;}while (a[n] != key)decreases ....;invariant ....;{n := n - 1;if (n < 0){break;}}return 0 <= n;}3.1.5 (http://rise4fun.com/Dafny/Qch) Напишите спецификацию иреализацию метода вычисления кубов натуральных чисел, помещающегов i-й элемент массива i*i*i.

Добейтесь того, чтобы Dafny успешно верифицировал реализацию. Затем модифицируйте реализацию таким образом,чтобы она не использовала умножения, только сложения.method Cubes(a: array<int>)modifies a;{}3.1.6 (http://rise4fun.com/Dafny/6xO) Напишите спецификацию ирекурсивную реализацию метода вычисления кубов натуральных чисел, помещающего в i-й элемент массива i*i*i. Реализация не должнаиспользовать умножения, только сложения.method Cubes(a: array<int>)modifies a;{}813.1.7 (http://rise4fun.com/Dafny/6bq) Напишите спецификацию, прикоторой Dafny докажет правильность реализации. Нужно написать постусловие и decreases, предусловие писать не нужно. Имя метода подскажет его смысл.

method NinetyOne(n: int) returns (r: int) if (100 < n) r :=n - 10; else r := NinetyOne(n + 11); r := NinetyOne(r);3.1.8 (http://rise4fun.com/Dafny/WvG) Метод в этой задаче возвращает истину тогда и только тогда, когда последовательности f и g имеют общий элемент. Напишите и верифицируйте реализацию, временнаясложность которой O(|f| + |g|), а не O(|f|*|g|).method Coincidence(f: seq<int>, g: seq<int>) returns (r: bool)requires forall i, j :: 0 <= i <= j < |f| ==> f[i] <= f[j];requires forall i, j :: 0 <= i <= j < |g| ==> g[i] <= g[j];ensures r <==> exists m :: m in f && m in g;{}Глава 4Аналитическаяверификация4.1Методы ФлойдаЗадачиВо всех задачах 1 , 2 , ... — входные переменные, 1 , 2 , ... — промежуточные переменные, 1 , 2 , ...

— выходные переменные. Если не сказано противное, входные переменные обладают целыми неотрицательнымизначениями.Если в алгоритмах не указано условие у оператора цикла, значит этоусловие — тождественная истина (т.е. цикл бесконечный).Доказать частичную корректность следующих числовых алгоритмов14.1.11(1 , 2 ) , (1 , 2 , ) ( = 1 · 2 )Часть задач взяты из [4], часть задач составлены Алексеем Хорошиловым824.1. Методы ФлойдаMultiply(1 , 2 )1 1 ← 02 2 ← 13 while 2 ≤ 24do (1 , 2 ) ← (2 + 1 , 2 + 1)5 ← 14.1.2(1 ) , (1 , ) ( = 1 · (1 + 1))Arithmetic(1 )1 1 ← 02 2 ← 13 while 2 ≤ 14do (1 , 2 ) ← (1 + 22 , 2 + 1)5 ← 14.1.3(1 ) , (1 , ) ( = 1 · (1 + 1) · (21 + 1))SumSquare(1 )1 1 ← 02 2 ← 13 while 2 ≤ 14do (1 , 2 ) ← (1 + 62 · 2 , 2 + 1)5 ← 14.1.4(1 , 2 ) , (1 , 2 , ) ( = 1 2 )Power(1 , 2 )1 1 ← 12 2 ← 13 while 2 ≤ 24do (1 , 2 ) ← (1 * 1 , 2 + 1)5 ← 14.1.5(1 , 2 ) (2 > 0), (1 , 2 , ) ( = 1 2 )8384Глава 4.

Аналитическая верификацияPower(1 , 2 )1 1 ← 12 2 ← 13 while 2 < 24do if 22 ≤ 25then (1 , 2 ) ← (1 * 1 , 22 )6else (1 , 2 ) ← (1 * 1 , 2 + 1)7 ← 14.1.6(1 , 2 ) , (1 , 2 , ) ( = 1 2 )Power(1 , 2 )1 1 ← 12 2 ← 03 while 2 < 24do if 2 = 05then (1 , 2 ) ← (1 , 1)6else if 22 ≤ 27then (1 , 2 ) ← (1 * 1 , 22 )8else (1 , 2 ) ← (1 * 1 , 2 + 1)9 ← 14.1.7 («GCD» – greatest common divisor) (1 , 2 ) (1 + 2 > 0),(1 , 2 , ) ( = gcd(1 , 2 ))GCD(1 , 2 )1 if 1 > 22then 1 ← 13else 1 ← 24 while 1 mod 1 ̸= 0 ∨ 2 mod 1 ̸= 05do 1 ← 1 − 16 ← 14.1.8 («GCD» – greatest common divisor) (1 , 2 ) (1 + 2 > 0),(1 , 2 , ) ( = gcd(1 , 2 ))4.1. Методы Флойда85GCD(1 , 2 )1 1 ← 12 2 ← 23 while 1 > 0 ∧ 2 > 04do if 1 ≥ 25then 1 ← 1 − 26else 2 ← 2 − 17 if 1 = 08then ← 29else ← 14.1.9 («LCM» – least common multiple) (1 , 2 ) (1 + 2 > 0),(1 , 2 , ) ( = 2 · lcm(1 , 2 ))2LCM(1 , 2 )1 (1 , 2 , 3 , 4 ) ← (1 , 2 , 2 , 1 )2 while 1 ̸= 0 ∧ 2 ̸= 03do if 1 ≥ 24then (1 , 4 ) ← (1 − 2 , 3 + 4 )5else (2 , 3 ) ← (2 − 1 , 3 + 4 )6 if 1 = 07then ← 48else ← 34.1.10() , (, ) ( = 2 )Square()1 (1 , 2 , 3 ) ← (0, 0, 0)2 while 1 < 3do (1 , 2 , 3 ) ← (1 + 1, 2 + 2, 2 + 3 )4 ← 1 + 34.1.11() , (, ) ( 2 ≤ < ( + 1)2 )86Глава 4.