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

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

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

SYSTEM_OF_COORDINATES=

class

type

Position = Real  Real

value

origin : Position = (0.0,0.0),

distance : Position  Position  Real

distance((x₁, y₁),(x₂, y₂)) 

((x₂ – x₁)2.0 + (y₂ – y₁)2.0)0.5

end

Здесь тип ‘Position’ предназначен для описания координат точек на плоскости, константа ‘origin’ задает начало координат, функция ‘distance’ определяет способ вычисления расстояния между двумя точками. Обратите внимание на то, что при описании константы ‘origin’ и функции ‘distance’ использован явный стиль описания (explicit definition), т.к. указано непосредственное значение константы и формула для вычисления расстояния.

Используя заданную спецификацию описать:

1. тип ‘Circle’ для описания окружности по ее центру и радиусу;

2. функцию ‘on_circle’, определяющую лежит ли точка с заданными координатами на заданной окружности;

3. окружность с радиусом 3.0 и центром в начале координат;

4. константу ‘pos’ для представления произвольной точки, лежащей на заданной окружности.

Указания:

• в пункте (a) опишите вспомогательные типы ‘Center’ и ‘Radius’ для представления центра окружности и ее радиуса соответственно, для описания типа ‘Center’ используйте тип ‘Position’, для типа ‘Radius’ воспользуйтесь следующим описанием:

Radius = { r : Real • r  0.0 }, задающим подтип действительных чисел с неотрицательными значениями;

• в пунктах (b) и (c) следует воспользоваться явным стилем описания (explicit definition), можно также использовать конструкцию let для достижения большей наглядности записи;

• в пункте (d) используйте неявный (implicit) стиль описания константы.

1. Определить функцию ‘max’, возвращающую значение максимума из двух целых чисел, используя один из следующих стилей описания:

1. явный,

1. неявный,

2. аксиоматический.

Указания:

• воспользуйтесь общей схемой определения функции, изложенной в пункте 1.2.3.5;

• для удобства записи используйте условное выражение языка RSL вида if логическое_выражение then выражение else выражение end.

