Застосовано метод доведення властивостей паралельних програм, що виконуються багатоекземплярно в режимі почергового покрокового переключення і взаємодіють через спільну пам'ять, для доведення властивості коректності банківської системи виплати грошових переказів. В роботі поставлено задачу, побудовано транзиційну систему для моделі зі спрощеним станом, сформульовано інваріант програми та проведено доведення істинності інваріанту над програмною системою у довільний момент часу. Зроблено висновки щодо зручності та адекватності застосування методу для доведення коректності паралельних систем. Ключові слова: коректність програмного забезпечення, доведення часткової коректності, паралельна програма, interleaving, інваріант, IPCL, композиційно-номінативні мови, формальна верифікація Применен метод доказательства свойств параллельных программ, которые выполняются многоэкземплярно в режиме поочередного пошагового переключения и взаимодействуют через общую память, для доказательства свойства корректности банковской системы выплаты денежных переводов. В работе поставлена задача, построена транзиционная система для модели с упрощенным состоянием, сформулирован инвариант программы и проведено доказательство истинности инварианта над программной системой в любой момент времени. Сделаны выводы о удобстве и адекватности применения метода для доказательства корректности параллельных систем. Ключевые слова: корректность программного обеспечения, доказательство частичной корректности, параллельная программа, interleaving, инвариант, IPCL, композиционно-номинативные языки, формальная верификация The method for properties proof for parallel programs running multiple-instance interleaving with shared memory was applied in order to prove the correctness property of the banking system for remittances payments. The task was stated, transitional system was built for the model with simplified state, and the program invariant was formulated and proved to keep true over the software system at any given time in this work. Conclusions about the convenience and adequacy of method application to prove the correctness of parallel systems were made.
Проектування
Тепер розглянемо детальніше процедуру авторизації. Легко побудувати більш-менш очевидну покрокову процедуру авторизації переказу в першому наближенні: 1) зафіксувати чергову спробу авторизації 2) якщо переказ не заблоковано то якщо переказ не виплачено то якщо надана коректна інформація по переказу то (*) якщо ця інформація співпадає з даними у базі то (*) авторизувати виплату переказу інакше (в усіх інших випадках) відмовити в авторизації 3) якщо спроб авторизації накопичилось більше 2, то заблокувати переказ.
Опустимо з аналізу перевірку коректності інформації (помічено *), оскільки реально це не впливає суттєво на результат авторизації (більш того, ці перевірки складають банківську таємницю) – так, це дуже важлива перевірка, але, як побачимо далі, вона не є критичною для доведення властивості, яка нас цікавить (іншими словами, цілком зрозуміло, як її робити). (Очевидно, що коли хоча б одна з умов не виконується, авторизація не пройде, оскільки вона відбувається лише у випадку, коли всі умови повертають True під час перевірки – принаймні логічно так має бути.) Як було відзначено, середовище SQL є середовищем з паралелізмом із взаємодією через спільну пам’ять. В зв’язку з цим слід також зауважити, що якщо деяка умова повернула True під час обчислення її значення, то пізніше (при виконанні наступних кроків) вона (той самий предикат умовного оператору) може потенційно прийняти значення False, отже коли виконання дійде до блоку “then” з “if-then-else”, наприклад, то значення предиката умови може вже бути False (хоча до виконання блоку “then” можна було приступити лише в ситуації, коли при обчислення предикату умови було отримано результат True). А отже, ми можемо отримати суперечливу ситуацію і зокрема, наприклад, авторизувати виплату одного переказу двічі.
Не зосереджуючись докладно на архітектурних рішеннях та дизайні системи, відзначимо ключові думки та їх обґрунтування.
1. Вузьке місце. Інтуїтивно зрозуміло, що критичним місцем системи є паралельна спроба авторизації одного й того ж переказу кілька разів (наприклад, коли дехто перехопив коректну інформацію про переказ і намагається отримати авторизацію не будучи дійсним одержувачем переказу). Цей факт не впливає на подальшу побудову системи та доведення необхідної властивості, але дозволяє краще розуміти вузькі місця і приймати правильні рішення щодо дизайну та архітектури системи.
2. Рівень ізоляції транзакцій SQL (Transaction Isolation Level). Кожна авторизація складає транзакцію
(насправді – дві транзакції: фіксація намірів авторизації та результат авторизації – власне авторизація).
Рівень ізоляції обирається Read Committed. Зрозуміло, що нам необхідний рівень, який гарантував би
неможливість одночасної роботи з одним переказом (фактично, не допускав би інтерференцію процесів), але,
поперше, найсуворіший рівень ізоляції – Serializable – не еквівалентний послідовному виконанню процесів
(тоді була б гарантована свобода від інтерференції), а по-друге, рівень ізоляції Serializable рекомендований до
застосування лише у випадках зі складною логікою обчислень (в даній системі логіка не є надто складною) і
має великий відсоток відкатів транзакцій (transaction roll-back), що призводить до необхідності повторних
спроб виконання транзакцій, ускладнення внутрішньої логіки виконання команд SQL-сервером (більше
блокувань будуть утримуватись довший час) та зменшення загальної швидкодії системи (детальніше про це
можна прочитати в документації по будь-якому SQL-серверу – Microsoft SQL Server, PostgreSQL, а також в [
3. Уточнення алгоритму авторизації. Введемо перевірку на кількість паралельних (виконуваних одночасно) авторизацій. Це можливо, оскільки ми фіксуємо спробу авторизації в журналі, незалежно від її результату, який з’ясується пізніше.
Таким чином, уточнений алгоритм авторизації виглядатиме наступним чином: 1) записати чергову спробу авторизації 2) якщо кількість одночасних (паралельних) спроб = 1, то якщо переказ не заблоковано то якщо переказ не виплачено то якщо надана коректна інформація по переказу і ця інформація співпадає з даними у базі то (*) авторизувати виплату переказу інакше (в усіх інших випадках) відмовити в авторизації 3) якщо спроб авторизації накопичилось більше 2, то заблокувати переказ. Паралельно з цим спеціальний оператор по вирішенню конфліктів може розблокувати спірні перекази, тобто паралельно виконується процес:
розблокувати переказ Побудова програми IPCL та моделюючої транзиційної системи
Нам знадобиться модель системи (модель реальної системи на мові SQL в мові IPCL). Отже, одним з
ключових моментів є визначення адекватного рівня деталізації системи (і, відповідно, доведення). Є різні
можливості в даному аспекті – так, можна розглядати модель як в [
Ще одне зауваження. В моделі ми зосередимось на роботі з одним переказом. Зрозуміло, що робота з різними переказами, хоч і виконувана в паралель, не інтерферує (немає взаємного впливу процесів авторизації різних переказів один на інший, адже такими процесами зачіпаються рядки таблиць, перетин яких є порожнім – оскільки вони мають принаймні різні коди переказів). Тому ми явно не будемо вказувати ні номер переказу, ні інформацію щодо нього.
Уточнення процедури авторизації. Нехай у нас є три таблиці: інформаційна (про перекази) Inf, авторизаційна (журнал авторизацій та спроб) Auth та таблиця з інформацією щодо блокувань Block. Авторизаційна таблиця містить кортежі зі станом спроб авторизації – “виплачено” (тобто авторизована виплата), “спроба авторизації” (зараз відбувається, in progress) та “відмова” (із зазначенням причини). Розглянемо ситуацію роботи з деяким переказом з кодом Invoice. Позначимо кількості рядків в цих таблицях наступним чином:
A – кількість виплат переказу Invoice, тобто кількість рядків таблиці Auth, які відносяться до Invoice та мають статус “виплачено”,
P – кількість паралельних (одночасних) спроб авторизації (виплати) переказу, тобто кількість рядків таблиці Auth, які відносяться до Invoice та мають статус “спроба авторизації”,
T – накопичувальна кількість всіх спроб виплати переказу, тобто загальна кількість рядків таблиці Auth, які відносяться до Invoice,
B – блокування переказу (0 = немає, 1 = є), тобто останній стан блокування Invoice, згідно таблиці Block, якщо такі записи є (1 – заблоковано або 0 – розблоковано), або 0, якщо немає відповідних записів в таблиці Block.
Зрозуміло, що значення всіх змінних завжди є невід’ємними цілими числами (це – кількості рядків в таблицях, окрім B, що приймає значення 0 або 1).
Тепер можна виписати процедуру авторизації у вигляді IPCL-програми над станом зі змінними A, P, T, B: Auth_Prog = (T, P) := (T +1, P +1);// фіксація спроби авторизації if ( P = 1 ) then if ( data_provided_correct() ) then
(A, P) := (A +1, P –1) else P := P –1 // фіксація успішної авторизації // завершення авторизації відмовою if ( B = 0 ) then if ( A = 0 ) then else P := P –1 else P := P –1 else P := P –1; if ( T > 2 ) then B := 1 else Id; де data_provided_correct() – предикат, що повертає True, коли передані дані щодо переказу є коректними згідно бази даних переказів (таблиця Inf) та False у протилежному випадку.
Паралельно може виконуватись процес “розблокувати переказ”: Unblock =
B := 0; Семантика відповідних функцій алгебри IPCLA буде визначена природним чином: sem (T, P) := (T +1, P +1) (d) ≡ d ∇ [ T a (T⇒(d) + 1), P a (P⇒(d) + 1) ], sem P = 1 (d) ≡ IF ( P⇒(d) = 1, True, False ), sem B=0 (d) ≡ IF ( B⇒(d) = 0, True, False ), sem A=0 (d) ≡ IF ( A⇒(d) = 0, True, False ), sem data_provided_correct() (d) ≡ choice (True, False), sem (A,P):=(A+1,P–1) (d) ≡ d ∇ [ A a (A⇒(d) + 1), P a (P⇒(d) – 1) ], sem P:=P–1 (d) ≡ d ∇ [ P a (P⇒(d) – 1) ], sem T>2 (d) ≡ IF ( T⇒(d) > 2, True, False ), sem B:=1 (d) ≡ d ∇ [ B a 1 ], sem Id (d) ≡ d (identity, дане не змінюється), sem B:=0 (d) ≡ d ∇ [ B a 0 ], де choice (A, B) – недетермінований вибір між значеннями A та B. Дане d має загальний вигляд d = [ P a p, T a t, A a a, B a b ]. Таким чином, маємо програму в IPCL (точніше, в підкласі – SeqILProgs): Program = Auth_Progn || Unblockm .
Оскільки у нас немає локальних даних (точніше, для спрощення ми від них відмовились – зокрема, в
data_provided_correct()), побудуємо спрощену модель (зі спрощеними станами) [
Auth_Prog = [M1:] (T, P) := (T +1, P +1); if [M2:] ( P = 1 ) then if [M3:] ( B = 0 ) then if [M4:] ( A = 0 ) then if [M5:] ( data_provided_correct() ) then
[M6:] (A, P) := (A +1, P –1) else [M7:] P := P –1 else [M8:] P := P –1 else [M9:] P := P –1 else [M10:] P := P –1; if [M11:] ( T > 2 ) then [M12:] B := 1 else [M13:] Id; [M14:] Unblock = [M15:] B := 0; [M16:] Множина SStates буде представляти собою підмножину N16×D, згідно спрощеного варіанту методу, де D = ND(V, W) – спільні глобальні дані для всіх процесів, причому {A, P, T, B}⊆V та N∪{0}⊆W. Функція SStep (виконання програми Program) буде визначена за цим алгоритмом наступним чином: s14, s15, s16, sem (T,P):=(T+1,P+1) (d)) ) | s1>0 & ∀i∈N16 • si∈N } ∪ s14, s15, s16, d) ) | s2>0 & ∀i∈N16 • si∈N & sem P=1 (d)=True } ∪ s14, s15, s16, d) ) | s2>0 & ∀i∈N16 • si∈N & sem P=1 (d)=False } ∪ s14, s15, s16, d) ) | s3>0 & ∀i∈N16 • si∈N & sem B=0 (d)=True } ∪ s14, s15, s16, d) ) | s3>0 & ∀i∈N16 • si∈N & sem B=0 (d)=False } ∪ s14, s15, s16, sem (A,P):=(A+1,P–1) (d)) ) | s6>0 & ∀i∈N16 • si∈N } ∪ s14, s15, s16, sem P:=P–1 (d)) ) | s7>0 & ∀i∈N16 • si∈N } ∪ s14, s15, s16, sem P:=P–1 (d)) ) | s8>0 & ∀i∈N16 • si∈N } ∪ s14, s15, s16, sem P:=P–1 (d)) ) | s9>0 & ∀i∈N16 • si∈N } ∪ s14, s15, s16, sem P:=P–1 (d)) ) | s10>0 & ∀i∈N16 • si∈N } ∪ s14, s15, s16, d) ) | s11>0 & ∀i∈N16 • si∈N & sem T>2 (d)=True } ∪ s14, s15, s16, d) ) | s11>0 & ∀i∈N16 • si∈N & sem T>2 (d)=False } ∪ s14+1, s15, s16, sem B:=1 (d)) ) | s12>0 & ∀i∈N16 • si∈N } ∪ s14+1, s15, s16, sem Id (d)) ) | s13>0 & ∀i∈N16 • si∈N } ∪ { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12–1, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13–1, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9–1, s10, s11+1, s12, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10–1, s11+1, s12, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11–1, s12+1, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11–1, s12, s13+1, s14, s15, s16, d) ) | s4>0 & ∀i∈N16 • si∈N & sem A=0 (d)=True } ∪ s14, s15, s16, d) ) | s4>0 & ∀i∈N16 • si∈N & sem A=0 (d)=False } ∪ s14, s15, s16, d) ) | s5>0 & ∀i∈N16 • si∈N & sem data_provided_correct() (d)=True } ∪ s14, s15, s16, d) ) | s5>0 & ∀i∈N16 • si∈N & sem data_provided_correct() (d)=False } ∪ { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5–1, s6, s7+1, s8, s9, s10, s11, s12, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6–1, s7, s8, s9, s10, s11+1, s12, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7–1, s8, s9, s10, s11+1, s12, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8–1, s9, s10, s11+1, s12, s13, { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15–1, s16+1, sem B:=0 (d)) ) | s15>0 & ∀i∈N16 • si∈N }, де si – кількість процесів, що знаходяться в позиції (на мітці) [Mi:] в даний момент часу. та
Візьмемо SStartStates = { (n, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, m, 0, d) | n∈N, m∈N, [ P a 0, T a 0, A a 0, B a 0 ] ⊆ d } SStopStates = { s | s=(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, n, 0, m, d’) & n∈N & m∈N & ∃s1, s2, …, sl • (s1∈SStartStates & sl=s & (∀i∈Nl-1 • (si, si+1)∈SStep) ) }.
В даній постановці модель можна розглядати як таку, що описує повний шлях існування (“життєвий цикл”) певного переказу (його спроби авторизації – вдалі та невдалі, блокування та розблокування спеціальним оператором). Оскільки n та m (ступені підпрограм) можуть бути довільними цілими невід’ємними числами, то, дійсно, модель задає довільний можливий шлях роботи з будь-яким одним переказом (іншими словами, сімейство програм). Обробка різних переказів не перетинається – такі процеси обробки переказів не інтерферують. До речі, програма P, зокрема, може перетворитись на послідовне виконання її підпрограм (в довільному ступені), згідно заданої семантики мови IPCL та алгоритму побудови моделі – така ситуація, мабуть, найчастіше виникає на практиці. Але разом з тим програма (і модель) передбачає можливість перетинатись довільним чином операторам (окремим діям) паралельних процесів (згідно заданої семантики – та принципів паралелізму з почерговим виконанням, interleaving concurrency). Отже, модель передбачає і описує всі можливі траси виконання програми Program та системи (авторизації виплати переказів), що моделюється. Доведення коректності
Таким чином, необхідно довести властивість A≤1, якщо на початку роботи A≤1, тобто {A≤1} Program {A≤1}.
Якщо то необхідно показати, що Розглянемо
PreCond(S) = (A⇒(d)≤1), PostCond(S) = (A⇒(d)≤1),
S = (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), ∀S∈SStartStates • ∀S’∈SStopStates • (PreCond(S) & (S, S’)∈SStep → PostCond(S)).
Inv(S) ≡ (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ),
S = (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d).
Цей інваріант, насправді, досить легко утворити, розуміючи логіку програми та описані вище критичні місця. Так, він вказує, що кількість паралельних (конкуруючих) процесів, які намагаються безпосередньо авторизувати даний переказ, не може бути більше одного (s3+s4+s5+s6≤1) – умова (P=1) відсікає інші можливості, при цьому значення A може бути лише 0 або 1. Якщо ж значення є вже 1 (переказ авторизовано і виплачено), то жоден процес не потрапить в “зону безпосередньої авторизації” ( (A⇒(d)=1) & (s5=0) & (s6=0) ). Ще додається одна умова “цілісності” – оператори виконуються у відповідній послідовності, “фантомні” (нові по ходу виконання) програми (підпрограми авторизації) не виникають, а кількість програм в точках перевірки (s2, s3, s4, s5, s6, s7, s8, s9, s10) дорівнює кількості паралельних спроб авторизації даного переказу (P). Більш того, в інваріанті не фігурує змінна B, тобто блокування несуттєво впливають на хід авторизації (з точки зору інтерференції та паралелізму), що зрозуміло з логіки програми. (Отже, оператори, пов’язані з блокуванням, можна було б взагалі опустити з моделі та аналізу.) Згідно методики доведемо, що
InvCond(Inv, PreCond, PostCond) = True, InvCond(Inv, PreCond, PostCond) = ∀S∈SStartStates • ( PreCond(S) → Inv(S) ) & ∀S∈SStopStates • ( Inv(S) → PostCond(S) ) & ∀(S, S’)∈SStep • ( Inv(S) → Inv(S’) ), а також перевіримо, що ∀S∈SStartStates • PreCond(S). Тоді будемо мати ∀S∈SStopStates • PostCond(S).
Оскільки для кожного що випливає з (A⇒(d)≤1), тобто PreCond(S), то ∀S∈SStartStates • ( PreCond(S) → Inv(S) ).
S∈SStartStates, де S = (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), s2=s3=s4=s5=s6=s7=s8=s9=s10=0, P⇒(d)=0 та A⇒(d)=0 ∨ A⇒(d)=1,
∀S∈SStates • ( Inv(S) → PostCond(S) ). { (A⇒(d)=0) → A⇒(d)≤1, (A⇒(d)=1) → A⇒(d)≤1 ⇒ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) → A⇒(d)≤1 } ⇒ ( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) → A⇒(d)≤1 ⇒ (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) )
→ A⇒(d)≤1 = Inv(S) → PostCond(S). ∀S∈SStopStates • ( Inv(S) → PostCond(S) ).
∀(S, S’)∈SStep • ( Inv(S) → Inv(S’) ).
Розглянемо всі пари (S, S’)∈SStep і покажемо, що для кожної такої пари спрощених станів якщо Inv(S), то і Inv(S’). Дослідимо множини пар станів (S, S’)∈SStep “по частинах” (множини “однотипних” перетворень). d’ = sem (T,P):=(T+1,P+1) (d) = d ∇ [ T a (T⇒(d) + 1), P a (P⇒(d) + 1) ].
P⇒(d’) = P⇒(d) + 1, а A⇒(d’) = A⇒(d).
{ ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2–1, s3+1, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s2>0 & ∀i∈N16 • si∈N & sem P=1 (d)=True } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) &
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True,
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem P=1 (d) = (P⇒(d) = 1) = True, тобто P⇒(d) = 1, то з
(s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)), P⇒(d) = 1 та s2>0 випливає, що
s2=1 та s3=s4=s5=s6=s7=s8=s9=s10=0, тоді, враховуючи
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True, Inv(S’) = ((s3+1)+s4+s5+s6≤1) & ((s2–1)+(s3+1)+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True. 3. Розглянемо (S, S’)∈SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2–1, s3, s4, s5, s6, s7, s8, s9, s10+1, s11, s12, s13, s14, s15, s16, d) ) | s2>0 & ∀i∈N16 • si∈N & sem P=1 (d)=False } ∪ Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True,
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem P=1 (d) = (P⇒(d) = 1) = False, то
Inv(S’) = (s3+s4+s5+s6≤1) & ((s2–1)+s3+s4+s5+s6+s7+s8+s9+(s10+1)=P⇒(d)) &
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True.
4. Розглянемо (S, S’)∈SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3–1, s4+1, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s3>0 & ∀i∈N16 • si∈N & sem B=0 (d)=True } { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3–1, s4, s5, s6, s7, s8, s9+1, s10, s11, s12, s13, s14, s15, s16, d) ) | s3>0 & ∀i∈N16 • si∈N & sem B=0 (d)=False }
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem A=0 (d) = (A⇒(d) = 0) = True, тобто A⇒(d) = 0, то
Inv(S’) = (s3+(s4–1)+(s5+1)+s6≤1) & (s2+s3+(s4–1)+(s5+1)+s6+s7+s8+s9+s10=P⇒(d)) &
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & ((s5+1)=0) & (s6=0) ) ) = True, адже перші два кон’юнкти – істинні з передумови (Inv(S) = True), а третій – оскільки A⇒(d) = 0. 7. Розглянемо (S, S’)∈SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4–1, s5, s6, s7, s8+1, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s4>0 & ∀i∈N16 • si∈N & sem A=0 (d)=False }
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem B=0 (d) = (B⇒(d) = 0) = False, то легко побачити, що { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4–1, s5+1, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s4>0 & ∀i∈N16 • si∈N & sem A=0 (d)=True }
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також sem data_provided_correct() (d) = (choice (True, False)) = True, звідси, враховуючи s5>0, маємо s5=1 та s3=s4=s6=0 (випливає з істинності першого кон’юнкта Inv(S)), звідси ( (A⇒(d)=1) & (s5=0) & (s6=0) ) = False, тому (A⇒(d)=0) = True,
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) &(s6=0) ) ) = True, тоді, очевидно,
Inv(S’) = (s3+s4+(s5–1)+(s6+1)≤1) & (s2+s3+s4+(s5–1)+(s6+1)+s7+s8+s9+s10=P⇒(d)) &
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & ((s5–1)=0) & ((s6+1)=0) ) ) = True.
{ ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5–1, s6, s7+1, s8, s9, s10, s11, s12, s13, s14, s15, s16, d) ) | s5>0 & ∀i∈N16 • si∈N & sem data_provided_correct() (d)=False } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True, S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d),
sem data_provided_correct() (d) = (choice (True, False)) = False, ( (A⇒(d)=1) & (s5=0) & (s6=0) ) = False, тому (A⇒(d)=0) = True, звідси, враховуючи s5>0, маємо s5=1 та s3=s4=s6=0 (випливає з істинності першого кон’юнкта Inv(S)), звідси Inv(S’) = (s3+(s4–1)+s5+s6≤1) & (s2+s3+(s4–1)+s5+s6+s7+(s8+1)+s9+s10=P⇒(d)) &
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True (з Inv(S) логічно випливає Inv(S’)).
8. Розглянемо (S, S’)∈SStep : щоб третій кон’юнкт ( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True, тоді
Inv(S’) = (s3+s4+(s5–1)+s6≤1) & (s2+s3+s4+(s5–1)+s6+(s7+1)+s8+s9+s10=P⇒(d)) &
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & ((s5–1)=0) & (s6=0) ) ) = True (перший і другий кон’юнкти випливають з Inv(S), а третій є істинним за рахунок (A⇒(d)=0) = True). 10. Розглянемо (S, S’)∈SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6–1, s7, s8, s9, s10, s11+1, s12, s13, s14, s15, s16, sem (A, P) := (A +1, P –1) (d)) ) | s6>0 & ∀i∈N16 • si∈N } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True,
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), а також s6>0, Inv(S’) = (s3+s4+s5+(s6–1)≤1) & (s2+s3+s4+s5+(s6–1)+s7+s8+s9+s10=P⇒(d’)) & ( (A⇒(d’)=0) ∨ ( (A⇒(d’)=1) & (s5=0) & ((s6–1)=0) ) ), d’ = sem (A, P) := (A +1, P –1) (d) = d ∇ [ A a (A⇒(d) + 1), P a (P⇒(d) – 1) ]. Таким чином, P⇒(d’) = P⇒(d) – 1, а A⇒(d’) = A⇒(d) + 1.
Тепер, з Inv(S) = True випливає, що s3+s4+s5+s6≤1, s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d) та (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) = True. { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7–1, s8, s9, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s7>0 & ∀i∈N16 • si∈N } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+(s7–1)+s8+s9+s10=P⇒(d’)) &
( (A⇒(d’)=0) ∨ ( (A⇒(d’)=1) & (s5=0) & (s6=0) ) ), якщо де то якщо то
Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+(s7–1)+s8+s9+s10=P⇒(d)–1) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 12. Розглянемо (S, S’)∈SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8–1, s9, s10, s11+1, s12, s13, s14, s15, s16, sem P := P –1 (d)) ) | s8>0 & ∀i∈N16 • si∈N } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True, де S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+(s8–1)+s9+s10=P⇒(d’)) & ( (A⇒(d’)=0) ∨ { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9–1, s10, s11+1, s12, s13, s14, s15, s16, sem P:=P–1 (d)) ) | s9>0 & ∀i∈N16 • si∈N }
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+(s9–1)+s10=P⇒(d’)) & ( (A⇒(d’)=0) ∨ де d’ = sem P:=P–1 (d) = d ∇ [ P a (P⇒(d) – 1) ].
Таким чином, P⇒(d’) = P⇒(d) – 1, а A⇒(d’) = A⇒(d). Звідси,
Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+(s9–1)+s10=P⇒(d)–1) & ( (A⇒(d)=0) ∨ { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10–1, s11+1, s12, s13, s14, s15, s16, sem P:=P–1 (d)) ) | s10>0 & ∀i∈N16 • si∈N } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+(s10–1)=P⇒(d’)) &
( (A⇒(d’)=0) ∨ ( (A⇒(d’)=1) & (s5=0) & (s6=0) ) ), де d’ = sem P:=P–1 (d) = d ∇ [ P a (P⇒(d) – 1) ].
Таким чином, P⇒(d’) = P⇒(d) – 1, а A⇒(d’) = A⇒(d).
Звідси, а також sem T>2 (d) = (T⇒(d) > 2) = True, то
Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+(s10–1)=P⇒(d)–1) &
( (A⇒(d)=0) ∨ ( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 15. Розглянемо (S, S’)∈SStep : { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11–1, s12+1, s13, s14, s15, s16, d) ) | s11>0 & ∀i∈N16 • si∈N & sem T>2 (d)=True } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True,
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 16. Розглянемо (S, S’)∈SStep : s13+1, s14, s15, s16, d) ) | s11>0 & ∀i∈N16 • si∈N & sem T>2 (d)=False } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True, а також sem T >2 (d) = (T⇒(d) > 2) = False, то 17. Розглянемо (S, S’)∈SStep :
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+ s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d’)) & ( (A⇒(d’)=0) ∨ де d’ = sem B :=0 (d) = d ∇ [ B a 0 ].
18. Розглянемо (S, S’)∈SStep :
Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨ { ( (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), (s1, s2, s3, s4, s5, s6, s7, s8, s9, s10,
s11, s12, s13–1, s14+1, s15, s16, sem Id (d)) ) | s13>0 & ∀i∈N16 • si∈N } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
S=(s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, d), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d’)) &
( (A⇒(d’)=0) ∨ ( (A⇒(d’)=1) & (s5=0) & (s6=0) ) ), Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = Inv(S) = True. 19. Розглянемо (S, S’)∈SStep : s12, s13, s14, s15–1, s16+1, sem B :=0 (d)) ) | s15>0 & ∀i∈N16 • si∈N } Inv(S) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) & ( (A⇒(d)=0) ∨
( (A⇒(d)=1) & (s5=0) & (s6=0) ) ) = True, Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d’)) &
( (A⇒(d’)=0) ∨ ( (A⇒(d’)=1) & (s5=0) & (s6=0) ) ), Таким чином, P⇒(d’) = P⇒(d), а A⇒(d’) = A⇒(d). Звідси,
Inv(S’) = (s3+s4+s5+s6≤1) & (s2+s3+s4+s5+s6+s7+s8+s9+s10=P⇒(d)) &
InvCond(Inv, PreCond, PostCond) = True.
∀S∈SStartStates • PreCond(S), ∀S∈SStopStates • PostCond(S) InvCond(Inv, PreCond, PostCond) = True.
∀S∈SStates • ( Inv(S) → PostCond(S) ), адже на початку роботи Program записів в таблиці Auth немає і [ A a 0 ]. Тоді автоматично отримаємо звідси необхідна умова (PostCond(S)) виконується на кожному досяжному кроці виконання програми Program. Тобто, фактично, було доведено більш сильне твердження – а саме, що програма є коректною і не порушує задану умову (A≤1) не лише на початку і в кінці, а і на протязі всього часу виконання, тобто на кожному кроці. Тотальна коректність
Оскільки програма не має циклів, ані блокувань, ані інших затримуючих або непередбачуваних факторів, які можуть «зациклити», або зупинити, або якимось чином затримати виконання – вона обов’язково завершить роботу за скінчену кількість кроків. Очевидне обмеження на кількість кроків – n * 9 + m, де 9 – діаметр графу переходів між мітками програми Auth_Prog. Висновки
Застосовано спрощений метод [