рефераты конспекты курсовые дипломные лекции шпоры

Реферат Курсовая Конспект

Система типов данных

Система типов данных - раздел Программирование, Предикатное программирование Любая Переменная Характеризуется Некоторым Типом. Язык Ccp Является Бестиповы...

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

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

Примитивными типами являются: логический, целый, вещественный и литерный. Для них соответственно будем использовать имена: BOOL, INT, REAL и CHAR. Набор базисных предикатов для примитивных типов соответствует распространенным арифметическим и логическим операциям. Например, базисные предикаты +(x, y: z), -(x, y:z), -(x:y), <(x, y:b) соответствуют операциям z = x + y, z = x - y, y = -x , b = x < y.

Для каждого примитивного типа определены два вида предикатов равенства: =(x: y) и =(x, y: b). Для предиката =(x: y) процессор присваивает переменной y значение переменной x. Для предиката =(x, y: b) процессор определяет значение отношения x = y и присваивает его логической переменной b. Предикат =(d: e) определен также для наборов переменных d и e.

Имеется набор базисных предикатов для задания констант. Предикаты
ConsIntZero( :x) и ConsIntOne( :x) определяют целочисленные значения 0 и 1 в качестве значения переменной x.

Далее в определениях типов T, S, X, Y и Z обозначают имена типов.

Новый тип S как подмножество типа T вводится определением

S = SUBSET(T, x, P, d) . (4.3)

Здесь x - переменная типа T, а d - произвольный, возможно пустой, набор переменных, P - имя предиката. Предикат P(x, d: b) является вычислимым, т. е. должен быть определен на языке CCP. Тип S есть множество истинности предиката P(x, d), т. е. S = {xÎT | P(x, d)}. Переменные набора d являются параметрами типа S. Примером подмножества типа является тип натуральных чисел:

NAT = SUBSET(INT, x, GE0) = {xÎINT | x ³ 0} ,

где GE0 есть имя предиката x ³ 0. Другим примером является диапазон целых чисел:


DIAP(n) = SUBSET(INT, x, IN1_n, n) = {xÎINT | x ³ 1 & x £ n} ,

где IN1_n есть имя предиката x ³ 1 & x £ n.

Структурный тип определяется в виде композиции других типов, называемых компонентными по отношению к структурному. Структурными типами являются: произведение типов (кортеж), объединение типов, множество подмножеств типа и предикатный тип. Базисные предикаты для структурного типа подразделяются на конструкторы, деструкторы и другие операции со значениями типа. Конструктор по значениям компонентных типов строит значение структурного типа. Деструктор для значения структурного типа определяет соответствующие значения компонент.

Произведение типов

Z = X ´ Y (4.4)

определяет тип Z в виде множества кортежей (x, y), т. е. Z = {(x, y) | x Î X, y Î Y}. Конструктором является предикат ConsStruct(x, y:z), где x Î X, y Î Y и z Î Z, а деструктором - CompStruct(z:x, y). Для конструктора и деструктора истинно отношение z = (x, y).

Объединение [13] типов

Z = X + Y (4.5)

определяет множество элементов вида (1, x) и (2, y) для типов X и Y, т. е. Z = {(1, x) | x Î X} È {(2, y) | y Î Y}. Первая компонента в этих кортежах (1 или 2) является тегом значения. Конструктор ConsUnion1(x:z) строит структурное значение z по некоторому x Î X, т. е. z = (1, x). Аналогично, для конструктора ConsUnion2(y:z) имеет место z = (2, y). Деструктор CompUnion(z:i, x, y) для z Î Z определяет, что либо z = (1, x) и i = 1, либо z = (2, y) и i = 2. Если i = 1, то значение y не определено. Если i = 2, то значение x не определено.

Множество подмножеств

Z = SET(X) (4.6)

для конечного типа X есть Z = {z | z Í X}. Конструктор ConsSetEmpty( :z) определяет пустое множество в качестве значения переменной z. Конструктор ConsSetElem(x :z) определяет z = {x} для x Î X. Предикат CompSet(z, x:b) определяет истинность формулы x Î z.

Предикатный тип

Z = PRED(D: E) (4.7)

есть множество вычислимых предикатов вида j(d: e) для непересекающихся наборов переменных d и e, причем набор d может быть пустым. Типы переменных определяются соответствующими наборами типов D и E. Таким образом, Z = {j(d: e) | d Î D, e Î E, j Î CCP}. Конструктор предиката ConsPred описан в разд. 4.8.

