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

Полученный вид экрана иллюстрирует рисунок 5.Еще раз нажмите клавишу RETURN (при этом в поле подсказкипоявится список альтернатив для гнезда decl_string) и выберите в полеподсказки альтернативу type_decl. Эффект выполнения данных действийпоказан на рисунке 6.36Рис. 5Рис. 637Теперь в выделенной позиции наберите на клавиатуре имя типа Element(при этом редактор переходит в текстовый режим) и нажмите клавишуRETURN.

По нажатию данной клавиши редактор возвращается в режимсинтаксически управляемого редактирования (поскольку введенный фрагментбыл синтаксически правильным) и на экране появляется следующее в порядкеобхода дерева гнездо редактирования (см. рис. 7).Рис. 73.4.Обработка ошибок редактированияРассмотрим теперь обработку ошибок редактирования. Для этого введите ввыделенной области некоторый текст, содержащий ошибку, например,синтаксически неверное определение типа в виде фрагмента Queue = инажмите клавишу RETURN. Вид экрана после выполнения этих действийиллюстрирует рисунок 8.38Рис. 8Как видно из этого рисунка, в командной строке появляется сообщение осинтаксической ошибке, редактор продолжает оставаться в текстовом режиме икаретка располагается в месте обнаружения ошибки. Устранить такую ошибкуможно двумя способами.

Во-первых, можно, оставаясь в текстовом режиме,отредактировать область ввода таким образом, чтобы она содержаласинтаксически правильный фрагмент. Во-вторых, можно выполнить командуundo из пункта edit командного меню, возвращающую редактор изтекстового режима в режим синтаксического управления (при этом редакторвозвращается в то состояние, в котором он находился до перехода в текстовыйрежим) и дальнейшее редактирование продолжать уже в синтаксическиуправляемом режиме. Второй способ наиболее удобен в тех ситуациях, когдапользователь нечетко помнит синтаксис языка и ему трудно устранить ошибкупрямым редактированием текста.Для устранения обнаруженной ошибки в нашем случае воспользуйтесьпервым способом, введите с клавиатуры в текущую позицию области ввода имяT и нажмите клавишу RETURN.

Полученный вид экрана иллюстрируетрисунок 9.39Рис. 9Отображенное на рисунке 9 состояние редактора показывает, что введенныйна предыдущем шаге редактирования фрагмент описания типа былсинтаксически правильным, поэтому редактор вышел из текстового режима (понажатию клавиши RETURN) и на экране появилось новое гнездоредактирования, соответствующее следующей в порядке обхода дереваметапеременной. Однако поскольку тип T не объявлен в данном модуле,редактор фиксирует ошибку описания типа, о чем свидетельствует выдаваемаяим диагностика и значение счетчика ошибок в строке статуса.Для устранения ошибок такого рода надо выделить с помощью мышинекорректную с точки зрения описания типа конструкцию (в нашем случае имяT) и выполнить команду cut-to-clipped из пункта edit командного меню.

Врезультате выполнения этой команды выделенная конструкция удаляется изтекста модуля и вместо нее появляется соответствующее гнездо редактирования(в нашем случае type_expr), которое и объявляется текущим. Аналогичныйрезультат был бы получен при выполнении команды delete_selection из тогоже пункта командного меню. Заметим, что команда undo не может бытьиспользована в данном случае, т.к.

она вызывается только из текстового режимаредактора.В качестве следующего этапа редактирования завершим определение типаQueue как конечного списка из элементов типа Element. Для этого выберите всписке альтернатив для текущего гнезда редактирования сначала альтернативуlist_type_expr и затем finite_list_type_expr.

