ചെന്നായ, ആട്, കാബേജ് പ്രശ്നത്തിന്റെ ഉദാഹരണം ഉപയോഗിച്ച് ഔപചാരിക പരിശോധന

എന്റെ അഭിപ്രായത്തിൽ, ഇൻറർനെറ്റിന്റെ റഷ്യൻ ഭാഷാ മേഖലയിൽ, ഔപചാരിക സ്ഥിരീകരണത്തിന്റെ വിഷയം വേണ്ടത്ര ഉൾക്കൊള്ളുന്നില്ല, പ്രത്യേകിച്ച് ലളിതവും വ്യക്തവുമായ ഉദാഹരണങ്ങളുടെ അഭാവമുണ്ട്.

ഒരു വിദേശ സ്രോതസ്സിൽ നിന്ന് ഞാൻ ഒരു ഉദാഹരണം നൽകും, ഒപ്പം നദിയുടെ മറുകരയിലേക്ക് ചെന്നായ, ആട്, കാബേജ് എന്നിവ കടക്കുന്നതിനുള്ള അറിയപ്പെടുന്ന പ്രശ്നത്തിന് എന്റെ സ്വന്തം പരിഹാരം ചേർക്കുകയും ചെയ്യും.

എന്നാൽ ആദ്യം, ഔപചാരിക സ്ഥിരീകരണം എന്താണെന്നും എന്തുകൊണ്ട് അത് ആവശ്യമാണെന്നും ഞാൻ ചുരുക്കമായി വിവരിക്കും.

ഔപചാരിക സ്ഥിരീകരണം സാധാരണയായി ഒരു പ്രോഗ്രാം അല്ലെങ്കിൽ അൽഗോരിതം ഉപയോഗിച്ച് മറ്റൊന്ന് പരിശോധിക്കുക എന്നാണ് അർത്ഥമാക്കുന്നത്.

പ്രോഗ്രാം പ്രതീക്ഷിച്ചതുപോലെ പ്രവർത്തിക്കുന്നുവെന്ന് ഉറപ്പാക്കാനും അതിന്റെ സുരക്ഷ ഉറപ്പാക്കാനും ഇത് ആവശ്യമാണ്.

കേടുപാടുകൾ കണ്ടെത്തുന്നതിനും ഇല്ലാതാക്കുന്നതിനുമുള്ള ഏറ്റവും ശക്തമായ മാർഗമാണ് ഔപചാരിക സ്ഥിരീകരണം: ഒരു പ്രോഗ്രാമിൽ നിലവിലുള്ള എല്ലാ ദ്വാരങ്ങളും ബഗുകളും കണ്ടെത്താനോ അവ നിലവിലില്ലെന്ന് തെളിയിക്കാനോ ഇത് നിങ്ങളെ അനുവദിക്കുന്നു.
8 സ്ക്വയറുകളുള്ള ബോർഡ് വീതിയുള്ള 1000 രാജ്ഞികളുടെ പ്രശ്നം പോലെ ചില സന്ദർഭങ്ങളിൽ ഇത് അസാധ്യമാണ് എന്നത് ശ്രദ്ധിക്കേണ്ടതാണ്: ഇതെല്ലാം അൽഗോരിതം സങ്കീർണ്ണതയിലേക്കോ നിർത്തുന്ന പ്രശ്നത്തിലേക്കോ വരുന്നു.

എന്നിരുന്നാലും, ഏത് സാഹചര്യത്തിലും, മൂന്ന് ഉത്തരങ്ങളിൽ ഒന്ന് ലഭിക്കും: പ്രോഗ്രാം ശരിയാണ്, തെറ്റാണ്, അല്ലെങ്കിൽ ഉത്തരം കണക്കാക്കാൻ കഴിഞ്ഞില്ല.

