स्पार्क (प्रोग्रामिंग लैंग्वेज): Difference between revisions
No edit summary |
No edit summary |
||
| Line 57: | Line 57: | ||
शुद्ध एडीए में यह चर <code>X</code> है को एक या एक हजार से बढ़ा सकता है या यह कुछ वैश्विक काउंटर सेट <code>X</code> के लिए और <code>X</code> में काउंटर के मूल मान को वापस कर सकते हैं यह <code>X</code> के साथ बिल्कुल कुछ भी नहीं कर सकता है। | शुद्ध एडीए में यह चर <code>X</code> है को एक या एक हजार से बढ़ा सकता है या यह कुछ वैश्विक काउंटर सेट <code>X</code> के लिए और <code>X</code> में काउंटर के मूल मान को वापस कर सकते हैं यह <code>X</code> के साथ बिल्कुल कुछ भी नहीं कर सकता है। | ||
स्पार्क 2014 के साथ, एक उपप्रोग्राम वास्तव में क्या करता है, इसके बारे में अतिरिक्त जानकारी प्रदान करने के लिए अनुबंध को कोड में जोड़ा जाता है। उदाहरण के लिए, हम उपरोक्त विनिर्देश को कहने के लिए बदल सकते हैं, | स्पार्क 2014 के साथ, एक उपप्रोग्राम वास्तव में क्या करता है, इसके बारे में अतिरिक्त जानकारी प्रदान करने के लिए अनुबंध को कोड में जोड़ा जाता है। उदाहरण के लिए, हम उपरोक्त विनिर्देश को कहने के लिए बदल सकते हैं,<syntaxhighlight lang="c++"> | ||
procedure Increment (X : in out Counter_Type) | |||
with Global => null, | |||
Depends => (X => X); | |||
</syntaxhighlight>यह निर्दिष्ट करता है कि इन्क्रीमेंट प्रक्रिया किसी भी वैश्विक चर का उपयोग नहीं करती और न तो अपडेट करती है और न ही पढ़ती है और <code>X</code> के नए मूल्य की गणना करने में उपयोग की जाने वाली एकमात्र डेटा वस्तु <code>X</code> के रूप में होती है। | |||
वैकल्पिक रूप से, डिजाइनर निर्दिष्ट कर सकता है,<syntaxhighlight lang="c++"> | |||
procedure Increment (X : in out Counter_Type) | |||
with Global => (In_Out => Count), | |||
Depends => (Count => (Count, X), | |||
X => null); | |||
</syntaxhighlight>यह निर्दिष्ट करता है कि इंक्रीमेंट ग्लोबल वैरिएबल काउंट का उपयोग उसी पैकेज में इंक्रीमेंट के रूप में करता है, कि काउंट का निर्यात मूल्य काउंट और <code>X</code>, के आयातित मूल्यों पर निर्भर करता है और <code>X</code> का निर्यात मूल्य किसी भी चर पर निर्भर नहीं करता है और यह केवल स्थिर डेटा से ही प्राप्त होता है। | |||
यह | यदि जीएनएटीप्रोव को उपप्रोग्राम के विनिर्देश और संबंधित निकाय पर चलाया जाता है, तो यह सूचना प्रवाह के मॉडल को बनाने के लिए उपप्रोग्राम के बॉडी का विश्लेषण करता है। इस मॉडल की तुलना उसके साथ की जाती है जिसे एनोटेशन और उपयोगकर्ता को रिपोर्ट की गई किसी भी विसंगतियों द्वारा निर्दिष्ट किया जाता है। | ||
इन विशिष्टताओं को विभिन्न गुणों पर जोर देकर आगे बढ़ाया जाता है, जिन्हें या तो तब होल्ड करने की आवश्यकता होती है जब एक सबप्रोग्राम पूर्व शर्त बनाया जाता है या जो एक बार सबप्रोग्राम के निष्पादन के पूरा हो जाने के बाद [[पोस्टकंडिशन]] को पूरा कर लेता है, जैसे हम निम्नलिखित उदाहरण के रूप में देख सकते हैं<syntaxhighlight lang="c++"> | |||
procedure Increment (X : in out Counter_Type) | |||
with Global => null, | |||
Depends => (X => X), | |||
Pre => X < Counter_Type'Last, | |||
Post => X = X'Old + 1; | |||
</syntaxhighlight>यह अब न केवल यह निर्दिष्ट करता है कि <code>X</code> केवल स्वयं से ही प्राप्त होता है, लेकिन उससे पहले भी इन्क्रीमेंट को <code>X</code> कहा जाता है, जो अपने प्रकार के अंतिम संभावित मूल्य से कम होना चाहिए, ताकि यह सुनिश्चित करने के लिए कि परिणाम कभी भी अतिप्रवाह नहीं होता है और उसके बाद में <code>X</code> के बराबर होगा जो <code>X</code> प्लस वन के प्रारंभिक मूल्य के बराबर होता है। | |||
इन विशिष्टताओं को विभिन्न गुणों पर जोर देकर आगे बढ़ाया | |||
यह | |||
== सत्यापन की शर्तें == | == सत्यापन की शर्तें == | ||
Revision as of 21:30, 8 March 2023
 | This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages)
