2.1.2. Способы контроля типов

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

Введем понятия, которые нам понадобятся для классификации способов контроля типов.

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

Программа называется типово-правильной, если она удовлетворяет правилам типизации языка, к которым относятся приписывание типов переменным и константам, определение типов выражений по типам их частей, согласование типов частей языковых конструкций (например, операторов присваивания) и т.п.

Например, правила типизации большинства языков программирования требуют, чтобы при описании массива были указаны типы его компонент и индексов. Определение типовой правильности программ также производится на этапе компиляции. Обозначим множество программ этого класса через Lt. Конечно, Lt -- подмножество Ls. Правила типизации для некоторого языка могут быть не определены. Такой язык называется нетипизированным (для него не определено множество Lt ); в противном случае язык типизированный. Типизированные языки имеют несомненные преимущества перед нетипизированными с точки зрения уменьшения ошибок при программировании. Все современные универсальные языки программирования типизированные, поэтому далее мы будем рассматривать только такие языки.

Программа называется программой без типовой ошибки, если при ее выполнении не возникает типовой ошибки несоответствия типа текущего значения переменной (константы, параметра и т.д.) типу, требуемому операцией, процедурой или другой языковой конструкцией, в которой находится эта переменная (константа, параметр и т.д.). Например, если текущее значение переменной I в операции А(I) выходит за границы изменения индекса массива А, то это типовая ошибка, если границы входят в понятие типа массива (как в Паскале), и не типовая ошибка в противном случае (как в ПЛ/1). Обозначим множество программ этого класса через Le. Ясно, что Le входит в Lt.

Программа называется программой с выловленными типовыми ошибками, если все возникающие при ее выполнении типовые ошибки обнаруживаются при контроле типов. Обозначим множество программ этого класса через Ld : Ld <= lt \ Le

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

Если Lt =Le, т.е. типово-правильные программы не могут содержать типовых ошибок, то язык называется языком с полным статическим контролем типов.

Если Ls =Lt, т.е. правила типизации языка очень слабые или их нет совсем (все синтаксически правильные программы являются типово-правильными), и, следовательно, вся работа по контролю типов производится во время выполнения программ, то язык называется языком с динамическим контролем типов, под которым подразумевается проверка типов объектов данных в процессе выполнения языковых конструкций и выдача сообщений о возможных типовых ошибках. Если при этом Ld =Lt \ Le, т.е. все типовые ошибки обнаруживаются при динамическом контроле типов, то язык называется языком с полным динамическим контролем типов.

Если Le < Lt < Ls, т.е. не все синтаксически правильные программы являются типово-правильными и типовоправильные программы могут содержать типовые ошибки, то язык называется языком со смешанным контролем типов. Если при этом Ld= Lt\ Le, то язык называется языком с полным смешанным контролем типов.

Все практические языки программирования -- это языки со смешанным контролем типов, т.е. контроль выполняется на этапе и компиляции, и выполнения. Конечно, для повышения эффективности выполнения программ было бы желательно количество проверок типа во время выполнения программы (т.е. мощность множества Lt \ Le ) уменьшить до нуля.

Однако пока это удается сделать лишь за счет существенной потери мощности языка, поэтому реальной целью является минимизация множества Lt \ Le при сохранении мощности и выполнении условия Ld=Lt \ Le.