Авторитетность издания
Добавить в закладки
Следующий номер на сайте
Ослабление утверждений корректности аргументов функции
Аннотация:
Abstract:
Авторы: Еловков Д.Д. () - , Сергеев С.Л. () - | |
Ключевые слова: ослабление утверждений, корректность, аргументы функции |
|
Keywords: , correctness, |
|
Количество просмотров: 8022 |
Версия для печати Выпуск в формате PDF (2.59Мб) |
Рассмотрим задачу верификации корректности выражения в языке программирования Хаскел с точки зрения правильности использования некоторой функции. Здесь под правильным использованием понимается применение функции лишь к аргументам, удовлетворяющим определенному предикату P-логики. Данная задача состоит в том, чтобы удостовериться, что в процессе вычисления выражения эта функция не будет применена к неправильным аргументам. Частным случаем здесь является полный запрет на вызов определенной функции. Например, для кода, полученного из ненадежного источника, может потребоваться гарантия того, что в нем не вызывается функция завершения программы. Предикат P-логики, соответствующий данному частному случаю, будет просто тождественно ложен. Рассмотрим такой простой пример, как насыщенное применение функции к аргументам где через Поясним это на примере следующих Хаскел-определений: Пусть функция Однако можно видеть, что значение функции f зависит от ее второго аргумента ( Необходимо привести некоторые соображения, чтобы обосновать справедливость приведенных рассуждений. Многие, посмотрев на выражение Однако стоит еще раз подчеркнуть, что Хаскел обладает нестрогой семантикой, а способ ее реализации спецификацией языка никак не навязывается. Помимо ленивого вычисления, было также предложено оптимистичное вычисление [3], которое может иногда вычислять подвыражения до того, как их значения фактически понадобятся. Тем не менее приведенные выше соображения корректны вне зависимости от механизма вычисления выражений. Дело в том, что Хаскел – безопасный язык. Система типов уже гарантирует, что программа не завершится с критической ошибкой. Таким образом, не важно, будет ли фактически вызвана функция с неправильными аргументами, главное – то, чтобы значение верифицируемого выражения не зависело от результата этого неправильного применения. Для того чтобы формулировать более слабые утверждения корректности аргументов функции, построим шаблон высказывания на основе определения данной функции. После этого в полученный шаблон подставляются выражения аргументов и их собственные утверждения корректности. Таким образом учитывается структура функции. Данный шаблон будет содержать в себе потенциал для получения более слабого утверждения. Это можно описать следующим образом: пусть
То есть высказывание Задача сводится к определению функции В приведенном примере с функциями Несколько упрощая задачу, а именно, не рассматривая рекурсию и функции высшего порядка, достаточно определить Самое существенное здесь – условные выражения, поскольку они являются прямым показателем зависимости результата от входных данных. Операционно это выражается в том, что исследуемое выражение вычисляется тогда, когда нужно вычислить значение всего условного выражения: Здесь для построения шаблона высказывания мы рекурсивно используем В правой части выражение Для выражения, представляющего собой применение функции к аргументам, нужно опять решить ту самую задачу, которая ставится в данной работе. Очевидно, Для всех остальных выражений T(e) можно определить как
Здесь И, наконец, выражению, представляющему собой просто переменную Такого тривиального определения функции При решении задачи определения корректности программы с точки зрения правильности использования определенных функций можно получать различные утверждения логики. Все они будут верными в том смысле, что их истинность соответствует корректности программы. Однако при тривиальном подходе получаемые утверждения в большинстве случаев слишком сильны. Следовательно, во-первых, их сложнее доказывать и, во-вторых, большее множество программ будет признано некорректными. Предложенная мето- дика позволяет получать более слабые утверждения корректности программ. Таким образом, корректность становится легче доказуемой, и мно- жество доказуемо корректных программ лучше аппроксимирует множество действительно корректных. Список литературы 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. |
Постоянный адрес статьи: http://swsys.ru/index.php?id=1595&page=article |
Версия для печати Выпуск в формате PDF (2.59Мб) |
Статья опубликована в выпуске журнала № 3 за 2008 год. | |
Статья находится в категориях: Haskell | |
Статья относится к отраслям: Вычисления |
Возможно, Вас заинтересуют следующие статьи схожих тематик: