Safety and liveness properties
કમ્પ્યુટર પ્રોગ્રામના અમલીકરણના ગુણધર્મો-ખાસ કરીને સહવર્તી અને વિતરિત સિસ્ટમો માટે-લાંબા સમયથી સલામતી ગુણધર્મો ("ખરાબ વસ્તુઓ થતી નથી") અને જીવંત ગુણધર્મો ("સારી વસ્તુઓ થાય છે") આપીને ઘડવામાં આવ્યા છે. એક સરળ ઉદાહરણ સલામતી અને જીવંતતા સમજાવશે. પૂર્વશરત અને પછીની શરતના સંદર્ભમાં કાર્યક્રમ સંપૂર્ણપણે સાચો છે જો સંતોષકારક સ્થિતિમાં શરૂ થયેલ કોઈપણ અમલ સંતોષકારક સ્થિતિમાં સમાપ્ત થાય છે. સંપૂર્ણ શુદ્ધતા એ સલામતી મિલકત અને જીવંત મિલકતનો સંયોજન છેઃ સલામતી મિલકત આ "ખરાબ વસ્તુઓ" ને પ્રતિબંધિત કરે છેઃ ફાંસીની સજા જે સંતોષકારક સ્થિતિમાં શરૂ થાય છે અને અંતિમ સ્થિતિમાં સમાપ્ત થાય છે જે સંતોષ આપતી નથી. પ્રોગ્રામ માટે, આ સુરક્ષા ગુણધર્મ સામાન્ય રીતે હોર ટ્રિપલનો ઉપયોગ કરીને લખવામાં આવે છે. જીવંતતા ગુણધર્મ, "સારી બાબત" એ છે કે જે અમલ સંતોષકારક સ્થિતિમાં શરૂ થાય છે તે સમાપ્ત થાય છે. નોંધ લો કે ખરાબ વસ્તુ અલગ છે, કારણ કે તે અમલ દરમિયાન ચોક્કસ જગ્યાએ થાય છે. એક "સારી વસ્તુ" અલગ હોવી જરૂરી નથી, પરંતુ સમાપ્તિનો જીવંત ગુણધર્મ અલગ છે. ઔપચારિક વ્યાખ્યાઓ કે જે આખરે સલામતીના ગુણધર્મો અને જીવંત ગુણધર્મો માટે પ્રસ્તાવિત કરવામાં આવી હતી તે દર્શાવે છે કે આ વિઘટન માત્ર સહજ ભાવે જ આકર્ષક નથી પણ તે સંપૂર્ણ પણ છેઃ અમલના તમામ ગુણધર્મો સલામતી અને જીવંત ગુણધર્મોનું સંયોજન છે. વધુમાં, વિઘટન હાથ ધરવું મદદરૂપ થઈ શકે છે, કારણ કે ઔપચારિક વ્યાખ્યાઓ એ સાબિતીને સક્ષમ કરે છે કે સલામતીના ગુણધર્મોની ચકાસણી માટે વિરુદ્ધ જીવંત ગુણધર્મોની ચકાસણી માટે વિવિધ પદ્ધતિઓનો ઉપયોગ કરવો આવશ્યક છે. સલામતી સલામતી મિલકત અમલ દરમિયાન થતી અલગ ખરાબ વસ્તુઓને પ્રતિબંધિત કરે છે. સુરક્ષા મિલકત આમ જે પ્રતિબંધિત છે તે કહીને જેની મંજૂરી છે તેની લાક્ષણિકતા દર્શાવે છે. ખરાબ વસ્તુ અલગ હોવાની જરૂરિયાતનો અર્થ એ છે કે અમલ દરમિયાન થતી ખરાબ વસ્તુ જરૂરી રીતે અમુક ઓળખી શકાય તેવા બિંદુ પર થાય છે. સલામતીની મિલકતને વ્યાખ્યાયિત કરવા માટે ઉપયોગમાં લઈ શકાય તેવી એક અલગ ખરાબ વસ્તુના ઉદાહરણોમાં નીચેનાનો સમાવેશ થાય છેઃ આપેલ પૂર્વશરતને સંતોષતી સ્થિતિમાં શરૂ થતું અમલ સમાપ્ત થાય છે, પરંતુ અંતિમ સ્થિતિ જરૂરી પોસ્ટ શરતને સંતોષતી નથી; બે સહવર્તી પ્રક્રિયાઓનો અમલ, જ્યાં બંને પ્રક્રિયાઓ માટેનો પ્રોગ્રામ કાઉન્ટર્સ નિર્ણાયક વિભાગમાં નિવેદનોને નિયુક્ત કરે છે; બે સહવર્તી પ્રક્રિયાઓનો અમલ જ્યાં દરેક પ્રક્રિયા બીજી સ્થિતિ બદલવાની રાહ જોઈ રહી હોય (જેને ડેડલોક તરીકે ઓળખવામાં આવે છે). પ્રોગ્રામના અમલીકરણને પ્રોગ્રામના અનંત ક્રમ આપીને ઔપચારિક રીતે વર્ણવી શકાય છે જે જણાવે છે કે અમલીકરણની પ્રગતિ તરીકે પરિણામ આવે છે, જ્યાં સમાપ્ત થતા પ્રોગ્રામ માટેની છેલ્લી સ્થિતિ અનંત રીતે પુનરાવર્તિત થાય છે. રસના પ્રોગ્રામ માટે, ચાલો સંભવિત પ્રોગ્રામ સ્થિતિઓના સમૂહને સૂચવીએ, પ્રોગ્રામ સ્થિતિઓના મર્યાદિત ક્રમના સમૂહને સૂચવીએ અને પ્રોગ્રામ સ્થિતિઓના અનંત ક્રમના સમૂહને સૂચવીએ. સંબંધ સિક્વન્સ માટે ધરાવે છે અને આઇએફએફ એ અથવા સમાનનો ઉપસર્ગ છે. કાર્યક્રમની મિલકત એ માન્ય ફાંસીનો સમૂહ છે. સલામતી મિલકતની આવશ્યક લાક્ષણિકતા એ છે કેઃ જો અમુક અમલ સંતોષકારક ન હોય તો તે સલામતી મિલકત માટે વ્યાખ્યાયિત ખરાબ વસ્તુ અમુક સમયે થાય છે. નોંધ લો કે આવી ખરાબ વસ્તુ પછી, જો વધુ અમલ અમલમાં પરિણમે છે, તો તે પણ સંતોષકારક નથી, કારણ કે ખરાબ વસ્તુ પણ થાય છે. અમે ખરાબ વસ્તુઓની અપરિવર્તનીયતા વિશેના આ અનુમાનને સલામતીની મિલકત તરીકે વ્યાખ્યાયિત કરવાની લાક્ષણિકતા તરીકે લઈએ છીએ. પ્રેડિકેટ લોજિકમાં આને ઔપચારિક બનાવવાથી સલામતીની મિલકત હોવાની ઔપચારિક વ્યાખ્યા મળે છે. સલામતી ગુણધર્મો માટેની આ ઔપચારિક વ્યાખ્યા સૂચવે છે કે જો અમલ સલામતી ગુણધર્મને સંતોષે છે તો દરેક ઉપસર્ગ (છેલ્લી સ્થિતિ પુનરાવર્તિત સાથે) પણ સંતોષે છે. જીવંતતા એ જીવંતતા ગુણધર્મ દરેક અમલ માટે સારી વસ્તુઓ સૂચવે છે અથવા, સમાનરૂપે, અમલ દરમિયાન જે થવું જોઈએ તેનું વર્ણન કરે છે. સારી વસ્તુ અલગ હોવી જરૂરી નથી-તેમાં અનંત સંખ્યામાં પગલાં સામેલ હોઈ શકે છે. જીવંત ગુણધર્મને વ્યાખ્યાયિત કરવા માટે ઉપયોગમાં લેવાતી સારી વસ્તુના ઉદાહરણોમાં નીચેનાનો સમાવેશ થાય છેઃ યોગ્ય સ્થિતિમાં શરૂ કરવામાં આવેલા અમલને સમાપ્ત કરવો; યોગ્ય સ્થિતિમાં શરૂ કરવામાં આવેલા અમલને સમાપ્ત ન કરવો; જ્યારે પણ પ્રવેશનો પ્રયાસ કરવામાં આવે ત્યારે નિર્ણાયક વિભાગમાં અંતિમ પ્રવેશની ખાતરી આપવી; વિવાદની હાજરીમાં સ્રોતની વાજબી પહોંચ. પ્રથમ ઉદાહરણમાં સારી બાબત અલગ છે પરંતુ અન્યમાં નહીં. ચોક્કસ વાસ્તવિક સમયની મર્યાદામાં જવાબ રજૂ કરવો એ જીવંત મિલકતને બદલે સલામતીની મિલકત છે. આનું કારણ એ છે કે એક અલગ ખરાબ વસ્તુ પર પ્રતિબંધ મૂકવામાં આવી રહ્યો છેઃ એક આંશિક અમલ જે એવી સ્થિતિમાં પહોંચે છે જ્યાં જવાબ હજુ પણ રજૂ કરવામાં આવ્યો નથી અને ઘડિયાળનું મૂલ્ય (એક સ્થિતિ ચલ) બંધનું ઉલ્લંઘન કરે છે. ડેડલોક સ્વતંત્રતા એ સલામતીની મિલકત છેઃ "ખરાબ વસ્તુ" એ ડેડલોક છે (જે અલગ છે). મોટાભાગે, એ જાણીને કે પ્રોગ્રામ આખરે કેટલીક "સારી વસ્તુઓ" કરે છે તે સંતોષકારક નથી; આપણે જાણવા માગીએ છીએ કે પ્રોગ્રામ અમુક પગલાંઓમાં અથવા અમુક સમયમર્યાદા પહેલાં "સારી વસ્તુઓ" કરે છે. જે મિલકત "સારી વસ્તુ" ને ચોક્કસ બંધન આપે છે તે સલામતી મિલકત છે (ઉપર નોંધ્યા મુજબ), જ્યારે નબળી મિલકત જે ફક્ત બંધન અસ્તિત્વમાં હોવાનો દાવો કરે છે તે જીવંત મિલકત છે. આવી જીવંત મિલકતને સાબિત કરવી એ કડક સલામતી મિલકતને સાબિત કરવા કરતાં સરળ હોવાની શક્યતા છે કારણ કે જીવંત મિલકતને સાબિત કરવા માટે સલામતી મિલકતને સાબિત કરવા માટે જરૂરી વિગતવાર હિસાબની જરૂર નથી. સલામતી મિલકતથી અલગ પાડવા માટે, જીવંત મિલકત અમલના કોઈપણ મર્યાદિત ઉપસર્ગને નકારી શકતી નથી (કારણ કે આવી મિલકત "ખરાબ વસ્તુ" હશે અને, આમ, સલામતી મિલકતને વ્યાખ્યાયિત કરશે). તે જીવંત ગુણધર્મને એવી મિલકત તરીકે વ્યાખ્યાયિત કરવા તરફ દોરી જાય છે જે કોઈપણ મર્યાદિત ઉપસર્ગને નકારી ન શકે. આ વ્યાખ્યા કોઈ સારી વસ્તુને અલગ હોવા સુધી મર્યાદિત કરતી નથી-સારી વસ્તુમાં તમામનો સમાવેશ થઈ શકે છે, જે અનંત લંબાઈનો અમલ છે. ઇતિહાસ લેમ્પોર્ટે મલ્ટીપ્રોસેસ (સહવર્તી) કાર્યક્રમોની ચોકસાઈ સાબિત કરવા પર તેમના 1977 ના પેપરમાં સલામતી મિલકત અને જીવંતતા મિલકત શબ્દોનો ઉપયોગ કર્યો હતો. તેમણે પેટ્રી નેટ થિયરીમાંથી શબ્દો ઉધાર લીધા હતા, જે પેટ્રી નેટના "ટોકન્સ" ની સોંપણી તેના "સ્થાનો" પર કેવી રીતે વિકસિત થઈ શકે છે તેનું વર્ણન કરવા માટે જીવંતતા અને બાઉન્ડનેસ શબ્દોનો ઉપયોગ કરી રહી હતી; પેટ્રી નેટ સલામતી એ બાઉન્ડનેસનું ચોક્કસ સ્વરૂપ હતું. ત્યારબાદ લેમ્પોર્ટે મ્યુનિકમાં ડિસ્ટ્રિબ્યુટેડ સિસ્ટમ્સ પર નાટોના ટૂંકા અભ્યાસક્રમ માટે સલામતીની ઔપચારિક વ્યાખ્યા વિકસાવી. એવું માનવામાં આવે છે કે હઠીલાપણામાં ગુણધર્મો અપરિવર્તનશીલ હોય છે. ઉપર આપેલી સલામતીની ઔપચારિક વ્યાખ્યા એલ્પર્ન અને સ્નેઇડરના પેપરમાં દેખાય છે; સલામતીના ગુણધર્મોના બે ઔપચારિકરણો વચ્ચેનું જોડાણ એલ્પર્ન, ડેમર્સ અને સ્નેઇડરના પેપરમાં દેખાય છે. એલ્પર્ન અને શ્નાઇડર જીવંતતા માટે ઔપચારિક વ્યાખ્યા આપે છે, તેની સાથે પુરાવા છે કે તમામ ગુણધર્મો સલામતીના ગુણધર્મો અને જીવંતતાના ગુણધર્મોનો ઉપયોગ કરીને બનાવી શકાય છે. તે પુરાવો ગોર્ડન પ્લોટકિનની આંતરદૃષ્ટિથી પ્રેરિત હતો કે સલામતીના ગુણધર્મો બંધ સમૂહોને અનુરૂપ છે અને જીવંતતાના ગુણધર્મો પ્રોગ્રામ સ્થિતિઓના અનંત ક્રમના સમૂહ પર કુદરતી ટોપોલોજીમાં ગાઢ સમૂહોને અનુરૂપ છે. ત્યારબાદ, અલ્પર્ન અને સ્નેઇડરએ સલામતીના ગુણધર્મો અને જીવંત ગુણધર્મોની ઔપચારિક વ્યાખ્યાઓ માટે માત્ર બુચી ઓટોમેટન લાક્ષણિકતા જ આપી ન હતી, પરંતુ સલામતીના ગુણધર્મોની ચકાસણી માટે અપરિવર્તનની જરૂર પડશે અને જીવંત ગુણધર્મોની ચકાસણી માટે સારી-પાયાની દલીલની જરૂર પડશે તે બતાવવા માટે આ ઓટોમેટા ફોર્મ્યુલેશનનો ઉપયોગ કર્યો હતો. મિલકતના પ્રકાર (સલામતી વિરુદ્ધ જીવંતતા) અને પુરાવાના પ્રકાર (અસ્થિરતા વિરુદ્ધ સારી રીતે સ્થાપિતતા) વચ્ચેનો પત્રવ્યવહાર એ એક મજબૂત દલીલ હતી કે મિલકતનું સલામતી અને જીવંતતામાં વિઘટન (અન્ય કોઈ વિભાજનના વિરોધમાં) ઉપયોગી હતું-સાબિત કરવા માટે મિલકતના પ્રકારને જાણવું એ પુરાવાના પ્રકારને નિર્ધારિત કરે છે જે જરૂરી છે. સંદર્ભો સમવર્તી કમ્પ્યુટિંગ સૈદ્ધાંતિક કોમ્પ્યુટર વિજ્ઞાન મોડેલ ચકાસણી