Чи можете ви точно описати, що таке «правильний стан» вашої системи? Якщо так, то маємо індуктивний інваріант. Це означає, що ваша система з меншою ймовірністю зробить погані речі, і ви ближче до того, щоб довести це. Ми написали інструкцію про те, як туди ⬇️ дістатися

Визначити «правильний стан» напрочуд важко. Найновіша функція Quint робить його доступним завдяки інтерактивному зворотному зв'язку, який навчить вас тому, що ви пропустили.

У сьогоднішньому блозі ми показуємо покроковий процес із надійною трансляцією, починаючи з загального та дозволяючи Quint вдосконалювати наше мислення, поки ми не зробимо все правильно. Дізнайтеся, як: