Корректность и устойчивость программных систем

Отладка

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

Создание надежного кода

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

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

Формальное доказательство корректности кода. Метод Флойда и утверждения Assert

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

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

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

Метод Флойда оказал большое влияние на реальные языки программирования. Во многих языках программирования, включая C++, C#, Java, Python, появился оператор утверждения Assert, позволяющий разметить программный текст предикатами. Что происходит, когда вычисление достигает соответствующей точки и вызывается метод Assert? Если истинен предикат Assert, то вычисления продолжаются, не оказывая никакого влияния на нормальный ход вычислений. Если он ложен, то корректность вычислений нарушена, выполнение приостанавливается с появлением соответствующего уведомления.

Давайте посмотрим, как эта схема работает в Python . Синтаксис оператора следующий:

 assert <предикат>, <уведомление>

Если предикат истинен, то, как было сказано, вычисления продолжаются, - все соответствует спецификациям на данном отрезке. Если же предикат ложен, спецификации нарушены. Интерпретатор Python создает исключительную ситуацию - объект класса AssertionError с выдачей уведомления. Программа завершает работу, поскольку спецификации нарушены.

Построю пример, демонстрирующий работу метода Флойда. Затем обсудим достоинства и недостатки такого подхода. Я построил класс Translate, содержащий метод перевода целых чисел из одной системы счисления в другую систему счисления. Буду заниматься доказательством корректности этого метода по методу Флойда, разметив код метода соответствующими предикатами. Код метода будет состоять из двух фрагментов, каждый из которых в результате декомпозиции будет задан соответствующей функцией. Первая функция переводит строку, задающую целое число в системе p, в десятичную систему. Вторая функция - переводит полученное десятичное число в систему q.

Приведу первые строчки класса, который мы начинаем строить:

class Translate(object):  
    """ Перевод чисел из одной системы счисления в другую """
    digits = '0123456789ABCDEFGHIJKLMNOPQRST'

Атрибут класса digits будет использоваться многими методами класса.

Приведу заголовок функции, которая переводит целое число из одной системы счисления в другую:

def TranslateFromPtoQ(self, s, p, q):
    """
    Перевод числа, заданного строкой s из системы счисления p
    	в систему счисления q
    """

С чего следует начинать код в доказательном программировании? Правильно, с записи предикатов, накладывающих ограничение на входные данные - s, p, q. Предикаты для параметров p, q записываются достаточно просто. Неформальная формулировка предиката, накладывающего ограничения на входную строку, представляющую целое число, может быть задана следующим образом: "все символы входной строки s должны быть цифрами системы p".

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

Предусловие нашей функции можно записать с помощью трех предикатов:

 #предикаты предусловия
        assert 2 <= p <= 30, 'p вне границ '
        assert 2 <= q <= 30, 'q вне границ'
 assert self.IsDigitsOfP(s, p),  'символы s не являются цифрами системы p ' 

Метод IsDigitsOfP, задающий предикат, определяется следующим образом:

def IsDigitsOfP(self, s, p):
           """
           Предикат - предусловие
           Все символы строки s
           должны быть цифрами системы счисления p
           """
           for item in s:
               d = self.digits.find(item)
               if (d >= p) or (d == -1): return False
           return True

Предикат проверяет, что все символы являются цифрами, и что все цифры - это цифры системы p.

Первый фрагмент кода нашего метода переводит строку s в десятичное число. Следуя правилам качественного программирования, эта подзадача реализована как отдельная функция, так что в самом коде присутствует только вызов функции:

#Перевод в десятичную систему 
        x = self.TranslateFromPto10(s, p)

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

 # Предикат:
        #  постусловие функции TranslateFromPto10
        #  предусловие функции TranslateFrom10ToQ
        assert self.IsStringEqualNumber(s, p, x), 'Ошибка при переводе строки s в десятичную систему'

Для завершения кода нашей функции нам осталось задать вызов функции, после чего записать предикат постусловия:

 #Перевод числа в систему q
        res = self.TranslateFrom10ToQ(x, q) 
        assert self.IsStringEqualNumber(res, q, self.TranslateFromPto10(s, p)), 'Ошибка при переводе s из системы p в систему q'
 return res

Завершающий предикат утверждает, что исходная строка в системе p и результирующая строка в системе q имеют одно и тоже десятичное значение.

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

def IsStringEqualNumber(self, s, p, N):        
        """
        Предикат:
        Проверяет имеет ли строка s в системе p 
        десятичное значение, равное N
        """
 m = len(s)
        num = 0
        for i in range(m):
            d = self.digits.find(s[i])
            num += d * p ** (m - i- 1)
        return num == N

def TranslateFromPto10(self, s, p):
    """
        Перевод числа, заданного строкой s,
        в десятичную систему счисления
    """    
    res = 0
    for sd in s:
        d = self.digits.find(sd)
        res = res * p + d
    assert self.IsStringEqualNumber(s, p, res), 'Ошибка при переводе строки s в десятичную систему'
    return res

    def TranslateFrom10ToQ(self, x, q):
        """
        Перевод десятичного числа x
        в систему счисления q
        """
        res = ''; x1 = x
        while x1 != 0:
            d = x1 % q
            x1 = x1 // q
            res = self.digits[d] + res
        assert self.IsStringEqualNumber(res, q, x), 'Ошибка при переводе десятичного числа в систему q'
        return res

Осталось провести тестирование методов построенного класса. Доказательство доказательством, а тестирование привычнее.

Тесты, встроенные в класс

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

Добавим в конец нашего класса следующий код:

if __name__ == '__main__':
    obj = Translate()
    print(obj.TranslateFromPtoQ('101', 2, 3))
    print(obj.TranslateFromPtoQ('121', 3, 2))
    print(obj.TranslateFromPtoQ('121', 10, 20)) 
    print(obj.TranslateFromPtoQ('101', 2, 40))

У тестов есть охрана:

if __name__ == '__main__':

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

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

Продолжим проверку работоспособности методов assert. Попробуем в первом вызове перевести отрицательное число, что не предусмотрено спецификацией:

print(obj.TranslateFromPtoQ('-101', 2, 3))

При вызове теста будет получен следующий результат:

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

Достоинства и недостатки утверждений assert

Начнем с достоинств. Утверждения assert играют две важные роли:

Недостатки являются, как часто бывает, продолжением достоинств.

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

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