Як заборонити некоректні стани в програмі на етапі компіляції

💡 Усі статті, обговорення, новини про Python — в одному місці. Приєднуйтесь до Python спільноти!

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

Чимала кількість отриманих коментарів була про те, що «в мейнстрім-мовах це непотрібно, і там роблять не так».

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

Задача

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

Ми моделюємо це як модуль/бібліотеку/клас/... (в залежності від вибору вашої мови програмування), яку називаємо Moonbase, в API якої входять наступні функції:

• begin_day — починає новий день (з астронавтом всередині бази, без скафандра, із закритим шлюзом. Це може бути конструктор класу або схожий механізм ініціалізації).
• open_lock
• close_lock
• spacesuit_on
• spacesuit_off
• leave_base
• enter_base
• moan
• take_sample
• empty_pocket
• end_day — закінчує день на базі. Це може бути деструктор класу або схожий механізм завершення.

Для простоти домовимось, що ці функції виводять повідомлення в stdout і нічого більше. З точки зору поведінки, така реалізація на Python буде вичерпною і достатньою:

 class Moonbase:
  def __init__(self):
    print ("DAY BEGINS")
  def open_lock(self):
    print ("OPENING LOCK")
  def close_lock(self):
    print ("CLOSING LOCK")
  def spacesuit_on(self):
    print ("SPACESUIT ON")
  def spacesuit_off(self):
    print ("SPACESUIT OFF")
  def leave_base(self):
    print ("LEAVING BASE")
  def enter_base(self):
    print ("ENTERING BASE")
  def moan(self):
    print (". o O (Ugh! Damn moon! I am too old for this!)")  
  def take_sample(self):
    print ("MINING REGOLITH")
  def empty_pocket(self):
    print ("EMPTYING POCKET")
  def end_day(self):
    print ("DAY ENDS")

Якщо ви хочете, щоб ці функції приймали додаткові аргументи або повертали значення, ви можете це зробити. Загалом робіть те, що є ідіоматичним/природним у вашій мові.

Додаткові правила

Додатково є набір правил, виконання яких ми хочемо забезпечити на етапі компіляції. Вони визначають, коли конкретну функцію можна або не можна викликати.

1. Скафандр можна одягнути тільки якщо він не одягнутий.
2. Скафандр можна зняти тільки якщо він одягнутий.
3. Шлюз можна відкрити тільки якщо він закритий.
4. Шлюз можна закрити тільки якщо він відкритий.
5. Щоб відкрити шлюз, скафандр має бути одягнутий.
6. Кишені скафандра мають бути порожніми, щоб його можна було одягнути (інакше крихти реголіту можуть пошкодити скафандр).
7. Скафандр не можна знімати ззовні.
8. Скафандр не можна знімати, якщо шлюз відкритий.
9. Скафандр не можна знімати, якщо його кишені повні (інакше крихти реголіту можуть пошкодити скафандр).
10. Базу можна залишити тільки якщо астронавт всередині, у скафандрі, і шлюз відкритий.
11. Якщо ви вийшли назовні, ви обов’язково повинні взяти зразок реголіту. Тобто ви можете увійти на базу тільки з повною кишенею скафандра і відкритим шлюзом.
12. Астронавт не повинен нарікати на життя на Місяці у скафандрі — це буде записано і погано вплине на його кар’єру.
13. Збір зразків реголіту можна здійснювати тільки ззовні. Це створює багато пилу, тому це потрібно робити тільки з закритим шлюзом. Кишеня скафандра має бути порожньою.
14. Кишеню скафандра можна очистити будь-коли. Якщо це зроблено ззовні, це означає, що астронавт більше не має зразка і, можливо, йому доведеться отримати новий для повернення на базу.
15. Наприкінці дня астронавт повинен бути всередині бази, без скафандра, із закритим шлюзом.

Ми можемо додати стан до наївної реалізації Python вище і використовувати його для забезпечення цих правил (але лише на етапі виконання, тож це лише ілюстрація, а не бажане рішення):

class Moonbase:
  lockOpen = False
  suitOn  = False
  isOutside = False
  pocketsFull = False
  
  def __init__(self):
    print ("DAY BEGINS")
  def open_lock(self):
    assert(not self.lockOpen)
    assert(self.suitOn)
    print ("OPENING LOCK")
    self.lockOpen=True
  def close_lock(self):
    assert(self.lockOpen)
    print ("CLOSING LOCK")
    self.lockOpen=False
  def spacesuit_on(self):
    assert(not self.suitOn)
    assert(not self.pocketsFull)
    print ("SPACESUIT ON")
    self.suitOn=True
  def spacesuit_off(self):
    assert(self.suitOn)
    assert(not self.isOutside)
    assert(not self.lockOpen)
    assert(not self.pocketsFull)
    print ("SPACESUIT OFF")
    self.suitOn=False
  def leave_base(self):
    assert(self.lockOpen)
    assert(self.suitOn)
    assert(not self.isOutside)
    print ("LEAVING BASE")
    self.isOutside=True
  def enter_base(self):
    assert(self.isOutside)
    assert(self.pocketsFull)
    assert(self.lockOpen)
    print ("ENTERING BASE")
    self.isOutside=False
  def moan(self):
    assert(not self.suitOn)
    print (". o O (Ugh! Damn moon! I am too old for this!)")  
  def take_sample(self):
    assert(self.isOutside)
    assert(not self.lockOpen)
    assert(not self.pocketsFull)
    print ("TAKING REGOLITH SAMPLE")
    self.pocketsFull=True
  def empty_pockets(self):
    assert(self.pocketsFull)
    print ("EMPTYING POCKETS")
    self.pocketsFull=False
  def end_day(self):
    assert(not self.isOutside)
    assert(not self.lockOpen)
    assert(not self.suitOn)
    assert(not self.pocketsFull)
    print ("DAY ENDS")