После этого в текстовом режиме40наберите имя Element и нажмите клавишу RETURN. Вид экрана послевыполнения указанных операций показан на рисунке 10.Рис. 103.5.Завершение редактирования модуляТеперь в модуле полностью закончено описание типов и можно переходитьк описанию функций. Для этого нажмите клавишу RETURN, чтобы на экранепоявилось гнездо редактирования для нового раздела объявлений (см. рис. 11) ивыберите в списке альтернатив метапеременную value_decl . При этом наэкране появляется заголовок раздела описания функций value и гнездоредактирования value_def для описания очередной функции.41Рис. 11В разделе описаний функций нашего модуля QUEUE должнынаходиться описания константы и двух функций, следовательно, полезно уметьвставлять в уже существующий список описаний новый элемент на то или иноеместо по желанию разработчика спецификации.

Для выполнения подобныхопераций в редакторе предусмотрены следующие возможности:• вставка нового элемента между указанными элементами списка – выделить спомощью мыши место вставки нового элемента (два соседних элементасписка) и щелкнуть левой кнопкой мыши на разделителе элементов (назапятой в нашем случае);• вставка нового элемента перед указанным элементом списка – выделить спомощью мыши нужный элемент списка и нажать комбинацию клавишESC ^B;• добавить новый элемент в конец списка – выделить последний элементсписка и нажать комбинацию клавиш ESC RETURN.Последние два способа добавления элемента в список основаны на том, чтонажатие определенной комбинации управляющих клавиш меняет порядокдвижения по абстрактному синтаксическому дереву при переходе к очередномугнезду редактирования.Для определения константы выберите в списке альтернативметапеременную explicit_value_def, а затем с помощью описанных вышеопераций добавьте в список описаний функций два новых гнезда value_def,уточнив каждое из них метапеременной explicit_function_def.

Обратите42внимание на то, что у последней описанной в модуле QUEUE функциидолжно быть предусловие, для этого выделите в описании последней функциигнездо value_expr и нажмите клавишу RETURN. Вид экрана послевыполнения всех этих операций представлен на рисунке 12.Рис. 12На этом завершим сеанс работы с редактором. Перед выходом из редакторанеобходимо сохранить построенный модуль в текущей директории. Для этоговыполните команду write-file из пункта save командного меню. По даннойкоманде текст модуля будет записан в файл с именем QUEUE.rsl . Выход изредактора осуществляется по команде exit.

После выхода из редакторатекущая директория будет содержать наряду с файлом QUEUE.rsl ещенесколько скрытых файлов со служебной информацией редактора для данногомодуля.Продолжить редактирование модуля можно в следующих сеансах работы,для чего следует указать имя файла с текстом модуля (в нашем случае QUEUE)в качестве параметра при вызове редактора.