Допустим, набор d не пустой, типы набора D являются конечными, а произвольный предикат j Î Z определен для любого d Î D, т. е. "j Î Z "d Î D $e j(d: e). При этих условиях предикат j(d: e) может трактоваться как массив. Переменные набора d называются индексами массива, а e - элементом массива. Конструктор массива ConsArray описан в разд. 4.9. Деструктор CompArray(j, d: e) определяет элемент e массива j для набора индексов d.

Совокупность типов программы представлена типами переменных, встречающихся в программе. Всякий тип либо является примитивным, либо вводится одним из определений вида (4.3)–(4.7).

Другими типами данных в языке CCP являются последовательности и деревья. Эти типы являются производными, а не базисными. Их определение является рекурсивным и использует произведение и объединение компонентных типов. Следует особо подчеркнуть, что типы указателей (pointers) не принадлежат языку CCP. В этом нет необходимости, поскольку структуры данных, использующие указатели в программе на чистом функциональном языке, могут быть преобразованы в эквивалентные структуры данных с использованием массивов, последовательностей и деревьев. Использование указателей подразумевается в списках для языков семейств ML и Лисп. Формальная семантика типов данных с указателями достаточно сложна.

Дадим примеры рекурсивных типов. Введем специальный тип: NIL = { nil}. Имя nil обозначает пустую последовательность. Тип последовательности, составленной из элементов некоторого типа T, вводится следующими определениями:

Seq = NIL + Seq1;

Seq1 = T ´ Seq.

Здесь тип T является параметром определяемого типа Seq. При использовании типа Seq в правой части определения другого типа в скобках указывается конкретный тип - параметр. Например, строковый тип как последовательность литер имеет определение

STRING = Seq(CHAR).

Тип списка LIST для языка Лисп представляется следующим набором определений:

LIST = Seq(ATOM);

ATOM = NIL + NUM + SYMBOL + LIST;

NUM = INT + REAL;

SYMBOL = STRING.

Определим семантику рекурсивно определяемых типов данных. Рассмотрим следующую систему определений типов:

Xk = φk(X1, X2,…, Xn, T1, T2,…, Ts); k = 1,…,n; n > 0; s ³ 0 . (4.8)

Здесь X1, X2,…, Xn - имена определяемых типов; φk - типовый терм вида Y ´ Z или Y + Z, где в качестве Y и Z могут быть типы X1, X2,…, Xn, T1, T2,…, Ts. Определения типов T1, T2,…, Ts не зависят от X1, X2,…, Xn. Например, система определений для типа LIST включает:

LIST = SeqATOM;

SeqATOM = NIL + Seq1;

Seq1 = ATOM ´ SeqATOM;

ATOM = NIL + NUM + SYMBOL + LIST.

Систему определений рекурсивных типов (4.8) перепишем в векторной форме:

X = φ(X) , (4.9)

где X = (X1, X2,…, Xn) - вектор типов и φ = (φ1, φ2,…, φn) - вектор типовых термов. Введем отношение ⊑ на векторах типов:

X ⊑ Y @ "k=1..n (Xk Í Yk).

Отношение Í определяет нижнюю полурешетку на множестве всех типов с пустым типом Æ в качестве минимального элемента. Вектор типов Q = (Æ, Æ,…, Æ) является минимальным элементом полурешетки, определяемой отношением ⊑ на множестве векторов типов.

Рассмотрим последовательность векторов типов {Xm}m³0, определяемую рекуррентно следующим образом:

X0 = Q, Xm+1 = φ(Xm), m ³ 0. (4.10)

Естественно ожидать, что предел последовательности {Xm}m³0 (если он существует) даст нам неподвижную точку - решение системы (4.9). Рассмотрим построение неподвижной точки для рекурсивного типа Seq. Получим следующую последовательность типов:

Seq0 = Æ;

Seq1 = NIL + (T ´ Seq0) = NIL + Æ = {1} ´ NIL È {2} ´ Æ = {(1, nil)};

Seq2 = NIL + {(t, (1, nil))}, где t Î T;

Seq3 = NIL + ({t2} ´ (NIL + {(t1, (1, nil))})) , где t1, t2 Î T, и т. д.


Лемма 4.1. Функция φ системы (4.9) определений рекурсивных типов X = φ(X) является непрерывной относительно произведения и объединения. Понятие непрерывности функций определено в разд. 3.1. Отметим, термы вида SUBSET, SET и PRED могут встречаться в системе (4.9), но они не могут участвовать в рекурсии. Например, недопустима рекурсия вида Z = SET(Z).

