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

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

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

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

class Alarm_Clock {
public:
void h_button() // Нажатие кнопки H
 {
    if (is_in_alarm_time_mode) {
        alarm_hours = (alarm_hours + 1) % 24;
    } else {
        hours = (hours + 1) % 24;
    }
 }

void m_button() // Нажатие кнопки M
 {
    if (is_in_alarm_time_mode) {
        alarm_minutes = (alarm_minutes + 1) % 60;
    } else {
        minutes = (minutes + 1) % 60;
    }
 }

void a_button() // Нажатие кнопки A
 {
    if (is_alarm_on) {
        if (is_in_alarm_time_mode) {
            is_in_alarm_time_mode = false;
        } else {
            bell_off();
            is_alarm_on = false;
        }
    } else {
        is_alarm_on = true;
        is_in_alarm_time_mode = true;
    }
 }

void tick() // Срабатывание минутного таймера
 {
    if (is_alarm_on && !is_in_alarm_time_mode) {
        if ((minutes == alarm_minutes - 1) && (hours == alarm_hours) ||
            (alarm_minutes == 0) && (minutes == 59) && (hours == alarm_hours - 1))
            bell_on();
        else if ((minutes == alarm_minutes) && (hours == alarm_hours))
            bell_off();
    }
    minutes = (minutes + 1) % 60;
    if (minutes == 0) hours = (hours + 1) % 24;
 }

private:
int hours; // Часы текущего времени
int minutes; // Минуты текущего времени
int alarm_hours; // Часы срабатывания будильника
int alarm_minutes; // Минуты срабатывания будильника
bool is_alarm_on; // Включен ли будильник?
bool is_in_alarm_time_mode;
 // Активен ли режим установки времени будильника?
void bell_on() {...} // Включить звонок
void bell_off() {...} // Выключить звонок
};

Приведение к автоматному коду для улучшения понятности выглядел даже более впечатляюще.

bool x1() {
    if ((minutes == alarm_minutes - 1) && (hours == alarm_hours) ||
        (alarm_minutes == 0) && (minutes == 59) && (hours == alarm_hours - 1))
        return true;
    else
        return false;
}

bool x2() {
    if ((minutes == alarm_minutes) && (hours == alarm_hours))
        return true;
    else
        return false;
}

void z1() {
    hours = (hours + 1) % 24;
}

void z2() {
    minutes = (minutes + 1) % 60;
}

void z3() {
    alarm_hours = (alarm_hours + 1) % 24;
}

void z4() {
    alarm_minutes = (alarm_minutes + 1) % 60;
}

void z5() {
    minutes = (minutes + 1) % 60;
    if (minutes == 0) hours = (hours + 1) % 24;
}

void z6() {
 ... // Включить звонок
}

void z7() {
 ... // Выключить звонок
}

// Реализация управляющего автомата
void A1() {
    switch (y) {
    case 1: // Будильник выключен
        if (e == h) { z1(); }
        else if (e == m) { z2(); }
        else if (e == a) { y = 2; }
        else if (e == t) { z5(); }
        break;
    case 2: // Установка времени будильника
        if (e == h) { z3(); }
        else if (e == m) { z4(); }
        else if (e == a) { y = 3; }
        else if (e == t) { z5(); }
        break;
    case 3: // Будильник включен
        if (e == h) { z1(); }
        else if (e == m) { z2(); }
        else if (e == a) { z7(); y = 1; }
        else if ((e == t) && x1()) { z5(); z6(); }
        else if ((e == t) && x2()) { z5(); z7(); }
        else if (e == t) { z5(); }
        break;
    }
}

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

MODULE AlarmClock;

 CONST
  AlarmOff  = 0;  AlarmSet  = 1;  AlarmWait = 2;

 VAR
  time: ARRAY 2 OF RECORD hours, minutes: INTEGER END;
  state: INTEGER;

 PROCEDURE Bell(on: BOOLEAN); END Bell;

 PROCEDURE Next(VAR var: INTEGER; mod: INTEGER); BEGIN
  var := (var + 1) MOD mod
 END Next;

 PROCEDURE PushHour*; BEGIN
  Next(time[ORD(state = AlarmSet)].hours, 24)
 END PushHour;

 PROCEDURE PushMinute*; BEGIN
  Next(time[ORD(state = AlarmSet)].minutes, 60)
 END PushMinute;

 PROCEDURE PushAlarm*; BEGIN
  Bell(FALSE);
  Next(state, 3) (* Off, Set, Wait *)
 END PushAlarm;

 PROCEDURE MinuteTick*; BEGIN
  Next(time[0].minutes, 60);
  IF time[0].minutes = 0 THEN Next(time[0].hours, 24) END;

  Bell((state # AlarmOff)
     & (time[1].hours   = time[0].hours)
     & (time[1].minutes = time[0].minutes))
 END MinuteTick;

END AlarmClock.

Вот и всё — этот код оказался слишком простым, чтобы как-то дополнительно его разбивать по режимам работы будильника. Похоже, авторы неосознанно подогнали начальный пример, названный ими громоздким и непонятным, под решение с автоматом. Хотя даже в таком виде выгода предложенного взгляда на разработку не выглядит очевидной.

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