определения

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

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

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

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

* * *

n-местное отношение (relation) на наборе множеств S1, S2, …, Sn - это множество R ⊆ S1 × S2 × … × Sn кортежей элементов S1, …, Sn. Если (s1, …, sn) ∈ R, где s1 ∈ S1, …, sn ∈ Sn, то говорится, что s1 , …, sn связаны (related) отношением R

одноместное отношение на множестве S называется предикатом (predicate) на S. говорится, что P истинен на s ∈ S, если s ∈ P. мы часто будем писать P(s) вместо s ∈ P, рассматривая P как функцию, переводящую элементы S в булевские значения

двуместное отношение R на множествах S и T называется бинарным отношением (binary relation). мы часто будем писать s R t вместо (s, t) ∈ R. если S и T совпадают (назовем это множество U), то мы будем говорить, что R - бинарное отношение на U

областью определения (domain) отношения R на множествах S и T называется множество элементов s ∈ S, таких, что (s, t) ∈ R для некоторого t. область определения R обозначается dom(R). областью значений (codomain) R называется множество элементов t ∈ T, таких, что (s, t) ∈ R для некоторого s. область значений R обозначается range(R)

отношение R на множествах S и T называется частичной функцией (partial function) из S в T, если из (s, t1) ∈ R и (s, t2) ∈ R следует, что t1 = t2. если, кроме того, dom(R) = S, то R называется всюду определенной функцией (total function)

пусть R - бинарное отношение на множестве S, а P - предикат на S. Если из s R s′ и P(s) следует P(s′), то говорится, что R сохраняет (preserves) P

бинарное отношение R на множестве S рефлексивно, если каждый элемент S связан отношением R с самим собой - т. е. для всех s ∈ S, s R s (или (s, s) ∈ R)

отношение R симметрично, если для всех s, t ∈ S из s R t следует t R s

отношение R транзитивно, если из s R t и t R u следует s R u

отношение R антисимметрично, если из s R t и t R s следует s = t

рефлексивное и транзитивное отношение R на множестве S называется предпорядком (preorder) на S. если предпорядок (на S) к тому же антисимметричен, то он называется частичным порядком (partial order) на S. частичный порядок ⩽ называется линейным порядком (total order) на S, если для любых s, t ∈ S выполняется либо s ⩽ t, либо t ⩽ s

пусть ⩽ есть частичный порядок на S, а s и t - элементы S. элемент j ∈ S называется объединением (join) (или точной верхней границей, least upper bound) s и t, если:
1. s ⩽ j и t ⩽ j, а также
2. для всякого k ∈ S, если s ⩽ k и t ⩽ k, то j ⩽ k

аналогично, элемент m ∈S называется пересечением (meet) (или точной нижней границей, greatest lower bound) s и t, если:
1. m ⩽ s и m ⩽ t, а также
2. для всякого n ∈ S, если n ⩽ s и n ⩽ t, то n ⩽ m

рефлексивное, транзитивное и симметричное отношение на множестве S называется отношением эквивалентности (equivalence relation) на S

пусть у нас есть предпорядок ⩽ на множестве S. убывающая цепочка (decreasing chain) на ⩽ есть последовательность s1, s2, s3, … элементов S, такая, что каждый элемент последовательности строго меньше предшествующего: si+1 < si для всякого i

пусть у нас есть множество S с предпорядком ⩽. предпорядок ⩽ называется полным (well founded), если он не содержит бесконечных убывающих цепочек. например, обычный порядок на натуральных числах, 0 < 1 < 2 < 3 < …, является полным, а тот же самый порядок на целых числах, … < −3 < −2 < −1 < 0 < 1 < 2 < 3 < … - нет. иногда мы не упоминаем ⩽ явно и просто называем S вполне упорядоченным множеством (well-founded set)

* * *

1. операционная семантика (operational semantics) специфицирует поведение языка программирования, определяя для него простую абстрактную машину (abstract machine). машина эта «абстрактна» в том смысле, что в качестве машинного кода она использует термы языка, а не набор команд какого-то низкоуровневого микропроцессора. для простых языков состояние (state) машины - это просто терм, а поведение ее определяется функцией перехода (transition function), которая для каждого состояния либо указывает следующее состояние, произведя шаг упрощения старого терма, либо объявляет машину остановившейся. смыслом (meaning) терма t объявляется конечное состояние, которого машина достигает, будучи запущена с начальным состоянием t. строго говоря, то, что мы здесь описываем, - это так называемая операционная семантика с малым шагом (small-step operational semantics), известная также как структурная операционная семантика (structural operational semantics)

2. денотационная семантика (denotational semantics) рассматривает смысл с более абстрактной точки зрения: смыслом терма считается не последовательность машинных состояний, а некоторый математический объект, например число или функция. построение денотационной семантики для языка состоит в нахождении некоторого набора семантических доменов (semantic domains), а также определении функции интерпретации (interpretation function), которая ставит элементы этих доменов в соответствие термам. поиск подходящих семантических доменов для моделирования различных языковых конструкций привел к возникновению сложной и изящной области исследований, известной как теория доменов (domain theory)

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