स्पार्क (प्रोग्रामिंग लैंग्वेज)

This article is about the programming language. For the cluster computing framework that can run on Scala, Java, and Python, see Apache Spark.

SPARK

File:Sparkada.jpg
Paradigm	Multi-paradigm
Developer	Altran and AdaCore
Stable release	Community 2021 / June 1, 2021 (2021-06-01)
टाइपिंग अनुशासन	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

स्पार्क एडा (प्रोग्रामिंग भाषा ) प्रोग्रामिंग लैंग्वेज पर आधारित प्रोग्रामिंग लैंग्वेज कंप्यूटर प्रोग्रामिंग लैंग्वेज का एक औपचारिक शब्दार्थ है, जिसका उद्देश्य सिस्टम में उपयोग किए जाने वाले उच्च अखंडता सॉफ्टवेयर के विकास के लिए है जहां पूर्वानुमान योग्य और अत्यधिक विश्वसनीय संचालन आवश्यक है। यह उन अनुप्रयोगों के विकास की सुविधा प्रदान करता है जो सुरक्षा, सुरक्षा या व्यावसायिक अखंडता की मांग करते हैं।

मूल रूप से, क्रमशः Ada 83, Ada 95 और Ada 2005 पर आधारित SPARK भाषा (SPARK83, SPARK95, SPARK2005) के तीन संस्करण थे।

स्पार्क भाषा का चौथा संस्करण, स्पार्क 2014, एडा 2012 पर आधारित, 30 अप्रैल 2014 को जारी किया गया था। स्पार्क 2014 भाषा और सहायक सॉफ्टवेयर सत्यापन उपकरणों का एक पूर्ण पुन: डिजाइन है।

स्पार्क भाषा में एडा भाषा का एक अच्छी तरह से परिभाषित उपसमुच्चय होता है जो स्थिर और गतिशील सत्यापन दोनों के लिए उपयुक्त रूप में घटकों के विनिर्देश का वर्णन करने के लिए अनुबंध (सॉफ्टवेयर) का उपयोग करता है।

SPARK83/95/2005 में, अनुबंधों को Ada टिप्पणियों में एन्कोड किया गया है और इसलिए किसी भी मानक Ada संकलक द्वारा अनदेखा किया जाता है, लेकिन SPARK परीक्षक और उससे जुड़े उपकरणों द्वारा संसाधित किया जाता है।

इसके विपरीत, स्पार्क 2014, अनुबंधों को व्यक्त करने के लिए एडा 2012 के बिल्ट-इन आस्पेक्ट सिंटैक्स का उपयोग करता है, उन्हें भाषा के मूल में लाता है। स्पार्क 2014 (जीएनएटीप्रोव) के लिए मुख्य टूल जीएनएटी|जीएनएटी/जीसीसी इंफ्रास्ट्रक्चर पर आधारित है, और जीएनएटी एडा 2012 फ्रंट-एंड की लगभग संपूर्णता का पुन: उपयोग करता है।

तकनीकी सिंहावलोकन

स्पार्क अपनी सभी संभावित अस्पष्टताओं और असुरक्षित निर्माणों को खत्म करने की कोशिश करते हुए एडा की ताकत का उपयोग करता है। स्पार्क प्रोग्राम डिज़ाइन द्वारा स्पष्ट होने के लिए हैं, और उनके व्यवहार को एडा संकलक की पसंद से अप्रभावित होना आवश्यक है। इन लक्ष्यों को आंशिक रूप से एडा की कुछ अधिक समस्याग्रस्त विशेषताओं (जैसे अप्रतिबंधित कार्य समानता) को छोड़ कर और आंशिक रूप से उन अनुबंधों को शुरू करके प्राप्त किया जाता है जो प्रोग्राम के कुछ घटकों के लिए एप्लिकेशन डिज़ाइनर के इरादों और आवश्यकताओं को कूटबद्ध करते हैं।

इन दृष्टिकोणों का संयोजन स्पार्क को अपने डिजाइन उद्देश्यों को पूरा करने की अनुमति देता है, जो हैं:

• तार्किक सुदृढ़ता
• कठोर औपचारिक परिभाषा
• सरल शब्दार्थ
• सुरक्षा
• अभिव्यंजक शक्ति (कंप्यूटर विज्ञान)
• सत्यापन और सत्यापन
• सीमित संसाधन (अंतरिक्ष और समय) आवश्यकताएँ।
• न्यूनतम रनटाइम सिस्टम आवश्यकताएँ

अनुबंध उदाहरण

नीचे एडीए सबप्रोग्राम विनिर्देश पर विचार करें:

प्रक्रिया वृद्धि (एक्स: बाहर काउंटर_टाइप में);

शुद्ध एडा में यह चर को बढ़ा सकता है X एक या एक हजार से; या यह कुछ वैश्विक काउंटर सेट कर सकता है X और काउंटर का मूल मान वापस करें X; या यह बिल्कुल कुछ नहीं कर सकता है X बिलकुल।

स्पार्क 2014 के साथ, एक उपप्रोग्राम वास्तव में क्या करता है, इसके बारे में अतिरिक्त जानकारी प्रदान करने के लिए अनुबंध को कोड में जोड़ा जाता है। उदाहरण के लिए, हम उपरोक्त विनिर्देश को कहने के लिए बदल सकते हैं:

प्रक्रिया वृद्धि (एक्स: बाहर काउंटर_टाइप में)
  वैश्विक => अशक्त के साथ,
       निर्भर करता है => (एक्स => एक्स);

यह निर्दिष्ट करता है कि Increment प्रक्रिया किसी भी वैश्विक चर का उपयोग नहीं करती (न तो अपडेट करती है और न ही पढ़ती है) और वह एकमात्र डेटा आइटम है जिसका उपयोग नए मूल्य की गणना में किया जाता है X है X अपने आप।

वैकल्पिक रूप से, डिजाइनर निर्दिष्ट कर सकता है:

प्रक्रिया वृद्धि (एक्स: बाहर काउंटर_टाइप में)
  वैश्विक => (In_Out => गणना) के साथ,
       निर्भर करता है => (गणना => (गणना, एक्स),
                   एक्स => अशक्त);

यह निर्दिष्ट करता है Increment वैश्विक चर का उपयोग करेगा Count के रूप में एक ही पैकेज में Increment, कि निर्यात मूल्य Count के आयातित मूल्यों पर निर्भर करता है Count और X, और यह कि निर्यात मूल्य X किसी भी चर पर बिल्कुल भी निर्भर नहीं करता है और यह केवल स्थिर डेटा से ही प्राप्त होगा।

यदि जीएनएटीप्रोव को उपप्रोग्राम के विनिर्देश और संबंधित निकाय पर चलाया जाता है, तो यह सूचना प्रवाह के मॉडल को बनाने के लिए उपप्रोग्राम के शरीर का विश्लेषण करेगा। इस मॉडल की तुलना उसके साथ की जाती है जिसे एनोटेशन और उपयोगकर्ता को रिपोर्ट की गई किसी भी विसंगतियों द्वारा निर्दिष्ट किया गया है।

इन विशिष्टताओं को विभिन्न गुणों पर जोर देकर आगे बढ़ाया जा सकता है, जिन्हें या तो तब होल्ड करने की आवश्यकता होती है जब एक सबप्रोग्राम कहा जाता है (पूर्व शर्त) या जो एक बार सबप्रोग्राम के निष्पादन के पूरा हो जाने के बाद होल्ड हो जाएगा (शर्त लगाना)। उदाहरण के लिए, हम निम्नलिखित कह सकते हैं:

'प्रक्रिया' वृद्धि (एक्स: 'इन आउट' काउंटर_टाइप)
'साथ' ग्लोबल => अशक्त,
       निर्भर करता है => (एक्स => एक्स),
       पूर्व => एक्स <काउंटर_टाइप'अंतिम,
       पोस्ट => एक्स = एक्स'ओल्ड + 1;

