Семантическая теория программ. Семантическая теория программ

• Название: Семантическая теория программ
• Дата: 15.11.2022
• Размер: 172.36 Kb.
• Имя файла: Семантическая теория программ.docx
• Тип: Программа; #789202
• страница: 2 из 4

Декларативная семантика

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

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

Формальное определение семантики становится общепринятой частью определения нового языка. Стандартное описание языка PL/I включает в себя VDL-подобную нотацию, описывающую семантику операторов PL/I, а для языка Ada было разработано определение на основе денотационной семантики. Тем не менее, изучение формальных определений семантики не оказало такого сильного влияния на практическое определение языков, как изучение формальных грамматик — на определение синтаксиса. Ни один из методов определения семантики не оказался по настоящему полезным ни для пользователя, ни для разработчиков компиляторов языков программирования.

Языки формальной спецификации

Языки и методы формальной спецификации, как средство проектирования и анализа программного обеспечения появились более сорока лет назад. За это время было немало попыток разработать как универсальные, так и специализированные языки формальных спецификаций (ЯФС), которые могли бы стать практическим инструментом разработки программ, таким же, как, например, языки программирования. За свою недолгую историю ЯФС уже прошли через несколько периодов подъема и спада. Оценки перспектив ЯФС варьировались от оптимистических прогнозов, предсказывающих появление языков описания требований, по которым будет генерироваться готовое программное обеспечение, до пессимистических утверждений, что ЯФС всегда будут только игрушкой для экспериментов в академических исследованиях. Вместе с тем, хотя сейчас даже термин «языки формальных спецификаций» известен далеко не всем программистам, нужно констатировать, что в этой отрасли программирования получены значительные результаты. Они выражаются, во-первых, в том, что есть несколько ЯФС, которые уже нельзя назвать экспериментальными, более того, некоторые ЯФС подкреплены соответствующими стандартами. Во-вторых, более четким стало представление о способах использования ЯФС, о месте формальных методов в жизненном цикле разработки программного обеспечения и в процессах его разработки и использования.

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

 описать эскизную модель (функциональности, поведения);

 доказать, что модель корректна (не противоречива, консистентна);

 детализировать (уточнить) модель;

 доказать, что детализация проведена корректно;

 повторять два предыдущих шага до тех пор, пока не будет получена готовая программа.

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

У специализированных языков несколько другая история. Некоторые из них, например SDL(Specification and Design Language), родились из практики проектирования систем релейного управления, где проект традиционно был больше похож на чертеж, чем на текстовое (языковое) описание. Здесь эволюция заключалась во взаимном сближении графической и текстовой нотации на основе взаимных компромиссов и ограничений. При этом участниками компромисса была некоторая графическая нотация и языки программирования, опыт, накопленный в других языках формальных спецификаций, либо игнорировался, либо заимствовался с большим опозданием.

ЯФС традиционно рассматривались как средство проектирования. Новый взгляд на ЯФС появился, когда стала актуальной задача анализа уже существующего программного обеспечения. Существенное продвижение на этом фронте было связано с направлением Объектно-Ориентированного Анализа. Его идеи во многом созвучны с Объектно-Ориентированным Проектированием. Не удивительно, что оба эти направления предлагают близкие изобразительные средства для описания архитектуры и поведения систем. В последнее время наиболее известным средством такого рода является (преимущественно) графический язык UML (Unified Modelling Language). Заметим, чтоUML и подобные ему языки спецификации, безусловно, являются неплохими средствами проектирования, но обычно непригодны для доказательства правильности, на что делался акцент в классических языках спецификации.

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

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

Исполнимые спецификации, исполнимые модели. Этот подход предполагает разработку прототипов (моделей) систем для демонстрации возможности достижения поставленной цели и проведения экспериментов при частичной реализации функциональности. Примерами таких методологий и языков являются SDL, RSL (RAISE Specification Language).

Алгебраические спецификации предполагают описание свойств композиций операций. Композиции могут быть последовательными, параллельными, с временными ограничениями и без. Преимуществом этого подхода является то, что в идеале можно полностью абстрагироваться от структур данных, которые используются в качестве входных и выходных значений и, возможно, используются для сохранения внутреннего состояния моделей. Основной недостаток – это нетрадиционность приемов спецификации, что затрудняет их внедрение в промышленных разработках. В качестве примера языка алгебраических спецификаций можно назвать ASN1 (Abstract Syntax Notation One), стандарт которого входит в группу стандартов, описывающихSDL, RSL.

Сценарные спецификации описывают не непосредственно целевую систему, а способы ее использования или взаимодействия с ней. Оказывается, что такие косвенные описания, с одной стороны, позволяют судить о некоторых свойствах системы (тем самым, они, конечно, являются спецификациями), и, с другой стороны, такие спецификации могут служить хорошим руководством по использованию системы, что не всегда можно сказать о других видах спецификаций. Наибольшее распространение получили работы OMGгруппы и продукты компанииRational Corporation.

