Е.А. Кузьменкова - Формальная спецификация программ (Е.А. Кузьменкова - Формальная спецификация программ.pdf), страница 2

Допускаются кванторы: ∀, ∃, ∃!.Упражнения1.Ниже приведены равенства, которые верны в классической логике. Какие изних верны в RSL?(a)(b)(c)(d)(e)(f)∼(∼a) ≡ atrue ∨ a ≡ truea ∨ true ≡ truea ⇒ true ≡ truea ⇒ b ≡ ∼a ∨ ba ∨ ∼a ≡ true7(g)(h)(i)(j)(k)(a ∧ ∼a) ≡ false(a ∧ b) ∧ c ≡ a ∧ (b ∧ c)(a ∨ b) ∨ c ≡ a ∨ (b ∨ c)(a = a) ≡ true(a ≡ a) ≡ trueУказания:• воспользуйтесь приведенными в разделе 1.1.2 таблицами истинности дляосновных логических операций;• для проверки справедливости предложенных утверждений достаточноисследовать их значения на наборах данных, где хотя бы один операндобращается в chaos.Например, для пункта (c):chaos ∨ true ≡ chaos,(chaos ≡ true) ≡ falseСледовательно, утверждение (c) неверно в RSL.2.

Упростить следующие выражения:(a) if true then false else chaos end ≡ ?(b) if a then ∼( a ≡ chaos) else false end ≡ ?Указание: воспользуйтесь свойствами (1) - (4) раздела 1.1.2.3.Какие из следующих выражений верны ?(a)(b)(c)∀ i : Int • ∃ j : Int • i+j = 0∀ i : Int • ∃ j : Nat • i+j = 0∃ i : Int • ∀ j : Int • i+j = 04.Напишите RSL выражение, выражающее тот факт, что нет наибольшегоцелого числа.Указание: воспользуйтесь квантифицированными выражениями RSL.5.Завершите определение функции, которая проверяет, является ли ееаргумент четным числом.is_even : Nat → Boolis_even(n) ≡ ...Указания:можноиспользоватьоперациюквантифицированное выражение.8\ (остатокотделения)или1.2.Описание функцийЦель данного раздела - познакомить читателя с различными принятыми вRSL стилями описания констант и функций, а также дать методическиерекомендации по выбору того или иного стиля описания в зависимости отрешаемой задачи.

Раздел содержит упражнения по выработке навыков описанияконстант и функций языка RSL в явном (explicit), неявном (implicit) иаксиоматическом (axiomatic) стилях.1.2.1. Декартовы произведения ( products )Декартовым произведением называется упорядоченный конечный наборзначений, возможно, различных типов, например:(1,2)(1,true,″John″).В декартовом произведении существенен порядок следования элементов, т.е.(1,2) и (2,1) являются различными значениями.Тип, представляющий собой декартово произведение других типов,задается выражением вида:type_expr1 × ... × type_exprn, где n≥2.Значениями такого типа являются декартовы произведения длины n (v1,...,vn),где каждое vi – некоторое значение типа type_expri.Примеры записи значений декартовых произведений с указанием их типов:(true,p ⇒ q) : Bool × Bool(x + 1, 0, ″this is a text″) : Nat × Nat × TextНад декартовыми произведениями разрешены операции = и ≠.1.2.2.

Описание константВ RSL константа рассматривается как частный случай функции, а именнокак функция без параметров с постоянным значением, поэтому для описанияконстант и функций в языке предусмотрено единое понятие value.Описание констант (value definition) в языке RSL может производиться водном из трех стилей:• явном (explicit),• неявном (implicit),• аксиоматическом.Явный стиль описания применяется, когда непосредственно указываетсязначение константы. Например, RSL- спецификация вида:value x : Int = 1определяет целочисленную константу x=1.Неявный стиль описания следует использовать, если точное значениеконстанты не указывается, а задаются лишь некоторые ограничения на этозначение. Например:value x : Int • x > 09определяет целочисленную константу x, значением которой может являтьсялюбое целое положительное число.

Спецификация при этом получаетсянеполной и может быть уточнена в дальнейшем. Такой прием называетсянедоспецификацией (under-specification) и применяется в том случае, когдаописываемое значение по каким-либо причинам не может быть определенополностью.Аксиоматический стиль описания заключается в том, что наряду с типомопределяемой константы задается также некоторый набор аксиом,накладывающих дополнительные ограничения на значение константы. Заметим,что как для явного, так и для неявного описаний можно построитьэквивалентное описание в аксиоматическом стиле. Например, эквивалентнаяформа приведенных выше описаний константы x в аксиоматическом стилевыглядит следующим образом:value x : Intaxiom x ≡ 1 (для явного описания),value x : Intaxiom x > 0 (для неявного описания).1.2.3.

