Software & Systems

Рассмотрим задачу верификации корректности выражения в языке программирования Хаскел с точки зрения правильности использования некоторой функции. Здесь под правильным использованием понимается применение функции лишь к аргументам, удовлетворяющим определенному предикату P-логики. Данная задача состоит в том, чтобы удостовериться, что в процессе вычисления выражения эта функция не будет применена к неправильным аргументам. Частным случаем здесь является полный запрет на вызов определенной функции. Например, для кода, полученного из ненадежного источника, может потребоваться гарантия того, что в нем не вызывается функция завершения программы. Предикат P-логики, соответствующий данному частному случаю, будет просто тождественно ложен.

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

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

Поясним это на примере следующих Хаскел-определений:

Пусть функция  может применяться только к положительному числу. Проверяя корректность выражения в правой части определения h в соответствии с описанным выше простым подходом, мы получим: .

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

Необходимо привести некоторые соображения, чтобы обосновать справедливость приведенных рассуждений. Многие, посмотрев на выражение , сразу же подумают, что вычисление этого выражения начинается с вычисления аргументов. При этом аргумент  должен быть вычислен независимо от того, положительно  или нет. Это на самом деле так для многих языков программирования, но в случае Хаскела мы имеем иную ситуацию. Хаскел, являясь чистым функциональным языком, не специфицирует порядок вычисления выражений. Более того, Хаскел обладает нестрогой семантикой [1], моделировать которую проще всего с помощью ленивых вычислений [2]. Именно такого подхода придерживается подавляющее большинство Хаскел-компиляторов. Ленивое вычисление применения функции к аргументам вызывает функцию с невычисленными аргументами, которые вычисляются только по мере необходимости. В приведенном примере второй аргумент  будет вычисляться, если первый будет положительным.

Однако стоит еще раз подчеркнуть, что Хаскел обладает нестрогой семантикой, а способ ее реализации спецификацией языка никак не навязывается. Помимо ленивого вычисления, было также предложено оптимистичное вычисление [3], которое может иногда вычислять подвыражения до того, как их значения фактически понадобятся. Тем не менее приведенные выше соображения корректны вне зависимости от механизма вычисления выражений. Дело в том, что Хаскел – безопасный язык. Система типов уже гарантирует, что программа не завершится с критической ошибкой. Таким образом, не важно, будет ли фактически вызвана функция с неправильными аргументами, главное – то, чтобы значение верифицируемого выражения не зависело от результата этого неправильного применения.

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

Это можно описать следующим образом: пусть  – шаблон утверждения функции f. Тогда подстановка будет иметь вид:

.

То есть высказывание  будет содержать переменные x и y, соответствующие параметрам функции f, а также переменные-высказывания и Cy, которые будут соответствовать утверждениям корректности выражений, стоящих на месте параметров  и y.

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

В приведенном примере с функциями  и  мы показали, опираясь только на здравый смысл, что аргументы, к которым в данном случае применяется f, всегда корректны. Определим теперь функцию  таким образом, чтобы иметь возможность проделывать эту процедуру автоматически и формально. Будем рассматривать  как функцию, определенную для различных видов Хаскел-выражений. При этом вычисление  для функции  будет заключаться в вычислении функции  для ее тела, которое, конечно же, является выражением. Запишем это в виде .

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

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

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

В правой части выражение  присутствует и само по себе, не как аргумент T. Его свободные переменные – свободные переменные получившегося шаблона. На их место будут подставлены аргументы, к которым применяется функция.

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

Для всех остальных выражений T(e) можно определить как

.

Здесь  – подвыражения e. Таким образом, для выражения, которое не является условным или применением функции, просто берется конъюнкция утверждений корректности его подвыражений.

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

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

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

Список литературы

1.   Peyton Jones S. и др. Report on the programming language Haskell 98, a non-strict, purely functional language, http://haskell.org, 1999.

2.   Augustsson L. Compiling lazy functional languages, part II, Chalmers University, 1987.

3.   Ennals R., Peyton Jones S. Optimistic evaluation: an adaptive evaluation strategy for non-strict programs, International Conference on Functional Programming, 2003.