1. Определить функцию ‘approx_sqrt’, которая с заданной точностью ‘eps’ (положительное вещественное число) находит приближённое значение корня квадратного из неотрицательного вещественного числа. Возвращаемый функцией результат должен быть таким, чтобы точное значение квадратного корня square_root(x) лежало в полуоткрытом интервале [approx_sqrt(x,eps),approx_sqrt(x,eps) + eps[.

Указания:

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

• обратите внимание на то, что функция определена не для всех значений входных параметров, т.е. является частично вычислимой.

1. Рассмотрим следующее описание функции:

value

f : Int  Int

f(x)  f(x)

Какие из перечисленных ниже функций удовлетворяют данному описанию?

(a) value

f : Int  Int

f(x)  chaos

(b) value

f : Int  Int

f(x)  1

(c) value

f : Int  Int

f(x)  1

Указания:

• запишите исходное определение функции в аксиоматическом стиле и с помощью эквивалентных преобразований упростите полученный результат;

• воспользуйтесь тем фактом, что частично вычислимые функции включают в себя всюду вычислимые функции.

1. Множества

Цель данного раздела - познакомить читателя с принятыми в RSL способами описания множеств и основными операциями над множествами. Раздел содержит упражнения по использованию абстракции множеств в моделеориентированных спецификациях.

1. Понятие множества

Множеством называется неупорядоченный набор различных значений одного и того же типа. Например:

{1,3,5}

{Mary,John,Peter}

При этом, как видно из определения множества, записи {1,3,5}, {5,3,1} и {3,5,1,1} определяют одно и то же множество.

Для описания типа множества в RSL предусмотрена конструкция type_expr‑set для конечных множеств и type_expr‑infset для бесконечных, при этом type_expr задает тип входящих в множество элементов. Так, значениями типа Bool‑set являются следующие конечные множества:

{}

{true}

{false}

{true, false},

причем сюда включается пустое множество {}.

Тип type_expr‑infset представляет как конечные, так и бесконечные множества, состоящие из элементов типа type_expr. Следовательно, для любого типа T тип T‑set является подтипом T‑infset. Например, тип Nat‑infset содержит все конечные (в том числе и пустое) и бесконечные множества натуральных чисел.

Для работы с множествами в RSL определены следующие операции: ,,\,,,,,, и card, кроме того можно использовать отношения  и .

Операция card вычисляет размер конечного множества, т.е. количество его элементов:

card : T‑infset  Nat

При применении к бесконечному множеству card возвращает chaos. Например:

card {1,4,56} = 3

card {} = 0

card {n  n : Nat}  chaos

1. Способы определения множеств

Конечное множество может быть задано путем непосредственного перечисления его элементов, как в приведенных выше примерах, в этом случае выражение, определяющее значение множества, имеет вид {v₁,...,v_n}, где n0. Кроме того, для конечных множеств, образованных из целых чисел, возможно также использование диапазона для задания значения множества, причем левая граница диапазона не должна превышать его правую границу (в противном случае множество будет пусто). Например, выражение {3 .. 7} задает множество {3,4,5,6,7}, {3 .. 3} – множество из единственного элемента {3} и  {3 .. 2} – пустое множество {}.

Более общей формой выражения, определяющего значение как конечного, так и бесконечного множества, является выражение вида:

{ value_expr  set_limitation },

называемое сокращенной (compehended) записью множества или сокращенным выражением, где value_expr задает формулу для вычисления значений элементов множества, set_limitation – некоторый предикат, определяющий элементы данного множества. Примером такой формы записи может служить следующее выражение:

{2n  n : Nat • n  3},

с помощью которого задается множество {0,2,4,6}.

Упражнения

1. Написать выражение, задающее значение множества, элементами которого являются нечетные числа в диапазоне от 0 до 10.

Указания:

используйте два способа задания значения множества: непосредственное перечисление его элементов и сокращенное выражение.

1. Пусть база данных университета описана следующим образом (для простоты комментарии приведены на русском языке):

scheme

UNIVERSITY_SYSTEM =

class

type

Student,

Course,

CourseInfo = Course  Student-set,

University = Student-set  CourseInfo-set

value

 allStudents возвращает множество всех студентов, обучающихся в

данном университете 

allStudents : University  Student-set,

 hasCourse проверяет, читается ли данный курс в данном

университете

hasCourse : Course  University  Bool,

 numberOK возвращает значение true, если любой читаемый в

университете курс посещает не менее 5 и не более 100 студентов 

numberOK : University  Bool,

 studOf возвращает множество студентов заданного университета,

посещающих заданный курс 

studOf : Course  University  Student-set,

 attending возвращает множество курсов, которые посещает

заданный студент в указанном университете 

attending : Student  University  Course-set,

 newStud добавляет нового студента к числу студентов заданного

университета 

newStud : Student  University  University,

 dropStud исключает указанного студента из числа студентов

заданного университета 

dropStud : Student  University  University

end

Определите функции, сигнатура которых приведена в данном описании.

Указания:

воспользуйтесь явным стилем описания функций и операциями над множествами.

1. Почему некоторые из перечисленных выше функций частично вычислимы?

1. Списки

Цель данного раздела - познакомить читателя с принятыми в RSL способами описания списков и основными операциями над списками. Раздел содержит упражнения по использованию списков в спецификациях программ.

1. Понятие списка

Списком называется последовательность значений одного и того же типа, например:

1,3,3,1,5

true,false,true

Для списков допустимо использование отношений  и . Порядок следования элементов в списке существенен, т.е. списки 1,3,5 и 5,3,1 являются различными (1,3,5  5,3,1). Кроме того, допускается повторное вхождение элементов в список (как в рассмотренных выше примерах), причем 1,3,3,1,5  1,3,5.

Для описания конечных списков в RSL используется конструкция вида type_expr^*, где type_expr задает тип элементов списка. Например, тип Bool^* описывает любой конечный список (в том числе и пустой) из булевских значений. Конструкция type_expr^ задает тип как конечных, так и бесконечных списков из элементов типа type_expr. Таким образом, для любого типа T, T^* является подтипом T^.

1. Способы определения списков

Для списков применяются те же способы определения значений, что и для множеств. Так, значение конечного списка может быть задано путем непосредственного перечисления его элементов. В этом случае значение списка определяется выражением вида v₁,...,v_n, где n0 и все v_i являются выражениями одного и того же типа, в частности,  задает пустой список. Конечный список из последовательных целых чисел можно задать, указав диапазон изменения значений элементов списка, т.е. выражением вида v₁..v₂, где v₁ и v₂ задают соответственно нижнюю и верхнюю границы диапазона, причем при v₁  v₂ список пуст.

Использование такого способа записи иллюстрируют следующие примеры:

3..7 3,4,5,6,7

3..3  3

3..2  

Значение списка можно задать также по аналогии с множествами и с помощью так называемого сокращенного выражения (comprehended list expression), имеющего вид  value_expr  list_limitation . Этот способ применяется в том случае, когда новый список строится на основе какого-то уже существующего. Здесь value_expr определяет общую формулу для вычисления значений элементов нового списка, list_limitation задает базовый список, на основе которого строится данный, с возможным указанием некоторого предиката для отбора элементов из базового списка.

Например, в выражении:

2n  n in 0 .. 3

базовым является список 0 .. 3, предикат отбора отсутствует и, следовательно, в результате вычисления получается список 0,2,4,6, причем упорядоченность элементов нового списка полностью определяется порядком следования элементов в базовом списке. Примером использования предиката для отбора элементов базового списка может служить выражение:

n  n in 1 .. 100 • is_a_prime(n),

где предикат is_a_prime(n) позволяет определить, является ли n простым числом. С помощью данного выражения задается список, элементами которого являются в возрастающем порядке простые числа из диапазона 1 .. 100, т.е. 2,3,5,7,...,97.

Для доступа к какому-либо отдельному элементу списка в RSL предусмотрено понятие индекса. В качестве индекса используются натуральные числа, причем индексация элементов списка начинается с 1 и для конечных списков заканчивается числом, равным длине списка. Например:

2,5,3(2)  5

2,5,3, 3(1)  2,5,3

2,5,3, 3(1)(2)  2,5,3(2)  5

Значение бесконечного списка может быть задано с помощью аксиом, определяющих правила формирования списка. Так, список, содержащий все натуральные числа в возрастающем порядке, может быть определен следующим образом:

value

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

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