Читателям предлагается в качествеупражнения по использованию редактора eden довести до конца построениетекста данного модуля.43Ответы и решения к упражнениям главы 11.1.(a)(b)(c)(d)(e)(f)(g)(h)(i)(j)(k)1.2.(a) false (по свойству (1) раздела 1.1.2.)(b) aРешение: if a then ∼( a ≡ chaos) else false end ≡ (по свойству (3))if a then ∼( true ≡ chaos) else false end ≡if a then true else false end ≡ (по свойству (3))if a then a else a end ≡ a1.3.(a) да (для данного i выбираем j = −i)(b) нет (не верно, например, для i > 0)(c) нет1.4.∀ i : Int • ∃ j : Int • j > i1.5.is_even : Nat → Boolis_even(n) ≡ (∃ m : Nat • n = 2 ∗ m)или альтернативное определение:is_even : Nat → Boolis_even(n) ≡ n \ 2 = 02.1.даданетнетданетнетдаданетдаили∼(∃ i : Int • ∀ j : Int • i ≥ j)type Complex = Real × Realvalue zero : Complex = (0.0,0.0)value c : Complex • let (x,y) = c in x = y endvalueadd : Complex × Complex → Complexadd((x1,y1), (x2,y2)) ≡ (x1 + x2, y1 + y2),mult : Complex × Complex → Complexmult((x1,y1), (x2,y2)) ≡ (x1 ∗ x2 − y1 ∗ y2, x1 ∗ y2 + y1 ∗ x2)(e) valuef : Complex → Complexf(c1) as c2 post c1 ≠ c2(a)(b)(c)(d)442.2.(a) typeCircle = Center × Radius,Center = Position,Radius = {| r : Real • r ≥ 0.0 |}(b) valueon_circle : Circle × Position → Boolon_circle((c,r), p) ≡ distance(c,p) = rили альтернативное определение:valueon_circle : Circle × Position → Boolon_circle(circ, p) ≡let(c,r) = circindistance(c,p) = rend(c) valuecircle : Circle = (origin, 3.0)(d) valuepos : Position • on_circle(circle, pos)2.3.(a)valuemax : Int × Int → Intmax(i,j) ≡ if i ≥ j then i else j end(b) valuemax : Int × Int → Intmax(i,j) as ypost (y = i ∧ y ≥ j) ∨ (y = j ∧ y ≥ i)(c) valuemax : Int × Int → Intaxiom∀ i,j : Int • max(i,j) ≡ if i ≥ j then i else j end2.4.valueapprox_sqrt : Real × Real −∼→ Realapprox_sqrt(x, eps) as spost s ↑ 2 ≤ x ∧ x < (s + eps) ↑ 2pre x ≥ 0.0 ∧ eps > 0.02.5.Описание:valuef : Int −∼→ Intf(x) ≡ f(x)45является краткой формой описания:valuef : Int −∼→ Intaxiom∀ x : Int • f(x) ≡ f(x),которое в силу истинности аксиомы эквивалентно:valuef : Int −∼→ IntСледовательно, исходному описанию удовлетворяют все частично вычислимые (вчастности, всюду вычислимые) функции из Int в Int.3.1.{1,3,5,7,9} или {s | s : Nat • (s < 10) ∧ (∃ n : Nat • s = 2 ∗ n)}3.2.schemeUNIVERSITY_SYSTEM =classtypeStudent,Course,CourseInfo = Course × Student-set,University = Student-set × CourseInfo-setvalueallStudents : University → Student-setallStudents(ss, cis) ≡ ss,hasCourse : Course × University → BoolhasCourse(c, (ss, cis)) ≡(∃ (c′, ss′) : CourseInfo • (c′, ss′) ∈ cis ∧ c = c′),numberOK : University → BoolnumberOK(ss, cis) ≡(∀ (c, ss′) : CourseInfo • (c, ss′) ∈ cis ⇒(card ss′ ≤ 100 ∧ card ss′ ≥ 5)),studOf : Course × University −∼→ Student-setstudOf(c, (ss, cis)) ≡{s | s : Student • ∃ ss′ : Student-set • s ∈ ss′ ∧ (c, ss′) ∈ cis }pre hasCourse(c, (ss, cis)),attending : Student × University −∼→ Course-setattending(s, (ss, cis)) ≡{c | c : Course • ∃ ss′ : Student-set • (c, ss′) ∈ cis ∧ s ∈ ss′}pre s ∈ allStudents(ss, cis),newStud : Student × University −∼→ UniversitynewStud(s, (ss, cis)) ≡ (ss ∪ {s}, cis) pre s ∉ ss,46dropStud : Student × University −∼→ UniversitydropStud(s, (ss, cis)) ≡(ss \ {s}, {(c, ss′ \ {s}) | (c, ss′) : CourseInfo • (c, ss′) ∈ cis })pre s ∈ ssend4.1.type Elemvalue(a) length : Elem* → Intlength(k) ≡ if k = 〈〉 then 0 else 1 + length(tl k) endилиlength : Elem* → Intlength(k) ≡ card (inds k)илиlength : Elem* → Intlength(k) ≡case k of〈〉 → 0,〈i〉 ^ lr → length(lr) + 1end(b) rev : Elem* → Elem*rev(k) ≡ if k = 〈〉 then 〈〉 else rev(tl k) ^ 〈hd k〉 endилиrev : Elem* → Elem*rev(k) ≡ 〈k(len k − i + 1) | i in 〈1 ..