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

स्पार्क

File:Sparkada.jpg
Paradigm	बहु-प्रतिमान
Developer	अल्ट्रान और एडाकोर
Stable release	समुदाय 2021 / June 1, 2021 (2021-06-01)
टाइपिंग अनुशासन	स्थैतिक, मजबूत, सुरक्षित, नामकारक
ओएस	क्रॉस-प्लेटफ़ॉर्म: लिनक्स, माइक्रोसॉफ्ट विंडोज़, मैक ओएस एक्स
लाइसेंस	जीपीएलवी3
वेबसाइट	About SPARK
Major implementations
स्पार्क प्रो, स्पार्क जीपीएल संस्करण, स्पार्क समुदाय
Influenced by
एडा, एफिल

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

मूल रूप से, स्पार्क लैंग्वेज के तीन संस्करण क्रमशः स्पार्क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 प्लस वन के प्रारंभिक मूल्य के बराबर होता है।

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

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

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

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

हुड के अनुसार, जीएनएटी प्रोव वीसी को डिस्चार्ज करने के लिए वाई3 इंटरमीडिएट लैंग्वेज और वीसी जेनरेटर और सीवीसी4, जेड3 और ऑल्ट एर्गो प्रमेय का उपयोग करता है। वाई3 टूलसेट के अन्य घटकों के माध्यम से इंटरैक्टिव प्रूफ चेकर्स सहित अन्य प्रोवर का उपयोग भी संभव होता है।

इतिहास

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

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

2009 के प्रारम्भ में, प्रैक्सिस ने एडीए कोर के साथ साझेदारी की और जीपीएल की शर्तों के अनुसार स्पार्क प्रो जारी किया। इसके बाद जून 2009 में स्पार्क जीपीएल संस्करण 2009 में आया, जिसका लक्ष्य एफओएसएस और अकादमिक कम्युनिटीज के रूप में उपयोग में लाया गया था ।

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

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

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

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

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

स्पार्क का उपयोग कई हाई प्रोफाइल सुरक्षा महत्वपूर्ण प्रणालियों में किया गया है, जिसमें वाणिज्यिक उड्‌डयन, रोल्स-रॉयस ट्रेंट श्रृंखला जेट इंजन, एआरआईएनसी एसीएएमएस प्रणाली, लॉकहीड मार्टिन सी-130जे सुपर हरक्यूलिस, सैन्य विमानन यूरोफाइटर टाइफून, हैरियर GR9, एयरमाची एम346 के रूप में सम्मलित हैं। वायु-यातायात प्रबंधन यूके एनएटीएस आईफैक्ट्स प्रणाली, रेल कई सिग्नलिंग अनुप्रयोग, चिकित्सा लाइफफ्लो वेंट्रिकुलर असिस्ट उपकरण और अंतरिक्ष अनुप्रयोग वर्मोंट लूनर क्यूबसैट के रूप में सम्मलित हैं।

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

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

अगस्त 2010 में, अल्ट्रान प्रैक्सिस के प्रमुख इंजीनियर रॉड चैपमैन ने स्पार्क में एसएचए-3 के उम्मीदवारों में से एक स्केन हैश फंक्शन को लागू किया। स्पार्क और सी कार्यान्वयन के प्रदर्शन की तुलना में और सावधानीपूर्वक अनुकूलन के बाद वह स्पार्क संस्करण को सी की तुलना में केवल 5 से 10% धीमी गति से चलाने में कामयाब रहा। और प्रदर्शन में सी से मेल खाने वाले स्पार्क कोड के साथ अंतर को बंद कर दिया।

सुरक्षा-महत्वपूर्ण फर्मवेयर के कार्यान्वयन के लिए एनवीआईडीआईए ने स्पार्क को भी अपनाया है।

2020 में, रॉड चैपमैन ने स्पार्क 2014 में ट्वीट एनएसीएल क्रिप्टोग्राफ़िक लाइब्रेरी को फिर से लागू किया। लाइब्रेरी के स्पार्क संस्करण में टाइप-सेफ्टी, मेमोरी-सेफ्टी और कुछ शुद्धता गुणों का एक पूर्ण ऑटो-एक्टिव प्रूफ है और निरंतर समय के कलनविधि को बनाए रखता है। स्पार्क कोड भी ट्वीट एनएसीएल से अधिक तेज होता है।

यह भी देखें

• जेड नोटेशन
• जावा मॉडलिंग लैंग्वेज

अग्रिम पठन

• 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 (जीपीएल) 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