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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 7)

Для устранения обнаруженной ошибки в нашем случае воспользуйтесь первым способом, введите с клавиатуры в текущую позицию области ввода имя T и нажмите клавишу RETURN. Полученный вид экрана иллюстрирует рисунок 9.

Рис. 9

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

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

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

Рис. 10

1. Завершение редактирования модуля

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

Рис. 11

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

• вставка нового элемента между указанными элементами списка – выделить с помощью мыши место вставки нового элемента (два соседних элемента списка) и щелкнуть левой кнопкой мыши на разделителе элементов (на запятой в нашем случае);

• вставка нового элемента перед указанным элементом списка – выделить с помощью мыши нужный элемент списка и нажать комбинацию клавиш ESC ^B;

• добавить новый элемент в конец списка – выделить последний элемент списка и нажать комбинацию клавиш ESC RETURN.

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

Для определения константы выберите в списке альтернатив метапеременную explicit_value_def, а затем с помощью описанных выше операций добавьте в список описаний функций два новых гнезда value_def, уточнив каждое из них метапеременной explicit_function_def. Обратите внимание на то, что у последней описанной в модуле QUEUE функции должно быть предусловие, для этого выделите в описании последней функции гнездо value_expr и нажмите клавишу RETURN. Вид экрана после выполнения всех этих операций представлен на рисунке 12.

Рис. 12

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

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

Ответы и решения к упражнениям главы 1

1.1. (a) да

1. да

2. нет

3. нет

4. да

5. нет

6. нет

7. да

8. да

9. нет

10. да

1.2. (a) false (по свойству (1) раздела 1.1.2.)

1. 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  a

1.3. (a) да (для данного i выбираем j  i)

(b) нет (не верно, например, для i  0)

1. нет

1.4.  i : Int •  j : Int • j  i или ( i : Int •  j : Int • i  j)

1.5. is_even : Nat  Bool

is_even(n)  ( m : Nat • n  2  m)

или альтернативное определение:

is_even : Nat  Bool

is_even(n)  n \ 2  0

2.1. (a) type Complex  Real  Real

1. value zero : Complex  (0.0,0.0)

2. value c : Complex • let (x,y) = c in x = y end

3. value

add : Complex  Complex  Complex

add((x₁,y₁), (x₂,y₂))  (x₁  x₂, y₁  y₂),

mult : Complex  Complex  Complex

mult((x₁,y₁), (x₂,y₂))  (x₁  x₂  y₁  y₂, x₁  y₂  y₁  x₂)

1. value

f : Complex  Complex

f(c₁) as c₂ post c₁  c₂

2.2. (a) type

Circle  Center  Radius,

Center  Position,

Radius = { r : Real • r  0.0 }

1. value

on_circle : Circle  Position  Bool

on_circle((c,r), p)  distance(c,p) = r

или альтернативное определение:

value

on_circle : Circle  Position  Bool

on_circle(circ, p) 

let

(c,r) = circ

in

distance(c,p) = r

end

1. value

circle : Circle = (origin, 3.0)

1. value

pos : Position • on_circle(circle, pos)

2.3. (a) value

max : Int  Int  Int

max(i,j)  if i  j then i else j end

1. value

max : Int  Int  Int

max(i,j) as y

post (y = i  y  j)  (y  j  y  i)

1. value

max : Int  Int  Int

axiom

 i,j : Int • max(i,j)  if i  j then i else j end

2.4. value

approx_sqrt : Real  Real  Real

approx_sqrt(x, eps) as s

post s  2  x  x  (s  eps)  2

pre x  0.0  eps  0.0

1. Описание:

value

f : Int  Int

f(x)  f(x)

является краткой формой описания:

value

f : Int  Int

axiom

 x : Int • f(x)  f(x),

которое в силу истинности аксиомы эквивалентно:

value

f : Int  Int

Следовательно, исходному описанию удовлетворяют все частично вычислимые (в частности, всюду вычислимые) функции из Int в Int.

3.1. {1,3,5,7,9} или {s  s : Nat • (s  10)  ( n : Nat • s  2  n)}

3.2. scheme

UNIVERSITY_SYSTEM =

class

type

Student,

Course,

CourseInfo = Course  Student-set,

University = Student-set  CourseInfo-set

value

allStudents : University  Student-set

allStudents(ss, cis)  ss,

hasCourse : Course  University  Bool

hasCourse(c, (ss, cis)) 

( (c, ss) : CourseInfo • (c, ss)  cis  c = c),

numberOK : University  Bool

numberOK(ss, cis) 

( (c, ss) : CourseInfo • (c, ss)  cis 

(card ss  100  card ss  5)),

studOf : Course  University  Student-set

studOf(c, (ss, cis)) 

{s  s : Student •  ss : Student-set • s  ss  (c, ss)  cis }

pre hasCourse(c, (ss, cis)),

attending : Student  University  Course-set

attending(s, (ss, cis)) 

{c  c : Course •  ss : Student-set • (c, ss)  cis  s  ss}

pre s  allStudents(ss, cis),

newStud : Student  University  University

newStud(s, (ss, cis))  (ss  {s}, cis) pre s  ss,

dropStud : Student  University  University

dropStud(s, (ss, cis)) 

(ss \ {s}, {(c, ss \ {s})  (c, ss) : CourseInfo • (c, ss)  cis })

pre s  ss

end

4.1. type Elem

value

1. length : Elem^*  Int

length(k)  if k   then 0 else 1  length(tl k) end

или

length : Elem^*  Int

length(k)  card (inds k)

или

length : Elem^*  Int

length(k) 

case k of

  0,

i ^ lr  length(lr)  1

end

1. 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 .. len k

или

rev : Elem^*  Elem^*

rev(k) 

case k of

  ,

i ^ lr  rev(lr) ^ hd k

end

1. type N1  { n : Nat • n  1 }

value

pascal : N1  (N1^*)^*

pascal(n) 

if n  1 then 1

else

let p  pascal(n  1) in

Характеристики

Список файлов книги