Доказательство. Докажем, что произведение Y ´ Z и объединение Y + Z непрерывны относительно вхождений компонентных типов Y и Z. Пусть {Ym}m³0 и {Zm}m³0 - возрастающие цепи типов. Требуется доказать, что

Èm³0(Ym ´ Zm) = (Èm³0Ym) ´ (Èm³0Zm).

Докажем сначала, что тип левой части равенства содержится в типе правой части. Пусть (y, z) Î Èm³0(Ym ´ Zm). Существует такое k, что (y, z) Î Ym ´ Zm для всех m ³ k. Тогда y Î Ym и z Î Zm для m ³ k. Далее, y Î Èm³0Ym и zÎ Èm³0Zm. И, как следствие, (y, z) Î (Èm³0Ym) ´ (Èm³0Zm). Допустим теперь, что (y, z) Î (Èm³0Ym) ´ (Èm³0Zm), и докажем, что (y, z) Î Èm³0(Ym ´ Zm).
Из определения произведения y Î Èm³0Ym и z Î Èm³0Zm. Существуют такие k1 и k2, что y Î Ym для m ³ k1 и z Î Zm для m ³ k2. Пусть k = max(k1, k2). Тогда (y, z) Î Ym ´ Zm для всех m ³ k. Далее, (y, z) Î Èm³0(Ym ´ Zm). Непрерывность произведения доказана. Непрерывность объединения доказывается аналогичным образом.

Непрерывность функции φ доказывается следующей цепочкой равенств:

Èm³0φ(Bm) = Èm³01(Bm), …, φn(Bm)) = (Èm³0φ1(Bm), …, Èm³0φn(Bm)) = = (φ1(Èm³0Bm), …, φn(Èm³0Bm)) = φ(Èm³0Bm). □

В соответствии с теоремой Клини о неподвижной точке (см. разд. 3.1) решением системы X = φ(X) является наименьшая неподвижная точка функции φ, т. е. Èm³0Xm, где X0 = Q, Xm+1 = φ(Xm).

Для построения последовательностей и деревьев вполне достаточно рекурсии с использованием произведения и объединения. Возможны другие, экзотические, формы рекурсии, однако они бесполезны при разработке реальных алгоритмов. Некоторые из них анализируются в книге [3].

– Конец работы –

Эта тема принадлежит разделу:

Предикатное программирование

Новосибирский государственный университет.. факультет информационных технологий..

Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Система типов данных

Что будем делать с полученным материалом:

Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:

Все темы данного раздела:

Новосибирск
  УДК 004.432.42 ББК 22.183.492 Ш 427   Шелехов В. И. Предикатное программирование: Учеб. пособие / Новосиб. гос. ун-т. Новосибирск, 2009

Язык исчисления вычислимых предикатов,
его логическая и операционная семантика .......................................................... 27 4.1. Структура программы на языке CCP ...............................

Семантика языка предикатного программирования.
Методы доказательства корректности предикатных программ ...................... 47 5.1. Язык P1: подстановка определения предиката на место вызова .........................

Общее понятие программы
Понятие программы обычно определяется в контексте некоторого языка программирования. Представление об общем понятии программы, абстрагированное от конкретного языка программирования, для специалист

Автоматическая вычислимость
Развитие средств вычислений сопровождается все большей степенью автоматизации вычислений. Потребность в проведении сложных и длительных расчетов привела человека к необходимости создания и совершен

Спецификация программы
Для определения связи программы со своей спецификацией рассмотрим следующую модель применения программы (рис. 1). Вычисление по программе является необходимым звеном в цепочке действий некоторого р

Формы спецификации программы
Распространена точка зрения, что спецификацию программы можно представить в виде функции. Поскольку это не всегда так, возникает вопрос о классификации форм, которые может принимать спецификация пр

Корректность программ с предикатной спецификацией
Для класса программ с предикатной спецификацией рассматривается программа вместе со своей спецификацией. Введенное в предыдущем разделе понятие предикатной спецификации уточняется следующим образом

Предикатная спецификация программы
Уточним и дополним понятие предикатной спецификации, определенное в разд. 1.2. Рассмотрим следующую простую схему взаимодействия программы с окружением: ввод входных данных происходит перед началом

Логическая семантика языка программирования
Всякая программа содержит логику. Это, например, бизнес-логика, извлекаемая нетривиальным анализом из текста программы в процессе реинжиниринга программы [16]. Это также логические формулы, получае