Ограничения состоят из пред- и постусловий функций, процедур и других операций и инвариантов данных. Имеются расширения этого подхода для объектно-ориентированных спецификаций. В этом случае к спецификациям операций добавляются спецификации методов классов, а к инвариантам – инварианты объектов и классов. Языком, поддерживающим спецификацию ограничений, является RSL.

2. Помехоустойчивое кодирование, теорема Шеннона, линейные коды, коды с малой плотностью проверок на чётность.

Корректирующий код (также помехоустойчивый код) — код, предназначенный для обнаружения и исправления ошибок.

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

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

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

Блоковые коды

Блоковый код, разбивающий информацию на фрагменты длиной {\displaystyle k} бит и преобразующий их в кодовые слова длиной {\displaystyle n} бит обычно обозначают {\displaystyle (n,\;k)}; при этом число {\displaystyle R={\frac {k}{n}}} называется скоростью кода. Если исходные {\displaystyle k} бит код оставляет неизменными, и добавляет {\displaystyle n-k} проверочных, такой код называется систематическим, иначе — несистематическим.

Задать блоковый код можно по-разному, в том числе таблицей, где каждой совокупности из {\displaystyle k} информационных бит сопоставляется {\displaystyle n} бит кодового слова. Однако хороший код должен удовлетворять как минимум следующим критериям:

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

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

Линейные коды общего вида

Линейный блоковый код — такой код, что множество его кодовых слов образует {\displaystyle k}-мерное линейное подпространство {\displaystyle C} в {\displaystyle n}-мерном линейном пространстве, изоморфное пространству {\displaystyle k}-битных векторов.

Это значит, что операция кодирования соответствует умножению исходного {\displaystyle k}-битного вектора на невырожденную матрицу {\displaystyle G}, называемую порождающей матрицей.

Для ортогонального по отношению к {\displaystyle C} подпространства {\displaystyle C^{\perp }} и матрицы {\displaystyle H}, задающей базис этого подпространства, и для любого вектора {\displaystyle {\overrightarrow {v}}\in C} справедливо:

{\displaystyle {\overrightarrow {v}}H^{T}={\overrightarrow {0}}}.

Минимальное расстояние и корректирующая способность

Расстоянием Хэмминга (метрикой Хэмминга) между двумя кодовыми словами {\displaystyle {\overrightarrow {u}}} и {\displaystyle {\overrightarrow {v}}} называется количество отличных бит на соответствующих позициях:

{\displaystyle d_{H}({\overrightarrow {u}},\;{\overrightarrow {v}})=\sum _{s}{|u^{(s)}-v^{(s)}|}}.

Минимальное расстояние Хэмминга {\displaystyle d_{\min }=\min _{u\neq v}d_{H}({\overrightarrow {u}},\;{\overrightarrow {v}})} является важной характеристикой линейного блокового кода. Она показывает, насколько «далеко» расположены коды друг от друга. Она определяет другую, не менее важную характеристику — корректирующую способность:

{\displaystyle t=\left\lfloor {\frac {d_{\min }-1}{2}}\right\rfloor }.

Корректирующая способность определяет, сколько ошибок передачи кода (типа {\displaystyle 1\leftrightarrow 0}) можно гарантированно исправить. То есть вокруг каждого кодового слова {\displaystyle A} имеем {\displaystyle t}окрестность {\displaystyle A_{t}}, которая состоит из всех возможных вариантов передачи кодового слова {\displaystyle A} с числом ошибок ({\displaystyle 1\leftrightarrow 0}) не более {\displaystyle t}. Никакие две окрестности двух любых кодовых слов не пересекаются друг с другом, так как расстояние между кодовыми словами (то есть центрами этих окрестностей) всегда больше двух их радиусов {\displaystyle d_{H}(A,\;B)\geqslant d_{\min }>2t}.

Таким образом, получив искажённую кодовую комбинацию из {\displaystyle A_{t}}, декодер принимает решение, что исходной была кодовая комбинация {\displaystyle A}, исправляя тем самым не более {\displaystyle t} ошибок.

Например, при наличии всего двух кодовых слов {\displaystyle A} и {\displaystyle B} с расстоянием Хэмминга между ними, равным 3, ошибка в одном бите слова {\displaystyle A} может быть исправлена, так как даже в этом случае принятое слово ближе к кодовому слову {\displaystyle A}, чем к {\displaystyle B}. Но если каналом были внесены ошибки в двух битах (в которых {\displaystyle A} отличалось от {\displaystyle B}), то результат ошибочной передачи {\displaystyle A} окажется ближе к {\displaystyle B}, чем {\displaystyle A}, и декодер примет решение, что передавалось слово {\displaystyle B}.

Коды Хэмминга

Коды Хэмминга — простейшие линейные коды с минимальным расстоянием 3, то есть способные исправить одну ошибку. Код Хэмминга может быть представлен в таком виде, что синдром:

{\displaystyle {\overrightarrow {s}}={\overrightarrow {r}}H^{T}},

где {\displaystyle {\overrightarrow {r}}} — принятый вектор, будет равен номеру позиции, в которой произошла ошибка. Это свойство позволяет сделать декодирование очень простым.

Общий метод декодирования линейных кодов