ഉത്തരം കണ്ടെത്തുന്നത് അസാധ്യമാണെങ്കിൽ, പ്രോഗ്രാമിന്റെ വ്യക്തമല്ലാത്ത ഭാഗങ്ങൾ പുനർനിർമ്മിക്കാനും അവയുടെ അൽഗോരിതം സങ്കീർണ്ണത കുറയ്ക്കാനും, ഒരു നിർദ്ദിഷ്ട അതെ അല്ലെങ്കിൽ ഇല്ല എന്ന ഉത്തരം ലഭിക്കുന്നതിന് പലപ്പോഴും സാധ്യമാണ്.

കൂടാതെ ഔപചാരിക സ്ഥിരീകരണം ഉപയോഗിക്കുന്നു, ഉദാഹരണത്തിന്, വിൻഡോസ് കേർണലിലും ഡാർപ ഡ്രോൺ ഓപ്പറേറ്റിംഗ് സിസ്റ്റങ്ങളിലും, പരമാവധി പരിരക്ഷ ഉറപ്പാക്കാൻ.

യാന്ത്രിക സിദ്ധാന്തം തെളിയിക്കുന്നതിനും സമവാക്യം പരിഹരിക്കുന്നതിനുമുള്ള വളരെ ശക്തമായ ഉപകരണമായ Z3Prover ഞങ്ങൾ ഉപയോഗിക്കും.

കൂടാതെ, Z3 സമവാക്യങ്ങൾ പരിഹരിക്കുന്നു, മാത്രമല്ല ബ്രൂട്ട് ഫോഴ്‌സ് ഉപയോഗിച്ച് അവയുടെ മൂല്യങ്ങൾ തിരഞ്ഞെടുക്കുന്നില്ല.
ഇൻപുട്ട് ഓപ്ഷനുകളുടെ 10^100 കോമ്പിനേഷനുകൾ ഉള്ള സന്ദർഭങ്ങളിൽ പോലും ഇതിന് ഉത്തരം കണ്ടെത്താൻ കഴിയുമെന്നാണ് ഇതിനർത്ഥം.

എന്നാൽ ഇത് ഇന്റിജറിന്റെ ഒരു ഡസൻ ഇൻപുട്ട് ആർഗ്യുമെന്റുകൾ മാത്രമാണ്, ഇത് പലപ്പോഴും പ്രായോഗികമായി നേരിടാറുണ്ട്.

8 രാജ്ഞികളെക്കുറിച്ചുള്ള പ്രശ്നം (ഇംഗ്ലീഷിൽ നിന്ന് എടുത്തത് മാനുവൽ).

# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]

# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]

# At most one queen per column
col_c = [ Distinct(Q) ]