Описание функцийОписание функции в RSL начинается с определения её сигнатуры, т.е.имени функции и типов входных и выходных параметров, здесь же задается видфункции с точки зрения возможности её вычисления для всех значений,определяемых типом входных параметров.1.2.3.1.Всюду вычислимые и частично вычислимые функцииФункция f, отображающая значения типа T1 в значения типа T2, являетсявсюду вычислимой (total function), если для любого значения из T1 f возвращаетнекоторое единственное значение из T2, т.е.

f обладает следующим свойством:∀ x : T1 • ∃! y : T2 • f(x) ≡ yСигнатура функции f в этом случае имеет вид:f : T1 → T2Всюду вычислимые функции всегда детерминированы и определены для всехзначений входных параметров.Функция f, отображающая значения типа T1 в значения типа T2, являетсячастично вычислимой (partial function), если существует такое значение v типаT1, для которого вычисление f(v) может либо вообще не завершиться (в этомслучае f(v) ≡ chaos), либо приводить к недетерминированному результату,когда разные обращения к функции f со значением v могут возвращатьразличные значения типа T2.Сигнатура частично вычислимой функции f имеет вид:f : T1 −∼→ T2Частично вычислимые функции включают в себя всюду вычислимые функции.10Дальнейшее определение функции подобно рассмотренному ранееопределению констант может производиться в различных стилях в зависимостиот специфики решаемой задачи.1.2.3.2.Явный стиль описания функцийОписание функции в явном стиле (explicit function definition) ориентированона описание конкретного алгоритма и используется в том случае, когда явнозадаётся способ преобразования входных параметров в выходные.

Примеромявного описания всюду вычислимой функции может служить следующийфрагмент RSL спецификации:valuef : Int → Intf(x) ≡ x + 1В качестве примера описания частично вычислимой функции в явном стилерассмотрим функцию p(x), вычисляющую значение 1/x:valuep : Real −∼→ Realp(x) ≡ 1.0/xpre x ≠ 0.0Последняя строка данного описания содержит предусловие, накладывающеенекоторое ограничение на значения входного параметра.1.2.3.3.Неявный стиль описания функцийОписание функции в неявном стиле (implicit function definition),абстрагируясь от конкретного алгоритма, во главу угла ставит формализациюотношений, связывающих между собой входные и выходные параметры, т.е.здесь описывается не сам алгоритм, а эффект его применения. Этот стильописания является более общим в том смысле, что алгоритм преобразования неуточняется и, следовательно, для одной и той же неявной спецификации можнопредложить разные алгоритмы, эффект применения которых удовлетворяетуказанной спецификации.

Ниже приведены примеры описания в неявном стилевсюду вычислимой функции f(x), возвращающей в качестве результатанекоторое целое число, превосходящее входное значение:valuef : Int → Intf(x) as r post r > xи частично вычислимой функции square_root(x) для нахождения значенияквадратного корня:valuesquare_root : Real −∼→ Realsquare_root(x) as spost s ∗ s = x /\ s ≥ 0.0pre x ≥ 0.011Причем, как видно из примеров, конкретный алгоритм получения результатаостается в обоих случаях за рамками рассмотрения.1.2.3.4.Аксиоматическое описание функцийПри использовании аксиоматического стиля описания функциипредлагается некоторый набор аксиом, определяющих свойства результатафункции, а также, возможно, и ее входных параметров. Этот стиль описанияможет применяться с одинаковым успехом и для описания алгоритма, и дляописания эффекта выполнения функции, поэтому как для явного , так и длянеявного описаний всегда можно предложить эквивалентное описание ваксиоматическом стиле.

Кроме того данный стиль является единственновозможным при описании алгебраических спецификаций, где аксиомы имеютспецифический вид (например, f(g(x), x) ≡ h(x)), т.е. в качестве аргументафункции допускается использование обращения к функции.В качестве примеров приведем аксиоматическое описание всюду вычислимойфункции f(x), эквивалентное рассмотренному выше явному описанию той жефункции:valuef : Int → Intaxiom ∀ x : Int • f(x) ≡ x + 1и частично вычислимой функции square_root(x), также рассмотренной ранее:valuesquare_root : Real −∼→ Realaxiom∀ x : Real • x ≥ 0.0 ⇒∃ s : Real •square_root(x) = s /\s ∗ s = x /\ s ≥ 0.01.2.3.5.Схема определения функцииПодводя итог вышесказанному, можно предложить следующую схемуопределения функции:1.