Любой код (в том числе нелинейный) можно декодировать с помощью обычной таблицы, где каждому значению принятого слова {\displaystyle {\overrightarrow {r}}_{i}} соответствует наиболее вероятное переданное слово {\displaystyle {\overrightarrow {u}}_{i}}. Однако данный метод требует применения огромных таблиц уже для кодовых слов сравнительно небольшой длины.

Для линейных кодов этот метод можно существенно упростить. При этом для каждого принятого вектора {\displaystyle {\overrightarrow {r}}_{i}} вычисляется синдром {\displaystyle {\overrightarrow {s}}_{i}={\overrightarrow {r}}_{i}H^{T}}. Поскольку {\displaystyle {\overrightarrow {r}}_{i}={\overrightarrow {v}}_{i}+{\overrightarrow {e}}_{i}}, где {\displaystyle {\overrightarrow {v}}_{i}} — кодовое слово, а {\displaystyle {\overrightarrow {e}}_{i}} — вектор ошибки, то {\displaystyle {\overrightarrow {s}}_{i}={\overrightarrow {e}}_{i}H^{T}}. Затем с помощью таблицы по синдрому определяется вектор ошибки, с помощью которого определяется переданное кодовое слово. При этом таблица получается гораздо меньше, чем при использовании предыдущего метода.

Линейные циклические коды

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

Циклическим кодом является линейный код, обладающий следующим свойством: если {\displaystyle {\overrightarrow {v}}} является кодовым словом, то его циклическая перестановка также является кодовым словом.

Слова циклического кода удобно представлять в виде многочленов. Например, кодовое слово {\displaystyle {\overrightarrow {v}}=(v_{0},\;v_{1},\;\ldots ,\;v_{n-1})} представляется в виде полинома {\displaystyle v(x)=v_{0}+v_{1}x+\ldots +v_{n-1}x^{n-1}}. При этом циклический сдвиг кодового слова эквивалентен умножению многочлена на {\displaystyle x} по модулю {\displaystyle x^{n}-1}.

Чаще всего используются двоичные циклические коды (то есть {\displaystyle v_{0},\;v_{1},\;\ldots } могут принимать значения 0 или 1).

Порождающий многочлен

Можно показать, что все кодовые слова конкретного циклического кода кратны определённому порождающему (генераторному) многочлену {\displaystyle g(x)}. Порождающий многочлен является делителем {\displaystyle x^{n}-1}.

С помощью порождающего многочлена осуществляется кодирование циклическим кодом. В частности:

• 
  несистематическое кодирование осуществляется путём умножения кодируемого вектора на {\displaystyle g(x)}: {\displaystyle v(x)=u(x)g(x)};
  
• 
  систематическое кодирование осуществляется путём «дописывания» к кодируемому слову остатка от деления {\displaystyle x^{n-k}u(x)} на {\displaystyle g(x)}, то есть {\displaystyle v(x)=x^{n-k}u(x)+[x^{n-k}u(x)\,{\bmod {\,}}g(x)]}.
  

Коды CRC

Коды CRC (англ. cyclic redundancy check — циклическая избыточная проверка) являются систематическими кодами, предназначенными не для исправления ошибок, а для их обнаружения. Они используют способ систематического кодирования, изложенный выше: «контрольная сумма» вычисляется путём деления {\displaystyle x^{n-k}u(x)} на {\displaystyle g(x)}. Ввиду того, что исправление ошибок не требуется, проверка правильности передачи может производиться точно так же.

Таким образом, вид многочлена {\displaystyle g(x)} задаёт конкретный код CRC. Примеры наиболее популярных полиномов:

Название кода	Степень	Полином
CRC-12	12	{\displaystyle x^{12}+x^{11}+x^{3}+x^{2}+x+1}
CRC-16	16	{\displaystyle x^{16}+x^{15}+x^{2}+1}
CRC-CCITT	16	{\displaystyle x^{16}+x^{12}+x^{5}+1}
CRC-32	32	{\displaystyle x^{32}+x^{26}+x^{23}+x^{22}+x^{16}+x^{12}+x^{11}+x^{10}+x^{8}+x^{7}+x^{5}+x^{4}+x^{2}+x+1}

Коды БЧХ

Коды Боуза — Чоудхури — Хоквингема (БЧХ) являются подклассом циклических кодов. Их отличительное свойство — возможность построения кода БЧХ с минимальным расстоянием не меньше заданного. Это важно, потому что, вообще говоря, определение минимального расстояния кода есть очень сложная задача.

Коды коррекции ошибок Рида — Соломона

Коды Рида — Соломона — недвоичные циклические коды, позволяющие исправлять ошибки в блоках данных. Элементами кодового вектора являются не биты, а группы битов (блоки). Очень распространены коды Рида-Соломона, работающие с байтами (октетами).

Математически коды Рида — Соломона являются кодами БЧХ.

Преимущества и недостатки блоковых кодов

Хотя блоковые коды, как правило, хорошо справляются с редкими, но большими пачками ошибок, их эффективность при частых, но небольших ошибках (например, в канале с АБГШ), менее высока.