Safety and liveness properties
एक कंप्यूटर प्रोग्राम के निष्पादन के गुण-विशेष रूप से समवर्ती और वितरित प्रणालियों के लिए-लंबे समय से सुरक्षा गुण ("बुरी चीजें नहीं होती हैं") और जीवंत गुण ("अच्छी चीजें होती हैं") देकर तैयार किए गए हैं। एक सरल उदाहरण सुरक्षा और जीवंतता को स्पष्ट करेगा। पूर्व शर्त और पश्चात शर्त के संबंध में एक कार्यक्रम पूरी तरह से सही है यदि किसी संतोषजनक स्थिति में शुरू किया गया कोई भी निष्पादन संतोषजनक स्थिति में समाप्त हो जाता है। पूर्ण शुद्धता एक सुरक्षा संपत्ति और एक जीवन संपत्ति का संयोजन हैः सुरक्षा संपत्ति इन "बुरी चीजों" को प्रतिबंधित करती हैः ऐसे निष्पादन जो संतोषजनक स्थिति में शुरू होते हैं और अंतिम स्थिति में समाप्त होते हैं जो संतुष्ट नहीं करते हैं। एक कार्यक्रम के लिए, इस सुरक्षा गुण को आमतौर पर होर ट्रिपल का उपयोग करके लिखा जाता है। जीवंतता गुण, "अच्छी बात", यह है कि संतोषजनक स्थिति में शुरू होने वाला निष्पादन समाप्त हो जाता है। ध्यान दें कि एक बुरी चीज असतत है, क्योंकि यह निष्पादन के दौरान एक विशेष स्थान पर होती है। एक "अच्छी चीज" को असतत होने की आवश्यकता नहीं है, लेकिन समाप्ति का जीवंत गुण असतत है। औपचारिक परिभाषाएँ जो अंततः सुरक्षा गुणों और जीवंतता गुणों के लिए प्रस्तावित की गई थीं, उन्होंने प्रदर्शित किया कि यह अपघटन न केवल सहज रूप से आकर्षक है, बल्कि पूर्ण भी हैः निष्पादन के सभी गुण सुरक्षा और जीवंतता गुणों का एक संयोजन हैं। इसके अलावा, अपघटन करना सहायक हो सकता है, क्योंकि औपचारिक परिभाषाएँ इस बात का प्रमाण देती हैं कि सुरक्षा गुणों को सत्यापित करने के लिए बनाम जीवंत गुणों को सत्यापित करने के लिए विभिन्न तरीकों का उपयोग किया जाना चाहिए। सुरक्षा एक सुरक्षा संपत्ति निष्पादन के दौरान होने वाली अलग-अलग बुरी चीजों को प्रतिबंधित करती है। इस प्रकार एक सुरक्षा संपत्ति यह बताती है कि क्या निषिद्ध है। बुरी चीज़ के अलग होने की आवश्यकता का मतलब है कि निष्पादन के दौरान होने वाली एक बुरी चीज़ आवश्यक रूप से किसी पहचान योग्य बिंदु पर होती है। एक असतत बुरी चीज के उदाहरण जिनका उपयोग एक सुरक्षा संपत्ति को परिभाषित करने के लिए किया जा सकता है, उनमें शामिल हैंः एक निष्पादन जो दी गई पूर्व शर्त को पूरा करने वाले राज्य में शुरू होता है, समाप्त हो जाता है, लेकिन अंतिम स्थिति आवश्यक पोस्ट शर्त को पूरा नहीं करती है; दो समवर्ती प्रक्रियाओं का निष्पादन, जहां दोनों प्रक्रियाओं के लिए कार्यक्रम एक महत्वपूर्ण खंड के भीतर बयानों को निर्दिष्ट करता है; दो समवर्ती प्रक्रियाओं का निष्पादन जहां प्रत्येक प्रक्रिया दूसरे की स्थिति बदलने की प्रतीक्षा कर रही है (जिसे गतिरोध के रूप में जाना जाता है)। एक कार्यक्रम के निष्पादन को औपचारिक रूप से कार्यक्रम के अनंत अनुक्रम के रूप में वर्णित किया जा सकता है जो बताता है कि निष्पादन आगे बढ़ता है, जहां एक समाप्ति कार्यक्रम के लिए अंतिम स्थिति को अनंत रूप से दोहराया जाता है। रूचि के कार्यक्रम के लिए, आइए संभावित कार्यक्रम अवस्थाओं के समूह को निरूपित करें, कार्यक्रम अवस्थाओं के परिमित अनुक्रमों के समूह को निरूपित करें, और कार्यक्रम अवस्थाओं के अनंत अनुक्रमों के समूह को निरूपित करें। संबंध अनुक्रमों के लिए होता है और आई. एफ. एफ. एक उपसर्ग या बराबर है। एक कार्यक्रम की संपत्ति अनुमत निष्पादन का समूह है। एक सुरक्षा संपत्ति की आवश्यक विशेषता यह हैः यदि कुछ निष्पादन संतुष्ट नहीं करता है तो उस सुरक्षा संपत्ति के लिए परिभाषित बुरी बात किसी बिंदु पर होती है। ध्यान दें कि इस तरह की बुरी चीज़ के बाद, यदि आगे के निष्पादन के परिणामस्वरूप निष्पादन होता है, तो यह भी संतुष्ट नहीं करता है, क्योंकि बुरी चीज़ भी होती है। हम बुरी चीजों की अपरिवर्तनीयता के बारे में इस निष्कर्ष को एक सुरक्षा संपत्ति होने के लिए परिभाषित विशेषता के रूप में लेते हैं। इसे विधेय तर्क में औपचारिक रूप देने से सुरक्षा गुण होने की औपचारिक परिभाषा मिलती है। सुरक्षा गुणों के लिए इस औपचारिक परिभाषा का तात्पर्य है कि यदि एक निष्पादन एक सुरक्षा गुण को संतुष्ट करता है तो (अंतिम स्थिति को दोहराने के साथ) का प्रत्येक उपसर्ग भी संतुष्ट करता है। जीवंतता एक जीवंतता गुण प्रत्येक निष्पादन के लिए अच्छी चीजों को निर्धारित करता है या, समान रूप से, कुछ ऐसा वर्णन करता है जो निष्पादन के दौरान होना चाहिए। अच्छी बात अलग होने की आवश्यकता नहीं है-इसमें अनंत संख्या में कदम शामिल हो सकते हैं। एक जीवंत संपत्ति को परिभाषित करने के लिए उपयोग की जाने वाली अच्छी चीज़ के उदाहरणों में शामिल हैंः एक निष्पादन की समाप्ति जो एक उपयुक्त स्थिति में शुरू किया जाता है; एक निष्पादन की गैर-समाप्ति जो एक उपयुक्त स्थिति में शुरू किया जाता है; जब भी प्रवेश का प्रयास किया जाता है तो एक महत्वपूर्ण खंड में अंतिम प्रवेश की गारंटी; विवाद की उपस्थिति में एक संसाधन तक उचित पहुंच। पहले उदाहरण में अच्छी बात अलग है लेकिन दूसरों में नहीं। एक निर्दिष्ट वास्तविक समय सीमा के भीतर एक उत्तर प्रस्तुत करना एक जीवन संपत्ति के बजाय एक सुरक्षा संपत्ति है। ऐसा इसलिए है क्योंकि एक असतत बुरी चीज़ को प्रतिबंधित किया जा रहा हैः एक आंशिक निष्पादन जो उस स्थिति में पहुँचता है जहाँ उत्तर अभी भी प्रस्तुत नहीं किया गया है और घड़ी का मूल्य (एक अवस्था चर) सीमा का उल्लंघन करता है। डेडलॉक स्वतंत्रता एक सुरक्षा संपत्ति हैः "बुरी चीज" एक गतिरोध है (जो असतत है)। अधिकांश समय, यह जानना कि एक कार्यक्रम अंततः कुछ "अच्छा काम" करता है, संतोषजनक नहीं है; हम यह जानना चाहते हैं कि कार्यक्रम कुछ चरणों के भीतर या कुछ समय सीमा से पहले "अच्छा काम" करता है। एक संपत्ति जो "अच्छी चीज़" को एक विशिष्ट सीमा देती है वह एक सुरक्षा संपत्ति है (जैसा कि ऊपर उल्लेख किया गया है), जबकि कमजोर संपत्ति जो केवल सीमा का दावा करती है वह एक जीवंत संपत्ति है। इस तरह की जीवंतता संपत्ति को साबित करना सख्त सुरक्षा संपत्ति को साबित करने की तुलना में आसान होने की संभावना है क्योंकि जीवंतता संपत्ति को साबित करने के लिए उस तरह के विस्तृत लेखांकन की आवश्यकता नहीं होती है जो सुरक्षा संपत्ति को साबित करने के लिए आवश्यक है। एक सुरक्षा संपत्ति से अलग होने के लिए, एक जीवंत संपत्ति एक निष्पादन के किसी भी सीमित उपसर्ग से इंकार नहीं कर सकती है (क्योंकि ऐसा एक "बुरी बात" होगी और इस प्रकार, एक सुरक्षा संपत्ति को परिभाषित करना होगा)। यह एक जीवंतता गुण को एक ऐसी संपत्ति के रूप में परिभाषित करने की ओर ले जाता है जो किसी भी सीमित उपसर्ग से इंकार नहीं करती है। यह परिभाषा एक अच्छी चीज़ को असतत होने तक सीमित नहीं करती है-अच्छी चीज़ में सभी शामिल हो सकते हैं, जो एक अनंत-लंबाई निष्पादन है। इतिहास लैम्पोर्ट ने बहु-प्रक्रिया (समवर्ती) कार्यक्रमों की शुद्धता को साबित करने पर अपने 1977 के पेपर में सुरक्षा संपत्ति और जीवन संपत्ति शब्दों का उपयोग किया। उन्होंने पेट्री नेट सिद्धांत से शब्दों को उधार लिया, जो यह वर्णन करने के लिए जीवंतता और सीमा शब्द का उपयोग कर रहा था कि पेट्री नेट के "टोकन" को उसके "स्थानों" के लिए कैसे विकसित किया जा सकता है; पेट्री नेट सुरक्षा सीमा का एक विशिष्ट रूप था। लैम्पोर्ट ने बाद में म्यूनिख में वितरित प्रणालियों पर एक नाटो लघु पाठ्यक्रम के लिए सुरक्षा की एक औपचारिक परिभाषा विकसित की। यह माना गया कि हकलाने के तहत गुण अपरिवर्तनीय हैं। ऊपर दी गई सुरक्षा की औपचारिक परिभाषा अल्पर्न और श्नाइडर द्वारा एक पेपर में दिखाई देती है; सुरक्षा गुणों के दो औपचारिकरणों के बीच संबंध अल्पर्न, डेमर्स और श्नाइडर द्वारा एक पेपर में दिखाई देता है। एल्पर्न और श्नाइडर जीवंतता के लिए औपचारिक परिभाषा देते हैं, एक प्रमाण के साथ कि सभी गुणों का निर्माण सुरक्षा गुणों और जीवंतता गुणों का उपयोग करके किया जा सकता है। यह प्रमाण गॉर्डन प्लॉटकिन की अंतर्दृष्टि से प्रेरित था कि सुरक्षा गुण बंद सेटों के अनुरूप होते हैं और जीवंतता गुण कार्यक्रम अवस्थाओं के अनंत अनुक्रमों के सेट पर एक प्राकृतिक टोपोलॉजी में घने सेटों के अनुरूप होते हैं। इसके बाद, अल्पर्न और श्नाइडर ने न केवल सुरक्षा गुणों और जीवंत गुणों की औपचारिक परिभाषाओं के लिए एक बुची स्वचालित लक्षण वर्णन दिया, बल्कि इन स्वचालित सूत्रीकरणों का उपयोग यह दिखाने के लिए किया कि सुरक्षा गुणों के सत्यापन के लिए एक अपरिवर्तनीय और जीवंत गुणों के सत्यापन के लिए एक अच्छी तरह से स्थापित तर्क की आवश्यकता होगी। संपत्ति के प्रकार (सुरक्षा बनाम जीवन) के साथ प्रमाण के प्रकार (अपरिवर्तनीयता बनाम अच्छी नींव) के बीच पत्राचार एक मजबूत तर्क था कि संपत्ति का सुरक्षा और जीवन में अपघटन (किसी अन्य विभाजन के विपरीत) एक उपयोगी था-यह जानना कि संपत्ति के प्रकार को साबित किया जाना है, उस प्रमाण के प्रकार को निर्धारित करता है जिसकी आवश्यकता होती है। संदर्भ समवर्ती संगणना सैद्धांतिक कंप्यूटर विज्ञान मॉडल जाँच