यह, अब, न केवल यह निर्दिष्ट करता है X अकेले स्वयं से ही प्राप्त होता है, लेकिन उससे पहले भी Increment कहा जाता है X अपने प्रकार के अंतिम संभावित मूल्य से कड़ाई से कम होना चाहिए (यह सुनिश्चित करने के लिए कि परिणाम कभी भी अतिप्रवाह नहीं होगा) और उसके बाद X के प्रारंभिक मूल्य के बराबर होगा X मैं भी सहमत हूं।

सत्यापन की शर्तें

GNATprove सत्यापन स्थिति जनरेटर या वीसी का एक सेट भी उत्पन्न कर सकता है। इन शर्तों का उपयोग यह स्थापित करने के लिए किया जाता है कि क्या कुछ गुण किसी दिए गए सबप्रोग्राम के लिए हैं। कम से कम, GNATprove कुलपतियों को यह स्थापित करने के लिए उत्पन्न करेगा कि सभी रन-टाइम त्रुटियाँ एक सबप्रोग्राम के भीतर नहीं हो सकती हैं, जैसे:

• सरणी सूचकांक सीमा से बाहर
• टाइप रेंज उल्लंघन
• शून्य से विभाजन
• संख्यात्मक अतिप्रवाह।

यदि कोई पोस्टकंडिशन या कोई अन्य अभिकथन एक सबप्रोग्राम में जोड़ा जाता है, तो GNATprove वीसी भी उत्पन्न करेगा जिसके लिए उपयोगकर्ता को यह दिखाने की आवश्यकता होती है कि ये गुण सबप्रोग्राम के माध्यम से सभी संभावित पथों के लिए हैं।

हुड के तहत, GNATprove वीसी को डिस्चार्ज करने के लिए Why3 इंटरमीडिएट लैंग्वेज और VC जेनरेटर, और CVC4, Z3 प्रमेय प्रस्तावक और Alt-Ergo प्रमेय का उपयोग करता है। Why3 टूलसेट के अन्य घटकों के माध्यम से अन्य प्रोवर (इंटरैक्टिव प्रूफ चेकर्स सहित) का उपयोग भी संभव है।

इतिहास

स्पार्क का पहला संस्करण (एडा 83 पर आधारित) बर्नार्ड कैरे और ट्रेवर जेनिंग्स द्वारा साउथेम्प्टन विश्वविद्यालय (ब्रिटेन के रक्षा मंत्रालय (यूनाइटेड किंगडम) के प्रायोजन के साथ) में तैयार किया गया था। SPARK नाम SPADE Ada Kernel से लिया गया था, पास्कल प्रोग्रामिंग भाषा के SPADE उपसमुच्चय के संदर्भ में।

बाद में प्रोग्राम वैलिडेशन लिमिटेड द्वारा और फिर प्रैक्सिस क्रिटिकल सिस्टम्स लिमिटेड द्वारा भाषा को उत्तरोत्तर विस्तारित और परिष्कृत किया गया। 2004 में, प्रैक्सिस क्रिटिकल सिस्टम्स लिमिटेड ने अपना नाम बदलकर प्रैक्सिस हाई इंटीग्रिटी सिस्टम्स लिमिटेड कर दिया। जनवरी 2010 में, कंपनी अल्ट्रॉन अधिनियम बन गई।

2009 की शुरुआत में, प्रैक्सिस ने AdaCore के साथ साझेदारी की, और GPL की शर्तों के तहत स्पार्क प्रो जारी किया। इसके बाद जून 2009 में स्पार्क GPL संस्करण 2009 आया, जिसका लक्ष्य FOSS और अकादमिक समुदाय था।

जून 2010 में, अल्ट्रान-प्रैक्सिस ने घोषणा की कि यूएस लूनर प्रोजेक्ट क्यूबसैट के सॉफ़्टवेयर में स्पार्क प्रोग्रामिंग भाषा का उपयोग किया जाएगा, जिसके 2015 में पूरा होने की उम्मीद है।

