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

Функцию из последнего примера можно задать и другим поствыражением:1valuemax : Nat × Nat → Natmax( a , b ) as mposti f a > b then m = aelse m = bend234567Сравните эту запись с эксплицитной записью той же функции:1valuemax : Nat × Nat → Natmax( a , b ) ≡i f a > b then a234else b5end6Рассмотрим такое имплицитное определение:1valuemax : Nat × Nat → Natmax( a , b ) as mposta > b ⇒m = a2345Оно отличается тем, что задает функцию max не полностью: еслиa > b, то известно требование на результат функции (он должен бытьравен а), в противном случае поствыражение истинно, а про результатфункции ничего не сказано.Рассмотрим другой пример:123valuemax : Nat × Nat → Natmax( a , b ) as m48Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)post4m= a ∨ m= b5Здесь точно результат функции не известен ни в одном случае (если числа a и b имеют различные значения). И тем не менее это тожедопустимое и полезное поствыражение.Иными словами, необходимо понимать следующие возможности:∙ поствыражение должно восприниматься как необходимый эффектфункции (если поствыражение, вычисленное на аргументах и результате функции, ложно, значит функция сработала неверно; если поствыражение истинно, ничего нельзя сказать про правильность работы функции); такие поствыражения описывают ту частьфункциональности, которая должна быть соблюдена обязательнои неукоснительно, любой «шаг влево-вправо» рассматривается самым критичным образом;∙ поствыражение должно восприниматься как достаточный эффектфункции (если поствыражение, вычисленное на аргументах и результате функции, истинно, значит функция сработала правильно;в противном случае ничего нельзя сказать о правильности работы функции); такие поствыражения описывают ряд случаев, но,возможно, не весь;∙ поствыражение должно восприниматься как необходимый и достаточный эффект функции.Язык RSL не предоставляет средств для указания того, как должновосприниматься каждое поствыражение.

В каждом случае эту «модальность» надо оговаривать явно. В дальнейших примерах, если это не сказано явно, будет предполагаться, что поствыражение должно описыватьнеобходимый и достаточный эффект.Например, ответьте, почему поствыражение в следующем примерезадает функцию, не являющуюся максимумом двух чисел, даже несмотря на то, что логика короткая (многие студенты на экзамене ошибочнопредполагают, что это поствыражение действительно описывает максимум и применяют подобное «преобразование» условного выражения вдизъюнкцию, не замечая совершаемой при этом ошибки):12valuemax : Nat × Nat → Nat1.6. Эксплицитное и имплицитное описание функций49max( a , b ) as mpostm= a ∧ a > b∨ m= b3456В поствыражении могут встречаться «вызовы» других функций:1valuesum : Nat * → Natsum ( x ) as sposti f x = ⟨ ⟩ then s = 0e l s e s = sum ( t l x ) + hd x end23456Вы уже заметили, насколько похожи эксплицитная и имплицитнаязапись функций.

На самом деле если функция не использует глобальных переменных по чтению-записи и завершается с детерминированнымрезультатом, то эксплицитная запись может быть переписана в имплицитном виде очень просто: вместо возвращаемых значений запись равенство, как это было сделано в последних примерах:123value max : Nat × Nat → Natmax( a , b ) as mpost m = ( i f a > b then a e l s e b end)Однако если функция использует глобальные переменные по чтениюзаписи, то поствыражение должно содержать описание побочного эффекта. Дело в том, что поствыражение нужно для описания результатафункции, поэтому:1) поствыражение не должно иметь побочного эффекта (а функцияможет иметь побочный эффект);2) поствыражение пишется только для функций, которые завершаются и завершаются детерминированным образом (для недетерминированных функций поствыражение ложно).Итак, если исходная функция имеет побочный эффект, например1variablea , b : Int234valueswap : Unit → write a , bUnit50Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)swap ( ) ≡5l o c a l variable temp : Int := a ina := b ;b := tempend6789то эквивалентное5 определение функции в имплицитном виде полностью сохраняет сигнатуру, а в поствыражение должно входить соотношение значений переменных до вызова функции и значений после вызовафункции:1variablea , b : Int23valueswap : Unit → write a , bswap ( )posta = b′ ∧ b = a′4567UnitШтрихованные переменные — это значения переменных до вызовафункции.ЗадачиПервые задачи несложные, в них надо формализовать указанныеутверждения. Большинство задач взяты из [3].1.16.1 Ни одному лысому не нужна расческаРешение:12345scheme Exmp = c l a s stype Lys , R4value need : Lys × R4 → Boolaxiom ∀ l : Lys , r : R4 ∙ ∼need ( l , r )end51.16.2Все мои тетки не справедливы.1.16.3Ни один кошмарный сон не приятен.слово «эквивалентное» ещё раз подчёркивает, что это поствыражение следует восприниматькак необходимое и достаточное описание эффекта функции1.6.