# Diagonal constraint
diag_c = [ If(i == j,
              True,
              And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
           for i in range(8) for j in range(i) ]

solve(val_c + col_c + diag_c)

Z3 പ്രവർത്തിപ്പിക്കുമ്പോൾ, നമുക്ക് പരിഹാരം ലഭിക്കും:

[Q_5 = 1,
 Q_8 = 7,
 Q_3 = 8,
 Q_2 = 2,
 Q_6 = 3,
 Q_4 = 6,
 Q_7 = 5,
 Q_1 = 4]

8 രാജ്ഞികളുടെ കോർഡിനേറ്റുകൾ ഇൻപുട്ടായി എടുക്കുകയും രാജ്ഞികൾ പരസ്പരം തോൽപ്പിക്കുന്നുണ്ടോ എന്ന ഉത്തരം നൽകുന്ന ഒരു പ്രോഗ്രാമുമായി താരതമ്യപ്പെടുത്താവുന്നതാണ് രാജ്ഞി പ്രശ്നം.

ഔപചാരിക സ്ഥിരീകരണം ഉപയോഗിച്ച് അത്തരമൊരു പ്രോഗ്രാം പരിഹരിക്കണമെങ്കിൽ, പ്രശ്‌നവുമായി താരതമ്യപ്പെടുത്തുമ്പോൾ, പ്രോഗ്രാം കോഡ് ഒരു സമവാക്യമാക്കി മാറ്റുന്ന രൂപത്തിൽ ഞങ്ങൾ ഒരു ചുവട് കൂടി എടുക്കേണ്ടതുണ്ട്: ഇത് നമ്മുടേതിന് സമാനമായി മാറും ( തീർച്ചയായും, പ്രോഗ്രാം ശരിയായി എഴുതിയിട്ടുണ്ടെങ്കിൽ).

കേടുപാടുകൾക്കായി തിരയുന്ന കാര്യത്തിലും ഏതാണ്ട് ഇതുതന്നെ സംഭവിക്കും: ഞങ്ങൾക്ക് ആവശ്യമായ ഔട്ട്‌പുട്ട് വ്യവസ്ഥകൾ ഞങ്ങൾ സജ്ജീകരിക്കുന്നു, ഉദാഹരണത്തിന്, അഡ്മിൻ പാസ്‌വേഡ്, ഉറവിടം അല്ലെങ്കിൽ ഡീകംപൈൽ ചെയ്ത കോഡ് സ്ഥിരീകരണത്തിന് അനുയോജ്യമായ സമവാക്യങ്ങളാക്കി മാറ്റുക, തുടർന്ന് എന്താണെന്നതിന് ഉത്തരം നേടുക. ലക്ഷ്യം നേടുന്നതിന് ഇൻപുട്ടായി ഡാറ്റ നൽകേണ്ടതുണ്ട്.

എന്റെ അഭിപ്രായത്തിൽ, ചെന്നായ, ആട്, കാബേജ് എന്നിവയെക്കുറിച്ചുള്ള പ്രശ്നം കൂടുതൽ രസകരമാണ്, കാരണം ഇത് പരിഹരിക്കുന്നതിന് ഇതിനകം നിരവധി (7) ഘട്ടങ്ങൾ ആവശ്യമാണ്.

ഒരൊറ്റ GET അല്ലെങ്കിൽ POST അഭ്യർത്ഥന ഉപയോഗിച്ച് നിങ്ങൾക്ക് ഒരു സെർവറിലേക്ക് തുളച്ചുകയറാൻ കഴിയുന്ന സാഹചര്യവുമായി താരതമ്യപ്പെടുത്താവുന്നതാണോ രാജ്ഞിയുടെ പ്രശ്നം എങ്കിൽ, ചെന്നായ, ആട്, കാബേജ് എന്നിവ കൂടുതൽ സങ്കീർണ്ണവും വ്യാപകവുമായ വിഭാഗത്തിൽ നിന്ന് ഒരു ഉദാഹരണം കാണിക്കുന്നു, അതിൽ ലക്ഷ്യം നേടാനാകും. നിരവധി അഭ്യർത്ഥനകൾ വഴി.

ഇത് താരതമ്യപ്പെടുത്താവുന്നതാണ്, ഉദാഹരണത്തിന്, നിങ്ങൾ ഒരു SQL കുത്തിവയ്പ്പ് കണ്ടെത്തുകയും അതിലൂടെ ഒരു ഫയൽ എഴുതുകയും തുടർന്ന് നിങ്ങളുടെ അവകാശങ്ങൾ ഉയർത്തുകയും തുടർന്ന് ഒരു പാസ്വേഡ് നേടുകയും ചെയ്യേണ്ട ഒരു സാഹചര്യവുമായി താരതമ്യം ചെയ്യാം.

പ്രശ്നത്തിന്റെ വ്യവസ്ഥകളും അതിന്റെ പരിഹാരവുംകർഷകന് ഒരു ചെന്നായ, ആട്, കാബേജ് എന്നിവ നദിക്ക് കുറുകെ കൊണ്ടുപോകേണ്ടതുണ്ട്. കർഷകനു പുറമെ ഒരു വസ്തുവിനെ മാത്രം ഉൾക്കൊള്ളാൻ കഴിയുന്ന ഒരു ബോട്ട് കർഷകനുണ്ട്. കർഷകൻ അവരെ ശ്രദ്ധിക്കാതെ വിട്ടാൽ ചെന്നായ ആടിനെയും ആട് കാബേജിനെയും തിന്നും.

4-ാം ഘട്ടത്തിൽ കർഷകൻ ആടിനെ തിരികെ കൊണ്ടുപോകേണ്ടി വരും എന്നതാണ് പരിഹാരം.
ഇനി നമുക്ക് അത് പ്രോഗ്രാമാറ്റിക് ആയി പരിഹരിക്കാൻ തുടങ്ങാം.

കർഷകൻ, ചെന്നായ, ആട്, കാബേജ് എന്നിവയെ 4 അല്ലെങ്കിൽ 0 മൂല്യം മാത്രം എടുക്കുന്ന 1 വേരിയബിളുകളായി സൂചിപ്പിക്കാം. പൂജ്യം എന്നാൽ ഇടതുകരയിലാണെന്നും ഒന്ന് വലതുവശത്താണെന്നും അർത്ഥമാക്കുന്നു.

import json
from z3 import *
s = Solver()
Num= 8

Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ]
Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ]
Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ]
Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ]