(Learn how and when to remove this template message)
|
| File:Sparkada.jpg | |
| Paradigm | Multi-paradigm |
|---|---|
| Developer | Altran and AdaCore |
| Stable release | Community 2021
/ June 1, 2021 |
| टाइपिंग अनुशासन | static, strong, safe, nominative |
| ओएस | Cross-platform: Linux, Microsoft Windows, Mac OS X |
| लाइसेंस | GPLv3 |
| वेबसाइट | About SPARK |
| Major implementations | |
| SPARK Pro, SPARK GPL Edition, SPARK Community | |
| Influenced by | |
| Ada, Eiffel | |
स्पार्क एडीए ( प्रोग्रामिंग लैंग्वेज ) प्रोग्रामिंग लैंग्वेज पर आधारित एक औपचारिक रूप से परिभाषित कंप्यूटर प्रोग्रामिंग लैंग्वेज होती है, जिसका उद्देश्य प्रणालियों में उपयोग किए जाने वाले उच्च इंटेग्रिटी सॉफ्टवेयर के विकास के लिए उद्धिष्ट होती है, जहां अपेक्षा के योग्य और अत्यधिक विश्वसनीय संचालन आवश्यक होता है। यह सुरक्षा तथा व्यावसायिक सत्यनिष्ठा की मांग करने वाले अनुप्रयोगों के विकास की सुविधा प्रदान करते है।
मूल रूप से, स्पार्क लैंग्वेज के तीन संस्करण क्रमशः स्पार्क83, स्पार्क95, स्पार्क2005 थे जो क्रमशः एडीए 83, एडीए 95, एडीए 2005 पर आधारित थे।
एडीए 2012 पर आधारित स्पार्क लैंग्वेज, स्पार्क 2014 का चौथा संस्करण 30 अप्रैल 2014 को रिलीज़ किया गया। स्पार्क 2014 लैंग्वेज का एक पूर्ण पुन: डिजाइन और सॉफ्टवेयर सत्यापन उपकरण का समर्थन है।
स्पार्क लैंग्वेज में एडीए लैंग्वेज का एक अच्छी तरह से परिभाषित उपसमुच्चय होता है, जो स्थिर और गतिशील सत्यापन दोनों के लिए उपयुक्त रूप में घटकों के विनिर्देश का वर्णन करने के लिए अनुबंध (सॉफ्टवेयर) का उपयोग करता है।
स्पार्क83/स्पार्क95/स्पार्क2005 में, अनुबंधों को एडीए टिप्पणियों में एन्कोड किया गया है और इसलिए किसी भी मानक एडीए कम्पाइलर द्वारा अनदेखा किया जाता है, लेकिन स्पार्क परीक्षक और उससे जुड़े उपकरणों द्वारा संसाधित किया जाता है।
इसके विपरीत, स्पार्क 2014, अनुबंधों को व्यक्त करने के लिए एडीए 2012 के बिल्ट-इन एस्पेक्ट सिंटैक्स का उपयोग करता है, उन्हें लैंग्वेज के मूल रूप में लाता है। स्पार्क 2014 जीएनएटीप्रोव के लिए मुख्य टूल जीएनएटी|जीएनएटी/जीसीसी इंफ्रास्ट्रक्चर पर आधारित होता है और जीएनएटी एडीए 2012 फ्रंट-एंड की लगभग संपूर्णता का पुन: उपयोग करता है।
प्रोद्योगिकीय संक्षिप्त विवरण
स्पार्क एडीए की क्षमताओं का उपयोग करते हुए अपनी सभी संभावित अस्पष्टताओं और असुरक्षित निर्माणों को खत्म करने का प्रयास करता है। स्पार्क प्रोग्राम डिज़ाइन द्वारा स्पष्ट होता है और एडीए कंपाइलर के चयन से उनके व्यवहार को अप्रभावित रखना आवश्यक होता है। इन लक्ष्यों को आंशिक रूप से एडीए की कुछ अधिक समस्याग्रस्त विशेषताओं जैसे अप्रतिबंधित कार्य समानता को छोड़ कर और आंशिक रूप से उन अनुबंधों को प्रारंभ करके प्राप्त किया जाता है जो प्रोग्राम के कुछ घटकों के लिए अनुप्रयोग डिज़ाइनर के प्रयोजन और आवश्यकताओं को कूटबद्ध या एन्कोड करते हैं।
इन दृष्टिकोणों का संयोजन स्पार्क को अपने डिजाइन उद्देश्यों को पूरा करने की अनुमति देता है, जो इस प्रकार है
- तार्किक सुदृढ़ता
- कठोर औपचारिक परिभाषा
- सरल शब्दार्थ
- सुरक्षा
- अभिव्यंजक शक्ति (कंप्यूटर विज्ञान)
- सत्यापनीयता
- सीमित संसाधन क्षेत्र और समय की आवश्यकताओ के रूप में होती है।
- न्यूनतम रनटाइम प्रणाली आवश्यकताओ के रूप में होती है।
अनुबंध उदाहरण
नीचे एडीए सबप्रोग्राम विनिर्देश पर विचार करते है, जो इस प्रकार है
procedure Increment (X : in out Counter_Type);
शुद्ध एडीए में यह चर X है को एक या एक हजार से बढ़ा सकता है या यह कुछ वैश्विक काउंटर सेट X के लिए और X में काउंटर के मूल मान को वापस कर सकते हैं यह X के साथ बिल्कुल कुछ भी नहीं कर सकता है।
स्पार्क 2014 के साथ, एक उपप्रोग्राम वास्तव में क्या करता है, इसके बारे में अतिरिक्त जानकारी प्रदान करने के लिए अनुबंध को कोड में जोड़ा जाता है। उदाहरण के लिए, हम उपरोक्त विनिर्देश को कहने के लिए बदल सकते हैं,
procedure Increment (X : in out Counter_Type)
with Global => null,
Depends => (X => X);
यह निर्दिष्ट करता है कि इन्क्रीमेंट प्रक्रिया किसी भी वैश्विक चर का उपयोग नहीं करती और न तो अपडेट करती है और न ही पढ़ती है और X के नए मूल्य की गणना करने में उपयोग की जाने वाली एकमात्र डेटा वस्तु X के रूप में होती है।
वैकल्पिक रूप से, डिजाइनर निर्दिष्ट कर सकता है,
procedure Increment (X : in out Counter_Type)
with Global => (In_Out => Count),
Depends => (Count => (Count, X),
X => null);
यह निर्दिष्ट करता है कि इंक्रीमेंट ग्लोबल वैरिएबल काउंट का उपयोग उसी पैकेज में इंक्रीमेंट के रूप में करता है, कि काउंट का निर्यात मूल्य काउंट और X, के आयातित मूल्यों पर निर्भर करता है और X का निर्यात मूल्य किसी भी चर पर निर्भर नहीं करता है और यह केवल स्थिर डेटा से ही प्राप्त होता है।
यदि जीएनएटीप्रोव को उपप्रोग्राम के विनिर्देश और संबंधित निकाय पर चलाया जाता है, तो यह सूचना प्रवाह के मॉडल को बनाने के लिए उपप्रोग्राम के बॉडी का विश्लेषण करता है। इस मॉडल की तुलना उसके साथ की जाती है जिसे एनोटेशन और उपयोगकर्ता को रिपोर्ट की गई किसी भी विसंगतियों द्वारा निर्दिष्ट किया जाता है।
इन विशिष्टताओं को विभिन्न गुणों पर जोर देकर आगे बढ़ाया जाता है, जिन्हें या तो तब होल्ड करने की आवश्यकता होती है जब एक सबप्रोग्राम पूर्व शर्त बनाया जाता है या जो एक बार सबप्रोग्राम के निष्पादन के पूरा हो जाने के बाद पोस्टकंडिशन को पूरा कर लेता है, जैसे हम निम्नलिखित उदाहरण के रूप में देख सकते हैं
procedure Increment (X : in out Counter_Type)
with Global => null,
Depends => (X => X),
Pre => X < Counter_Type'Last,
Post => X = X'Old + 1;
यह अब न केवल यह निर्दिष्ट करता है कि X केवल स्वयं से ही प्राप्त होता है, लेकिन उससे पहले भी इन्क्रीमेंट को X कहा जाता है, जो अपने प्रकार के अंतिम संभावित मूल्य से कम होना चाहिए, ताकि यह सुनिश्चित करने के लिए कि परिणाम कभी भी अतिप्रवाह नहीं होता है और उसके बाद में X के बराबर होगा जो X प्लस वन के प्रारंभिक मूल्य के बराबर होता है।
सत्यापन की शर्तें
GNATprove सत्यापन स्थिति जनरेटर या वीसी का एक सेट भी उत्पन्न कर सकता है। इन शर्तों का उपयोग यह स्थापित करने के लिए किया जाता है कि क्या कुछ गुण किसी दिए गए सबप्रोग्राम के लिए हैं। कम से कम, GNATprove कुलपतियों को यह स्थापित करने के लिए उत्पन्न करेगा कि सभी रन-टाइम त्रुटियाँ एक सबप्रोग्राम के भीतर नहीं हो सकती हैं, जैसे:
- सरणी सूचकांक सीमा से बाहर
- टाइप रेंज उल्लंघन
- शून्य से विभाजन
- संख्यात्मक अतिप्रवाह।
यदि कोई पोस्टकंडिशन या कोई अन्य अभिकथन एक सबप्रोग्राम में जोड़ा जाता है, तो GNATprove वीसी भी उत्पन्न करेगा जिसके लिए उपयोगकर्ता को यह दिखाने की आवश्यकता होती है कि ये गुण सबप्रोग्राम के माध्यम से सभी संभावित पथों के लिए हैं।
हुड के अनुसार , GNATprove वीसी को डिस्चार्ज करने के लिए Why3 इंटरमीडिएट लैंग्वेज और VC जेनरेटर, और CVC4, Z3 प्रमेय प्रस्तावक और Alt-Ergo प्रमेय का उपयोग करता है। Why3 टूलसेट के अन्य घटकों के माध्यम से अन्य प्रोवर (इंटरैक्टिव प्रूफ चेकर्स सहित) का उपयोग भी संभव है।
इतिहास
स्पार्क का पहला संस्करण (एडीए 83 पर आधारित) बर्नार्ड कैरे और ट्रेवर जेनिंग्स द्वारा साउथेम्प्टन विश्वविद्यालय (ब्रिटेन के रक्षा मंत्रालय (यूनाइटेड किंगडम) के प्रायोजन के साथ) में तैयार किया गया था। स्पार्क नाम SPADE एडीए Kernel से लिया गया था, पास्कल प्रोग्रामिंग लैंग्वेज के SPADE उपसमुच्चय के संदर्भ में।[1]
बाद में प्रोग्राम वैलिडेशन लिमिटेड द्वारा और फिर प्रैक्सिस क्रिटिकल प्रणाली ्स लिमिटेड द्वारा लैंग्वेज को उत्तरोत्तर विस्तारित और परिष्कृत किया गया। 2004 में, प्रैक्सिस क्रिटिकल प्रणाली ्स लिमिटेड ने अपना नाम बदलकर प्रैक्सिस हाई इंटीग्रिटी प्रणाली ्स लिमिटेड कर दिया। जनवरी 2010 में, कंपनी अल्ट्रॉन अधिनियम बन गई।
2009 की शुरुआत में, प्रैक्सिस ने एडीए Core के साथ साझेदारी की, और GPL की शर्तों के अनुसार स्पार्क प्रो जारी किया। इसके बाद जून 2009 में स्पार्क GPL संस्करण 2009 आया, जिसका लक्ष्य FOSS और अकादमिक समुदाय था।
जून 2010 में, अल्ट्रान-प्रैक्सिस ने घोषणा की कि यूएस लूनर प्रोजेक्ट क्यूबसैट के सॉफ़्टवेयर में स्पार्क प्रोग्रामिंग लैंग्वेज का उपयोग किया जाएगा, जिसके 2015 में पूरा होने की उम्मीद है।
जनवरी 2013 में, अल्ट्रान-प्रैक्सिस ने अपना नाम बदलकर अल्ट्रान कर लिया, जो अप्रैल 2021 में कैंपजेमिनी इंजीनियरिंग (इसे पकड़ लो के साथ अल्ट्रान के विलय के बाद) बन गया।
स्पार्क 2014 की पहली प्रो रिलीज़ की घोषणा 30 अप्रैल, 2014 को की गई थी, और दाँत साफ करने का धागा और अकादमिक समुदायों के उद्देश्य से स्पार्क 2014 जीपीएल संस्करण के तुरंत बाद इसका अनुसरण किया गया।
औद्योगिक अनुप्रयोग
सुरक्षा संबंधी प्रणालियाँ
स्पार्क का उपयोग कई हाई प्रोफाइल सुरक्षा-महत्वपूर्ण प्रणालियों में किया गया है, जिसमें वाणिज्यिक विमानन (रोल्स-रॉयस ट्रेंट श्रृंखला जेट इंजन, ARINC ACAMS प्रणाली , लॉकहीड मार्टिन C-130J सुपर हरक्यूलिस), सैन्य विमानन (यूरोफाइटर टाइफून, हैरियर GR9, Aermacchi) सम्मलित हैं। M-346), वायु-यातायात प्रबंधन (UK NATS iFACTS प्रणाली ), रेल (अनेक सिग्नलिंग अनुप्रयोग), चिकित्सा (लाइफफ्लो वेंट्रिकुलर असिस्ट डिवाइस), और अंतरिक्ष अनुप्रयोग (वर्मोंट लूनर क्यूबसैट)।[citation needed]
सुरक्षा संबंधी प्रणालियाँ
स्पार्क का उपयोग सुरक्षित प्रणाली डेवलपमेंट में भी किया गया है। उपयोगकर्ताओं में सम्मलित हैं रॉकवेल कॉलिन्स (टर्नस्टाइल और सिक्योरवन क्रॉस-डोमेन समाधान), मूल अनेक सीए का विकास, एनएसए टोकनर डिमॉन्स्ट्रेटर, सेक्यूनेट मल्टी-लेवल वर्कस्टेशन, म्यूएन सेपरेशन कर्नेल और जीनोड ब्लॉक-डिवाइस एनक्रिप्टर।
अगस्त 2010 में, अल्ट्रान प्रैक्सिस के प्रमुख अभियंता रॉड चैपमैन ने स्पार्क में Sha-3|SHA-3 के उम्मीदवारों में से एक स्केन (हैश फंक्शन) को लागू किया। स्पार्क और सी कार्यान्वयन के प्रदर्शन की तुलना में और सावधानीपूर्वक अनुकूलन के बाद, वह स्पार्क संस्करण को सी की तुलना में केवल 5 से 10% धीमी गति से चलाने में कामयाब रहा। ) प्रदर्शन में C से मेल खाने वाले स्पार्क कोड के साथ अंतर को बंद कर दिया।[2] सुरक्षा-महत्वपूर्ण फर्मवेयर के कार्यान्वयन के लिए NVIDIA ने स्पार्क को भी अपनाया है।[3] 2020 में, रॉड चैपमैन ने स्पार्क 2014 में TweetNaCl क्रिप्टोग्राफ़िक लाइब्रेरी को फिर से लागू किया।[4] लाइब्रेरी के स्पार्क संस्करण में टाइप-सेफ्टी, मेमोरी-सेफ्टी और कुछ शुद्धता गुणों का एक पूर्ण ऑटो-एक्टिव प्रूफ है, और निरंतर-समय के एल्गोरिदम को बनाए रखता है। स्पार्क कोड भी TweetNaCl से अधिक तेज है।
यह भी देखें
संदर्भ
- ↑ "चिंगारी - कुदाल एडा कर्नेल (RavenSPARK सहित)". AdaCore. Retrieved 30 June 2021.
- ↑ Handy, Alex (24 August 2010). "एडा-व्युत्पन्न स्केन क्रिप्टो स्पार्क दिखाता है". SD Times. BZ Media LLC. Retrieved 31 August 2010.
- ↑ "एंबेडेड सॉफ़्टवेयर की सुरक्षा और सुरक्षा के भविष्य को सुरक्षित करना". 8 January 2020.
- ↑ "स्पार्कनासीएल". GitHub. 8 October 2021.
अग्रिम पठन
- John Barnes (2012). SPARK: The Proven Approach to High Integrity Software. Altran Praxis. ISBN 978-0-9572905-1-8.
- John W. McCormick and Peter C. Chapin (2015). Building High Integrity Applications with SPARK 2014. Cambridge University Press. ISBN 978-1-107-65684-0.
- Philip E. Ross (September 2005). "The Exterminators". IEEE Spectrum. 42 (9): 36–41. doi:10.1109/MSPEC.2005.1502527. ISSN 0018-9235. S2CID 26369398.
बाहरी संबंध
- स्पार्क 2014 community site
- स्पार्क Pro website
- स्पार्क Libre (GPL) Edition website
- Altran
- Correctness by Construction: A Manifesto for High-Integrity Software Archived 30 October 2012 at the Wayback Machine
- UK's Safety-Critical Systems Club
- Comparison with a C specification language (Frama C)
- Tokeneer Project Page
- Muen Kernel Public Release
- LifeFlow LVAD Project
- VTU CubeSat Project