Модель корректности программы
Рассмотрим программу с предикатной спецификацией на языке, для которого можно построить логическую семантику. Программа со спецификацией представляется в виде тройки Хоара: {P(x)} S {Q(x,

Система правил вывода программы из спецификации
Понятие корректности программы, введенное в разд. 2.3, состоит из трех условий (2.7–2.9). Главным из них является условие (2.7) соответствия программы и спецификации, согласно которому постусл

Однозначность предикатов
Предикат H(x, y) является однозначным в области X для набора переменных x, если он определяет функцию, отображающую значения набора x в значения набора y. Должно быть истинным следующее усло

Теорема тождества спецификации и программы
Теорема определяет условия, при которых программа может быть выведена из спецификации. Теорема 2.1 тождества спецификации и программы. Рассмотрим программу со специфи

Отношения порядка
R называется бинарным отношением на множестве D, если R Í D ´ D. Утверждение (a, b) Î R принято записывать в виде a R b. Для произвольного отношения R используются следующ

Наименьшая неподвижная точка
Далее будем считать, что (D, ⊑, ⊥) – полная решетка с наименьшим элементом, т. е. "a Î D. ⊥⊑ a. Пусть F: D→D - произвольная тотальная (т. е. всюду

Математическая индукция
Математическая индукция – это метод доказательства некоторого утверждения P(n) для всех значений натурального параметра n; n = 0, 1, 2, … . Доказательство проводится по следующей схеме.

Его логическая и операционная семантика
Нас интересуют языки программирования, допускающие построение логической семантики. Во-первых, следует исключить из рассмотрения языки для реактивных систем, определяющих взаимодействующие параллел

Структура программы на языке CCP
Язык CCP (Calculus of Computable Predicates) - язык исчисления вычислимых предикатов, определяющий множество вычислимых формул исчисления предикатов. К языку предъявляются два требования: по

Логическая и операционная семантика языка CCP
Логическая семантика есть функция LS, сопоставляющая каждой конструкции S языка CCP некоторую формулу LS в исчислении предикатов, т. е. LS(S) = LS. Пусть j(d:

Семантика вызова предиката
Пусть имеется вызов предиката A(z:u) . (4.12) Здесь A есть имя предиката или имя переменной предикатного типа; z - возможно пустой набор имен переменных; u - непу

Конструктор предиката
Конструктор предиката является базисным предикатом ConsPred(x, B: A), где x - возможно пустой набор переменных; B - имя предиката; A - имя переменной предикатного типа. Значением п

Конструктор массива
Конструктор массива является базисным предикатом ConsArray(x, B: A), где x - возможно пустой набор переменных, B - имя предиката, отличное от ConsPred и ConsArray. Значением переме

Программа
Программа на языке CCP состоит из конечного набора определений предикатов. Для каждого определения правой частью является оператор суперпозиции (4.16), параллельный оператор (4.19) или услов

Рекурсивные определения предикатов
Для определяемых предикатов B и C отношение depend(B, C) обозначает непосредственную зависимость B от C, если в правой части определения B имеется вызов предиката C. Предикат B определяет

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

Методы доказательства корректности рекурсивных программ
Рассмотрим следующую конкретизацию системы (4.36) определений рекурсивного кольца предикатов A1, A2,…, An: Aj(t, xj:

Лексемы
Текст программы представлен в виде последовательности строк символов. Переход на новую строку эквивалентен символу «пробел». Программа может содержать комментарии, текст которых считается не принад

Определение предиката
ОПРЕДЕЛЕНИЕ-ПРЕДИКАТА ::= ИМЯ-ПРЕДИКАТА ОПИСАНИЕ-ПРЕДИКАТА ИМЯ-ПРЕДИКАТА ::= ИДЕНТИФИКАТОР Значением ОПИСАНИЯ-ПРЕДИКАТА является предикат, обозначаемый именем предиката.

Спецификация предиката
Предикат, используемый в программе, должен иметь определение предиката. Если предикат определяется в другом модуле программы, то предикат может быть представлен своей спецификацией. СПЕЦИФ

Вызов предиката
Элементарным оператором программы является вызов предиката. ВЫЗОВ-ПРЕДИКАТА ::= ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ | ВЫЗОВ-ПРЕДИКАТА-ГИПЕРФУНКЦИИ ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ ::=

Программа
Программа состоит из одного или нескольких модулей. Модуль определяет независимую часть программы. ОПИСАНИЕ-МОДУЛЯ ::= [ЗАГОЛОВОК-МОДУЛЯ] СПИСОК-ОПИСАНИЙ ЗАГОЛОВОК-МОДУЛЯ ::=

Выражения
ПЕРВИЧНОЕ-ВЫРАЖЕНИЕ ::= КОНСТАНТА | ПЕРЕМЕННАЯ | АГРЕГАТ | ИМЯ-ПРЕДИКАТА | ГЕНЕРАТОР-ПРЕДИКАТА | ВЫЗОВ-ФУНКЦИИ | ( ВЫРАЖЕНИЕ ) | ИМЯ-ТИПА |

Описание типа массива
ИЗОБРАЖЕНИЕ-ТИПА-МАССИВА ::= array ( ИЗОБРАЖЕНИЕ-ТИПА-ЭЛЕМЕНТА , ИЗМЕРЕНИЯ-МАССИВА ) ИЗОБРАЖЕНИЕ-ТИПА-ЭЛЕМЕНТА ::= ИЗОБРАЖЕНИЕ-Т

Вырезка массива
ВЫРЕЗКА-МАССИВА ::= ВЫРАЖЕНИЕ-МАССИВ [ СУЖЕННЫЙ-НАБОР-ТИПОВ-ИНДЕКСОВ ] ВЫРАЖЕНИЕ-МАССИВ ::= ВЫРАЖЕНИЕ СУЖЕННЫЙ-НАБОР-ТИПОВ-ИНДЕКСОВ ::=

Определение массива
ОПРЕДЕЛЕНИЕ-МАССИВА ::= ОПРЕДЕЛЕНИЕ-ИНДЕКСОВ ОПРЕДЕЛЕНИЕ-ЭЛЕМЕНТА-МАССИВА | АГРЕГАТ-МАССИВ | ОПРЕДЕЛЕНИЕ-МАССИВА-ПО-ЧАСТЯМ ОПРЕДЕЛЕНИЕ-МАССИВА-ПО-ЧАСТЯМ ::=

Объединение массивов
Операндами операции «+» объединения массивов: ВЫРАЖЕНИЕ-МАССИВ + ВЫРАЖЕНИЕ-МАССИВ являются выражения, значениями которых являются массивы. Объединяемые массивы до

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

Процессы
Для большинства программ можно построить спецификацию в виде предусловия и постусловия. Однако не всякую программу можно специфицировать таким образом. Имеется класс программ реального времени, в ч

Императивное расширение
Императивное расширение языка P определяет дополнительные языковые конструкции, возникающие в программе в результате проведения трансформаций предикатной программы (см. введение). Использование эти

Технология предикатного программирования
Типичный способ реализации языка программирования заключается в реализации транслятора с языка программирования на язык команд целевой ЭВМ или на некоторый другой реализованный язык программировани

Подстановка определения предиката на место вызова
Пусть A(x: y) { S } - определение предиката на императивном расширении языка P, а A(e: z) - вызов предиката в теле некоторого другого предиката B. Здесь x, y, z обозначают списки переменных, а e -

Замена хвостовой рекурсии циклом
Подстановка определения нерекурсивного предиката на место вызова является эффективной при наличии в программе одного вызова. Подстановка определения рекурсивного предиката усложняет программу и поэ

Склеивание переменных
Трансформация склеивания переменных есть замена в определении предиката нескольких переменных одной. Трансформация определяет список имен переменных. Переменные из указанного списка переменн

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

Трансформация кодирования структурных объектов
Трансформация кодирования структурных объектов реализует представление используемых в программе структурных типов (списков, деревьев и др.) посредством структур более низкого уровня, таких к

Гиперфункции
Пример 7.2. Допустим, для списка s целых чисел требуется извлечь второй элемент и присвоить переменной e. Список может содержать менее двух элементов. Логическая переменная exist =

Else break
} } }; Подставим определения предикатов взятьЧисло и перваяЦифра на место вызовов. Проведем очевидные упрощения. Сумма(string s, nat

Else break
} }; Далее, поскольку внутренний цикл в теле предиката Сумма не имеет нормального выхода, можно заменить оператор #2 на break и убрать скобки оператора продолжени

Else break
} n = n + v } } На четвертом этапе применяется трансформация кодирования строки s вырезкой массива. При этом разные значения списка s представляются вырезками од

Else break
} n = n + v } Можно обнаружить следующий недостаток программы (7.39): если строка s завершается цифрой, то проверка исчерпания строки реализуется

Хотите получать на электронную почту самые свежие новости?
Education Insider Sample
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
Реклама
Соответствующий теме материал
  • Похожее
  • Популярное
  • Облако тегов
  • Здесь
  • Временно
  • Пусто
Теги