Евгений Корныхин - Формальная спецификация программ (1185143), страница 2
Текст из файла (страница 2)
Сигнатура модели с внутренним состоянием9Можно объединить объявления типов Stack и Element так:1scheme STACK = c l a s s23type Stack , Element45endЗа каждым из таких типов закреплено некоторое множество значенийи операторы сравнения на равенство/неравенство.Операции описываются с указанием их имени, типов аргументов итипов результатов. Если типов несколько, они пишутся через символ×. Порядок типов важен. Так описываются операции в аппликативномстиле:12scheme STACK = c l a s stype Stack , Element3∼4value push : Stack × Element → Stack5∼6value pop : Stack → Stack × Element78endВнимательный читатель спросит, зачем нужно 2 аргумента для того,чтобы поместить данные в стек? Или, если я хочу достать элемент с вершины стека, зачем я должен передавать еще какой-то аргумент? Делокак раз в аппликативном стиле.
В нем мы обязаны передавать полностью всю информацию, которой будет пользоваться операция и какойинформацией операция будет отвечать. Полностью — значит, настоящиеаргументы (например, те данные, которые надо положить в стек), состояние окружения модели (если это важно для ее функционирования) ивнутреннее состояние модели! В данном случае окружение влияния неоказывает, а внутреннее состояние имеется и его мы указали в качестведополнительных аргументов (Stack в аргументах и результатах операций).Как отмечалось ранее, модель может «зацикливаться» 1 , может отвечать недетерминированно. Будем называть операцию модели тотальной, если по этой операции модель не «зацикливается» и ведет себя де1на деле модель не зацикливается, это слово выбрано для сокращения ситуации, когда модельперестает отвечать на входные воздействия10Глава 1.
RAISE SPECIFICATION LANGUAGE (RSL)терминированным образом. Для того, чтобы указать в модели, что некаяоперация является тотальной, нужно поставить в ее сигнатуре стрелку →. В прошлом примере тотальной операцией должна быть операцияpush, а про операцию pop нельзя сказать, что она должна быть тотальной:12scheme STACK = c l a s stype Stack , Element34valuepush : Stack × Element → Stack ,∼pop : Stack → Stack × Element567endЗаметим, что указать в операции, что она не должна быть тотальной,нельзя (операция либо только тотальная как push, либо всякая как pop).В последнем примере показано, как задать несколько операций в однойсекции value.Операции push и pop получают аргумент типа Element «от пользователя», а аргумент типа Stack является одним из результатов других pushи pop.
Но рано или поздно должен найтись, грубо говоря, «самое старое»,«первоначальное», значение в типе Stack для операций push или pop (этозначение не представимо в виде результата push или pop, для его представления нужно иное средство). Для стека таким «первоначальным»значением является пустой стек. Добавим его в модель, такое значениеявляется константой:12scheme STACK = c l a s stype Stack , Element34valueempty : Stack ,push : Stack × Element → Stack ,∼pop : Stack → Stack × Element5678end1.2. Предопределенные типы11Задачиописать сигнатуры операций над моделями, рассмотренными в предыдущих задачах. Указать требование тотальности операций, если операция должна быть тотальной.1.2Предопределенные типыInt, Nat, Real, Bool, Char, Text, Unit.Тип Int содержит в себе все возможные целые числа. Ограниченийна их значения (типа MAXINT) нет.Тип Nat содержит число 0 и все возможные положительные целые числа.
Ограничений сверху на их значения нет. Тип поддерживаетвсе операции, определенные для типа Int. Неограниченные целые числанеобходимы для того, чтобы представлять такие заранее неограниченные величины как количества элементов, время (как количество единицвремени).Тип Real содержит в себе все возможные вещественные числа. Важно понимать, что эти числа являются математической абстракцией техвещественных чисел, которые представимы в архитектуре компьютера.Тип Real — это те числа, с которыми работают математики. Следовательно, они включают и все вещественные числа, представимые в какойугодно архитектуре компьютера. Например, в этом типе есть число «квадратный корень из двух».Тип Bool содержит булевские значения true и false.Тип Char содержит все возможные отдельные символы.
Этот типне привязан ни к одной из кодировок (поскольку этот тип — лишь математическая абстракция). Этот тип содержит все мыслимые символы.Поэтому не определена операция получения «кода символа», привычнаядля многих языков программирования.Тип Text является массивом символов (о массивах см.ниже).Тип Unit является специальным и используется для ограниченного количества случаев (см.ниже). Основное применение — то же, какоеимеет ключевое слово void в сигнатурах функций языка Си.12Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)Операции над встроенными типамиАрифметические:123456789value+: Int × Int → Int ,−: Int × Int → Int ,* : Int × Int → Int ,∼/ : Int × Int → Int ,∼\ : Int × Int → Int ,∼↑ : Int × Int → Int ,abs : Int → Nat ,real : Int → Real ,1011121314151617+: Real × Real → Real ,−: Real × Real → Real ,* : Real × Real → Real ,∼/ : Real × Real → Real ,∼↑ : Real × Real → Real ,abs : Real → Real ,int : Real → Int ,1819202122××××IntIntIntInt→→→→<:≤:>:≥:IntIntIntIntBool ,Bool ,Bool ,Bool ,<:≤:>:≥:RealRealRealReal∼:∧:∨:⇒:Bool→ Bool ,Bool × Bool → Bool ,Bool × Bool → Bool ,Bool × Bool → Bool ,2324252627××××RealRealRealReal→→→→Bool ,Bool ,Bool ,Bool ,2829303132Для любого типа определены операции сравнения на равенство:1type T1.3.
Аппликативное описание операций23413value= : T × T → Bool ,̸= : T × T → BoolПорядок вычисления операций строго определен: сначала первый аргумент, затем, если необходимо, второй и т.д.Логика короткая. Это означает, например, что если первый аргументконъюнкции равен false, то второй аргумент не вычисляется и вся конъюнкция принимает значение false.Задачито, что было в задачнике Кузьменковой (запись выражений над предопределенными типами)1.3Аппликативное описание операцийRSL не является языком программирования. Однако он позволяетв некоторых несложных случаях написать определение операций в аппликативном (функциональном) стиле. Кроме этого, операции можнореализовать в императивном стиле (этому посвящен раздел 1.4).Рассмотрим простую модель стека: Stack = Nat (количество элементов в стеке).
Тогда операции можно определить так:12scheme STACK = c l a s stype Stack = Nat , Element345valueempty : Stack = 0 ,6push : Stack × Element → Stackpush ( s , e ) ≡ s +1,789∼pop : Stack → Stackpop ( s ) ≡ s−1101112endМожно использовать рекурсию (и, при желании, лямбда-абстракцию):14123456Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)value∼gcd : Nat × Nat → Natgcd ( a , b ) ≡i f a > b then gcd ( b , a )e l s i f a = 0 then be l s e gcd ( a , b−a ) endТак можно записать определение функции, возвращающей несколькозначений:1234valueminmax : Nat × Nat → Nat × Natminmax ( a , b ) ≡i f a > b then ( b , a ) e l s e ( a , b ) end1.4Императивное описание операцийТеперь посмотрим, как записать определение операции в императивном стиле. Так можно записать псевдокод алгоритма Евклида:1scheme GCD = c l a s s23variable a : Nat , b : Nat45678910111213value∼e u c l i d : Unit → write a , b Nateuclid () ≡while a > 0 ∧ b > 0 doi f a > b then a := a − be l s e b := b − a endend ;i f a = 0 then b e l s e a endendКак видно, язык RSL предлагает использовать такие известные понятия как глобальные переменные, присваивание, последовательностиоператоров, условный оператор if-then-elsif-else-end, операторы циклов (while), но это ещё не всё.
Заметьте, если операции нужно получитьдоступ к переменной, то это надо указать в сигнатуре операции при помощи ключевого слова write (и read, см. ниже).1.4. Императивное описание операций15Глобальные переменныеПеременные, определенные вне функции, являются глобальными. Каждая глобальная переменная должна быть определена в разделе variable,а в сигнатуре функции должен быть указан режим работы функции спеременной: «только по чтению» или «по записи-чтению». Функции разрешено оперировать лишь с теми глобальными переменными, которыеуказаны в сигнатуре.
Обращаться к глобальным переменным (даже просто по чтению), не упомянутым в сигнатуре, запрещается. Например,123456scheme S1 = c l a s svariable s t a t u s : Textvalue∼i n i t : Unit → write s t a t u s Uniti n i t ( ) ≡ ( s t a t u s := " i n i t i a l i z e d ")endФункция init не имеет аргументов — для указания этого факта передстрелкой в сигнатуре функции указан тип Unit. Также у функции нети результатов. Однако функции разрешено иметь побочный эффект ввиде изменения значения глобальной переменной status.Еще пример:1234567scheme S2 = c l a s svariable s t a t u s : Textvalue∼is_initialized : Unit → read s t a t u s Boolis_initialized ( ) ≡( s t a t u s = " i n i t i a l i z e d ")endЗдесь глобальная переменная лишь читается в функции, поэтому всигнатуре переменная status указана с модификатором read.Можно указать в сигнатуре, что функция может читать или изменятьлюбую глобальную переменную.
В этом случае надо после слов writeили read вместо имени переменной написать ключевое слово any:12345scheme S3 = c l a s svariable a , b : Natvaluesum : Unit → read any Natsum ( ) ≡ a + b166Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)endТело функции1234567891011123456789101112Язык RSL позволяет задавать выполнение функции в виде последовательности операторов (операторы разделяются точкой с запятой),условного оператора, операторов цикла, оператора выбора case:scheme S3 = c l a s svariable a , b : Natvalueswap : Unit → write a , b Unitswap ( ) ≡(a := a + b ;b := a − b ;a := a − b ;)endЕсли функции нужно вернуть некоторое значение, последовательность операторов должна завершаться выражением, чей результат будетрезультатом работы функции:scheme S4 = c l a s svariable a , b : Natvalueswap : Unit → write a , b Natswap ( ) ≡(a := a + b ;b := a − b ;a := a − b ;a + b)endСреди операторов, объединяемых в последовательность операторов,может быть присваивание, вызов функций, чей возвращаемый тип Unit,условный оператор, оператор цикла.1.4.
Императивное описание операцийУсловный оператор:123456789101112131415scheme S4 = c l a s svariable a , b : Nat , s : Textvaluemax : Unit → read a , b , write s Natmax ( ) ≡(i f a > b thens := " f i r s t " ;aelses := " second " ;bend)endУсловный оператор с веткой elsif :123456789101112131415161718scheme S4 = c l a s svariable x : Int , s : TextvalueAbs : Unit → read x , write s NatAbs ( ) ≡(i f x > 0 thens := " p o s i t i v e " ;xe l s i f x = 0 thens := " z e r o " ;0elses := " n e g a t i v e " ;−xend)endОператоры циклов (while, do-until и for):1variable a : Nat , b : Nat1718234567891234567812345678123456789Глава 1. RAISE SPECIFICATION LANGUAGE (RSL)value∼e u c l i d : Unit → write a , b Nateuclid () ≡while a > 0 ∧ b > 0 doi f a > b then a := a − be l s e b := b − a endend ;i f a = 0 then b e l s e a endvariable n : Nat , x : Natvalue∼d i g i t s : Unit → write n , x Natdigits () ≡n := 0 ;do n := n + 1 ; x := x / 10while x = 0 ;nvariable sum : Natvalue∼sumN : Nat → write sum UnitsumN( n ) ≡sum := 0 ;for i in ⟨ 1 .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