# Each creature can be only on left (0) or right side (1) on every state
HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]
WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]
GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]
CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]
Side = HumanSide+WolfSide+GoatSide+CabbageSide

പരിഹരിക്കാൻ ആവശ്യമായ ഘട്ടങ്ങളുടെ എണ്ണമാണ് സംഖ്യ. ഓരോ ഘട്ടവും നദിയുടെയും ബോട്ടിന്റെയും എല്ലാ ഘടകങ്ങളുടെയും അവസ്ഥയെ പ്രതിനിധീകരിക്കുന്നു.

ഇപ്പോൾ, നമുക്ക് ഇത് ക്രമരഹിതമായി തിരഞ്ഞെടുക്കാം, ഒരു മാർജിൻ ഉപയോഗിച്ച്, 10 എടുക്കുക.

ഓരോ എന്റിറ്റിയും 10 കോപ്പികളായി പ്രതിനിധീകരിക്കുന്നു - ഇത് ഓരോ 10 ഘട്ടങ്ങളിലും അതിന്റെ മൂല്യമാണ്.

ഇനി തുടക്കത്തിനും പൂർത്തീകരണത്തിനുമുള്ള വ്യവസ്ഥകൾ ക്രമീകരിക്കാം.

Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]

അപ്പോൾ ചെന്നായ ആടിനെ തിന്നുന്നതോ ആട് കാബേജ് തിന്നുന്നതോ ആയ വ്യവസ്ഥകൾ സമവാക്യത്തിലെ നിയന്ത്രണങ്ങളായി ഞങ്ങൾ സജ്ജമാക്കുന്നു.
(ഒരു കർഷകന്റെ സാന്നിധ്യത്തിൽ, ആക്രമണം അസാധ്യമാണ്)

# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]

അവസാനമായി, അങ്ങോട്ടോ തിരിച്ചുപോകുമ്പോഴോ കർഷകന്റെ സാധ്യമായ എല്ലാ പ്രവർത്തനങ്ങളും ഞങ്ങൾ നിർവ്വചിക്കും.
അയാൾക്ക് ഒന്നുകിൽ ഒരു ചെന്നായയെയോ ആടിനെയോ കാബേജിനെയോ കൂടെ കൊണ്ടുപോകാം, അല്ലെങ്കിൽ ആരെയും കൊണ്ടുപോകരുത്, അല്ലെങ്കിൽ എവിടേയും യാത്ര ചെയ്യരുത്.

തീർച്ചയായും, കർഷകനില്ലാതെ ആർക്കും കടക്കാൻ കഴിയില്ല.

നദി, ബോട്ട്, എന്റിറ്റി എന്നിവയുടെ ഓരോ തുടർന്നുള്ള അവസ്ഥയും മുമ്പത്തേതിൽ നിന്ന് കർശനമായി പരിമിതമായ രീതിയിൽ മാത്രമേ വ്യത്യാസപ്പെട്ടിരിക്കൂ എന്ന വസ്തുത ഇത് പ്രകടിപ്പിക്കും.

