Проектируем по спецификации

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

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

Зададим задачу. Необходимо спроектировать и реализовать механизм сохранения и чтения токенов авторизации. Требования: ограниченный доступ на запись в хранилище. Нельзя просто взять и предоставлять классам хранилище или интерфейс по работе с хранилищем, через который можно перезаписывать локальный storage. Так же токены должны храниться в криптостойком хранилище. В любом случае это будет “обертка” над Android SDK Shared Preferences. Префы представляют собой key-value хранилище.

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

AuthStorage

AuthStorage - это интерфейс, который определяет основные действия для работы с токенами авторизации:

• readToken: Возвращает токен авторизации.

Спецификация

Предусловие:

• Хранилище инициализировано, алгоритмы шифрования указан

Постусловие:

• Возвращается валидный токен безопасности, если таковой имеется.
• Если токен отсутствует, возвращается AuthToken типа Empty. Так как пример на Kotlin, сделаем через sealed классы:

sealed class AuthToken {
  data class Value(val token: String) : AuthToken() {
    init {
      require(token.isNotBlank())
    }
  }

  data object Empty : AuthToken()
}

ReadOnlyAuthStorage

ReadOnlyAuthStorage - реализация AuthStorage, которая позволяет только читать токен без возможности его изменения.

Методы

• readToken
• isTokenExist
• keyFor (генерирует уникальный ключ, по которому будет храниться токен. Используется тип токена)

ReadWriteAuthStorage

ReadWriteAuthStorage расширяет ReadOnlyAuthStorage добавлением функций записи.

Методы

• readAuthToken (наследуется от AuthStorage)
• storeAuthToken: Сохраняет токен авторизации.

Спецификация для storeAuthToken

Предусловие:

• Предоставленный для сохранения токен действителен (не null, не пустой и не истекший).

Постусловие:

• Токен сохранен в хранилище.
• При попытке получения токена методом readAuthToken возвращается последний сохраненный токен.

Пример правильной спецификации для storeAuthToken

Данная спецификация используется для метода storeAuthToken в ReadWriteAuthStorage.

Предусловие: Токен не должен быть null, пустой строкой или истекшим. Это гарантирует, что в хранилище не будут сохраняться невалидные токены.

Постусловие: Токен успешно сохранен в хранилище, и последующие вызовы readAuthToken возвращают этот же токен, демонстрируя успешное сохранение.

Связь с методами формальной верификации:

И хотя такие комментарии сами по себе не являются методами формальной верификации, они играют ключевую роль в процессе верификации, поскольку:

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

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

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

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

В качестве заключения

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

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

Вдогонку предоставлю интересный ролик про ООП, наставляет на “правильное” ООП-мышление и наставляет на отказ от прежнего процедурного подхода.

P.S. В Kotlin есть удобный пакет Preconditions, которые могут использовать для задания правил пред- и постусловий. Пример:

fun checkLightValue(light: Int) {
  require(light in 0..10) { "Значение [Light] должно находиться с диапазоне от 0 до 10 включительно." }
}