जनवरी 2013 में, अल्ट्रान-प्रैक्सिस ने अपना नाम बदलकर अल्ट्रान कर लिया, जो अप्रैल 2021 में कैंपजेमिनी इंजीनियरिंग (इसे पकड़ लो के साथ अल्ट्रान के विलय के बाद) बन गया।

स्पार्क 2014 की पहली प्रो रिलीज़ की घोषणा 30 अप्रैल, 2014 को की गई थी, और दाँत साफ करने का धागा और अकादमिक समुदायों के उद्देश्य से स्पार्क 2014 जीपीएल संस्करण के तुरंत बाद इसका अनुसरण किया गया।

औद्योगिक अनुप्रयोग

सुरक्षा संबंधी प्रणालियाँ

SPARK का उपयोग कई हाई प्रोफाइल सुरक्षा-महत्वपूर्ण प्रणालियों में किया गया है, जिसमें वाणिज्यिक विमानन (रोल्स-रॉयस ट्रेंट श्रृंखला जेट इंजन, ARINC ACAMS सिस्टम, लॉकहीड मार्टिन C-130J सुपर हरक्यूलिस), सैन्य विमानन (यूरोफाइटर टाइफून, हैरियर GR9, Aermacchi) शामिल हैं। M-346), वायु-यातायात प्रबंधन (UK NATS iFACTS सिस्टम), रेल (अनेक सिग्नलिंग अनुप्रयोग), चिकित्सा (लाइफफ्लो वेंट्रिकुलर असिस्ट डिवाइस), और अंतरिक्ष अनुप्रयोग (वर्मोंट लूनर क्यूबसैट)।

सुरक्षा संबंधी प्रणालियाँ

स्पार्क का उपयोग सुरक्षित सिस्टम डेवलपमेंट में भी किया गया है। उपयोगकर्ताओं में शामिल हैं रॉकवेल कॉलिन्स (टर्नस्टाइल और सिक्योरवन क्रॉस-डोमेन समाधान), मूल अनेक सीए का विकास, एनएसए टोकनर डिमॉन्स्ट्रेटर, सेक्यूनेट मल्टी-लेवल वर्कस्टेशन, म्यूएन सेपरेशन कर्नेल और जीनोड ब्लॉक-डिवाइस एनक्रिप्टर।

अगस्त 2010 में, अल्ट्रान प्रैक्सिस के प्रमुख अभियंता रॉड चैपमैन ने SPARK में Sha-3|SHA-3 के उम्मीदवारों में से एक स्केन (हैश फंक्शन) को लागू किया। स्पार्क और सी कार्यान्वयन के प्रदर्शन की तुलना में और सावधानीपूर्वक अनुकूलन के बाद, वह स्पार्क संस्करण को सी की तुलना में केवल 5 से 10% धीमी गति से चलाने में कामयाब रहा। ) प्रदर्शन में C से मेल खाने वाले स्पार्क कोड के साथ अंतर को बंद कर दिया। सुरक्षा-महत्वपूर्ण फर्मवेयर के कार्यान्वयन के लिए NVIDIA ने स्पार्क को भी अपनाया है। 2020 में, रॉड चैपमैन ने स्पार्क 2014 में TweetNaCl क्रिप्टोग्राफ़िक लाइब्रेरी को फिर से लागू किया। लाइब्रेरी के स्पार्क संस्करण में टाइप-सेफ्टी, मेमोरी-सेफ्टी और कुछ शुद्धता गुणों का एक पूर्ण ऑटो-एक्टिव प्रूफ है, और निरंतर-समय के एल्गोरिदम को बनाए रखता है। स्पार्क कोड भी TweetNaCl से काफी तेज है।

यह भी देखें

• जेड अंकन
• जावा मॉडलिंग भाषा

अग्रिम पठन

• 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.

बाहरी संबंध

• SPARK 2014 community site
• SPARK Pro website
• SPARK 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