Эксплицитное и имплицитное описание функций1.16.4Все битвы сопровождаются страшным шумом.1.16.5Не все двоечники ленивы.1.16.6Каждый, кто упорно работает, добивается успеха.1.16.7Ни один бездельник не станет знаменитостью.1.16.8Некоторые художники не бездельники.1.16.9Некоторые бездельники не художники.1.16.101.16.11ния.51Некоторые подушки мягкие.Тот, кто может укрощать крокодилов, заслуживает уваже-1.16.12Ни одна лягушка не имеет поэтической внешности.1.16.13Ни одна тачка не комфортабельна.1.16.14Всякий орел умеет летать.1.16.15Некоторые свиньи не умеют летать.1.16.16Некоторые свиньи — не орлы.1.16.17Ни один судья не справедлив.1.16.18Ни один ребенок не любит прилежно заниматься.1.16.19 Все шутки для того и предназначены, чтобы смешить людей.1.16.20Ни один парламентский акт не шутка.1.16.21Пауки ткут паутину.1.16.22Все лекарства имеют отвратительный вкус.1.16.23Ни у одной ящерицы нет волос.52Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)1.16.24Все свиньи прожорливы.1.16.25Все, что сделано из золота, драгоценно.1.16.26Некоторые секретари — птицы.1.16.27Все секретари заняты полезным делом.1.16.28Ничто разумное не ставит меня в тупик.1.16.29Логика часто ставит меня в тупик.1.16.30Некоторые цыплята — не кошки.1.16.31угольника.Точки A, B, C являются вершинами равнобедренного тре-1.16.32 Иванов, Петров, Васильев и Сидоров могут вытащить этумашину из ямы, если они трезвы и видят бутылку.1.16.33 Иванов, Петров, Васильев и Сидоров не могут решать квадратные уравнения, даже если они трезвы, но видят бутылку.1.16.34Не все углы, синус которых больше 1/2, больше /6.1.16.35 Квадратные корни из некоторых рациональных чисел иррациональны.1.16.36 Синус и косинус равны друг другу тогда и только тогда,когда равны тангенс и котангенс.1.16.37Когда кто-то поет больше часа, он надоедает.1.16.38Все девочки боятся лягушек и мышей.1.16.39Кошки бывают только белые и серые.1.16.40Все ораторы либо честолюбивы, либо скучны.1.16.41 Число делится на 25 в том и только том случае, когда оноделится на 50 либо дает при делении на 50 остаток 25.1.6.

Эксплицитное и имплицитное описание функций531.16.42 Все комплексные числа действительны или становятся действительными после умножения на i.1.16.43Не все студенты отличники или спортсмены.√1.16.44 Для того чтобы выполнялось равенство = 2 , необходимо и достаточно, чтобы было положительным действительным числом.1.16.45ложь.Не все, что рассказывал барон К.

Ф. И. фон Мюнхгаузен,1.16.46Некоторые людоеды — плохие люди.1.16.47Некоторые финансисты — мошенники, но не все.1.16.48Прапорщики любят порядок, и не только они.1.16.49Милиционеры замешаны в преступлениях, но не все.1.16.50Некоторые замки не отпираются, но запираются.1.16.51Если будешь хорошо учиться, поступишь в вуз, а иначепровалишься.1.16.52Ничего не вижу, ничего не слышу, ничего не знаю.1.16.53Молодо—зелено.1.16.54Взялся за гуж — не говори, что не дюж.1.16.55Чтобы не быть собакой, достаточно быть кошкой.1.16.56Чтобы не быть человеком, необходимо быть свиньей.1.16.57Некоторые кошки поют по ночам.1.16.58Все компакты совершенно нормальны.1.16.59Некоторые мюмзики не куздры.54Глава 1.

RAISE SPECIFICATION LANGUAGE (RSL)1.16.60Три точки A, B, C лежат на одной окружности.1.16.61Три точки A, B, C не лежат на одной прямой.1.16.62Числа a и b имеют одинаковый знак.1.16.63Одно из чисел a, b равно 0.1.16.64Числа a и b имеют разные знаки.1.16.65Ромео и Джульетта любят друг друга.1.16.66Гамлет и Клавдий ненавидят друг друга.1.16.67Мери любила Печорина, но не взаимно.1.16.68 Чтобы прийти на свадьбу, необходимо приглашение женихаили невесты.1.16.69Некоторые лентяи не оптимисты, но жизнелюбы.1.16.70Все замки отпираются и запираются.1.16.71Никто из нашего класса не поехал в Москву и Париж.1.16.72Все мои одноклассники поехали в Москву и Париж.1.16.73Некоторые числа четные.1.16.74Некоторые лекции невозможно понять.1.16.75Всякому в Москве не перекланяешься.Более сложные задачи:1.17.1 Весна, и вы говорите: «Все парни и девушки сейчас влюбленыдруг в друга».