2 ബിറ്റുകളിൽ കൂടരുത്, കൂടാതെ മറ്റ് നിരവധി പരിധികളോടെയും, കർഷകന് ഒരു സമയത്ത് ഒരു സ്ഥാപനം മാത്രമേ കൊണ്ടുപോകാൻ കഴിയൂ, എല്ലാവരെയും ഒരുമിച്ച് വിടാൻ കഴിയില്ല.

Travel = [ Or(
And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]

നമുക്ക് പരിഹാരം പ്രവർത്തിപ്പിക്കാം.

solve(Side + Start + Finish + Safe + Travel)

നമുക്ക് ഉത്തരം ലഭിക്കും!

എല്ലാ വ്യവസ്ഥകളും തൃപ്തിപ്പെടുത്തുന്ന സ്ഥിരമായ ഒരു കൂട്ടം സംസ്ഥാനങ്ങൾ Z3 കണ്ടെത്തി.
സ്ഥല-സമയത്തിന്റെ ഒരു തരം ചതുരാകൃതിയിലുള്ള കാസ്റ്റ്.

എന്താണ് സംഭവിച്ചതെന്ന് നമുക്ക് മനസ്സിലാക്കാം.

അവസാനം എല്ലാവരും കടന്നുവെന്ന് ഞങ്ങൾ കാണുന്നു, ആദ്യം ഞങ്ങളുടെ കർഷകൻ വിശ്രമിക്കാൻ തീരുമാനിച്ചു, ആദ്യത്തെ 2 ഘട്ടങ്ങളിൽ അവൻ എവിടെയും നീന്തുന്നില്ല.

Human_2 = 0
Human_3 = 0

ഞങ്ങൾ തിരഞ്ഞെടുത്ത സംസ്ഥാനങ്ങളുടെ എണ്ണം അമിതമാണെന്നും 8 മതിയാകുമെന്നും ഇത് സൂചിപ്പിക്കുന്നു.

ഞങ്ങളുടെ കാര്യത്തിൽ, കർഷകൻ ഇത് ചെയ്തു: ആരംഭിക്കുക, വിശ്രമിക്കുക, വിശ്രമിക്കുക, ആടിനെ കടക്കുക, പിന്നിലേക്ക് കടക്കുക, കാബേജ് കടക്കുക, ആടിനൊപ്പം മടങ്ങുക, ചെന്നായയെ കടക്കുക, ഒറ്റയ്ക്ക് മടങ്ങുക, ആടിനെ വീണ്ടും വിതരണം ചെയ്യുക.

എന്നാൽ അവസാനം പ്രശ്നം പരിഹരിച്ചു.

#Старт.
 Human_1 = 0
 Wolf_1 = 0
 Goat_1 = 0
 Cabbage_1 = 0
 
 #Фермер отдыхает.
 Human_2 = 0
 Wolf_2 = 0
 Goat_2 = 0
 Cabbage_2 = 0
 
 #Фермер отдыхает.
 Human_3 = 0
 Wolf_3 = 0
 Goat_3 = 0
 Cabbage_3 = 0
 
 #Фермер отвозит козу на нужный берег.
 Human_4 = 1
 Wolf_4 = 0
 Goat_4 = 1
 Cabbage_4 = 0
 
 #Фермер возвращается.
 Human_5 = 0
 Wolf_5 = 0
 Goat_5 = 1
 Cabbage_5 = 0
 
 #Фермер отвозит капусту на нужный берег.
 Human_6 = 1
 Wolf_6 = 0
 Cabbage_6 = 1
 Goat_6 = 1
 
 #Ключевая часть операции: фермер возвращает козу обратно.
 Human_7 = 0
 Wolf_7 = 0
 Goat_7 = 0
 Cabbage_7 = 1
 
 #Фермер отвозит волка на другой берег, где он теперь находится вместе с капустой.
 Human_8 = 1
 Wolf_8 = 1
 Goat_8 = 0
 Cabbage_8 = 1
 
 #Фермер возвращается за козой.
 Human_9 = 0
 Wolf_9 = 1
 Goat_9 = 0
 Cabbage_9 = 1
 
 #Фермер повторно доставляет козу на нужный берег и завершают переправу.
 Human_10 = 1
 Wolf_10 = 1
 Goat_10 = 1
 Cabbage_10 = 1

ഇനി നമുക്ക് വ്യവസ്ഥകൾ മാറ്റാനും പരിഹാരങ്ങളൊന്നുമില്ലെന്ന് തെളിയിക്കാനും ശ്രമിക്കാം.

ഇത് ചെയ്യുന്നതിന്, ഞങ്ങളുടെ ചെന്നായ സസ്യഭക്ഷണം നൽകും, അവൻ കാബേജ് കഴിക്കാൻ ആഗ്രഹിക്കും.
ആപ്ലിക്കേഷൻ സുരക്ഷിതമാക്കുക എന്നതാണ് ഞങ്ങളുടെ ലക്ഷ്യം, പഴുതുകൾ ഇല്ലെന്ന് ഉറപ്പാക്കേണ്ട കേസുമായി ഇതിനെ താരതമ്യം ചെയ്യാം.

 Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]