Відкрите питання

Чи можемо ми забезпечити виконання всіх цих правил на етапі компіляції — так, щоб код, який порушує їх, взагалі не можна було б скомпілювати та запустити? Наприклад, щоб отака програма (псевдокод) не компілювалась:

  begin_day ()
  spacesuit_on
  open_lock
  leave_base
  close_lock
  /* Cannot take spacesuit off, will suffocate, so we should get compile error on the next line */
  spacesuit_off
  end_day

Я зробив маленький проєкт на GitHub, який містить реалізації на Haskell, та на OCaml (інтерфейс бібліотеки, та його імплементація). В них обох коректність переходів контролюється за рахунок кодування поточного стану системи лише в сигнатурах функцій. Що лишає реалізацію API дуже простою, майже як в моєму першому прикладі на Python (який не перевіряє ніяких правил взагалі). Для Haskell код модуля Moonbase займає 53 (непустих) рядки, для OCaml — 24. Ось, наприклад, імплементація Moonbase на OCaml:

type ('lock, 'suit, 'location, 'pockets) state = State
let begin_day () = print_endline "DAY BEGINS"; State
let open_lock _ = print_endline "OPENING LOCK"; State
let close_lock _ = print_endline "CLOSING LOCK"; State
let spacesuit_on _ = print_endline "SPACESUIT ON"; State
let spacesuit_off _ = print_endline "SPACESUIT OFF"; State
let leave_base _ = print_endline "LEAVING BASE"; State
let enter_base _ = print_endline "ENTERING BASE"; State
let moan _ = print_endline ". o O (Ugh! Damn moon! I am too old for this!)"; State  
let take_sample _ = print_endline "TAKING REGOLITH SAMPLE"; State
let empty_pockets _ = print_endline "EMPTYING POCKETS"; State
let end_day _ = print_endline "DAY ENDS"

І ось сігнатури, які, власне, і забезпечують дотримання правил:

type ('lock, 'suit, 'location, 'pockets) state
 
val begin_day     : unit -> ([`lock_closed], [`spacesuit_off], [`inside], [`empty]) state

val open_lock     : ([`lock_closed], [`spacesuit_on], 'location, 'pockets) state 
                  -> ([`lock_open], [`spacesuit_on], 'location, 'pockets) state

val close_lock    : ([`lock_open], [`spacesuit_on], 'location, 'pockets) state 
                  -> ([`lock_closed], [`spacesuit_on], 'location, 'pockets) state

val spacesuit_on  : ([`lock_closed], [`spacesuit_off], [`inside], [`empty]) state 
                  -> ([`lock_closed], [`spacesuit_on], [`inside], [`empty]) state

val spacesuit_off : ([`lock_closed], [`spacesuit_on], [`inside], [`empty]) state
                  -> ([`lock_closed], [`spacesuit_off], [`inside], [`empty]) state

val leave_base    : ([`lock_open], [`spacesuit_on], [`inside], 'pockets) state
                  -> ([`lock_open], [`spacesuit_on], [`outside], 'pockets) state 

val enter_base    : ([`lock_open], [`spacesuit_on], [`outside], [`full]) state
                  -> ([`lock_open], [`spacesuit_on], [`inside], [`full]) state

val moan          : ('lock, [`spacesuit_off], 'location, 'pockets) state
                  -> ('lock, [`spacesuit_off], 'location, 'pockets) state

val take_sample   : ([`lock_closed], [`spacesuit_on], [`outside], [`empty]) state 
                  -> ([`lock_closed], [`spacesuit_on], [`outside], [`full]) state

val empty_pockets : ('lock, 'suit, 'location, [`full]) state 
                  -> ('lock, 'suit, 'location, [`empty]) state

val end_day       : ([`lock_closed], [`spacesuit_off], [`inside], [`empty]) state -> unit

Я додав до проєкту простий Makefile, який дозволяє скомпілювати код за допомогою dockerized compiler, щоб ви могли за бажанням спробувати мій код, не встановлюючи собі весь toolchain Haskell або OCaml.

Як це роблять у мейнстрімі

Я сподіваюсь, що ви мені покажете :)

Якщо цей іграшковий приклад вас зацікавив, я був би радий побачити реалізації на інших мовах програмування — форкайте мій проєкт, додавайте свою мову, відкривайте PR.