Z3 ഞങ്ങൾക്ക് ഇനിപ്പറയുന്ന പ്രതികരണം നൽകി:

 no solution

ഇതിനർത്ഥം യഥാർത്ഥത്തിൽ പരിഹാരങ്ങളൊന്നുമില്ല എന്നാണ്.

അങ്ങനെ, കർഷകന് നഷ്ടം കൂടാതെ സർവവ്യാപിയായ ചെന്നായയുമായി കടക്കുക അസാധ്യമാണെന്ന് ഞങ്ങൾ പ്രോഗ്രാമാറ്റിക് ആയി തെളിയിച്ചു.

പ്രേക്ഷകർക്ക് ഈ വിഷയം താൽപ്പര്യമുണ്ടെങ്കിൽ, ഭാവിയിലെ ലേഖനങ്ങളിൽ ഒരു സാധാരണ പ്രോഗ്രാമിനെയോ പ്രവർത്തനത്തെയോ ഔപചാരിക രീതികൾക്ക് അനുയോജ്യമായ ഒരു സമവാക്യമാക്കി മാറ്റുന്നത് എങ്ങനെയെന്ന് ഞാൻ നിങ്ങളോട് പറയും, അത് പരിഹരിക്കുക, അതുവഴി നിയമാനുസൃതമായ എല്ലാ സാഹചര്യങ്ങളും കേടുപാടുകളും വെളിപ്പെടുത്തും. ആദ്യം, അതേ ടാസ്ക്കിൽ, എന്നാൽ ഒരു പ്രോഗ്രാമിന്റെ രൂപത്തിൽ അവതരിപ്പിച്ചു, തുടർന്ന് ക്രമേണ അത് സങ്കീർണ്ണമാക്കുകയും സോഫ്റ്റ്വെയർ വികസനത്തിന്റെ ലോകത്ത് നിന്നുള്ള നിലവിലെ ഉദാഹരണങ്ങളിലേക്ക് നീങ്ങുകയും ചെയ്യുന്നു.

അടുത്ത ലേഖനം ഇതിനകം തയ്യാറാണ്:
ആദ്യം മുതൽ ഒരു ഔപചാരിക സ്ഥിരീകരണ സംവിധാനം ഉണ്ടാക്കുന്നു: PHP, Python എന്നിവയിൽ ഒരു പ്രതീകാത്മക VM എഴുതുന്നു

അതിൽ ഞാൻ പ്രശ്നങ്ങളുടെ ഔപചാരിക പരിശോധനയിൽ നിന്ന് പ്രോഗ്രാമുകളിലേക്ക് നീങ്ങുകയും വിവരിക്കുകയും ചെയ്യുന്നു
അവ എങ്ങനെ സ്വയമേവ ഔപചാരിക നിയമ സംവിധാനങ്ങളാക്കി മാറ്റാം.

അവലംബം: www.habr.com