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

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

Latest revision as of 06:48, 19 October 2023

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

मूल रूप से, स्पार्क लैंग्वेज के तीन संस्करण क्रमशः स्पार्क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 पर आधारित बर्नार्ड कैरे और ट्रेवर जेनिंग्स द्वारा साउथेम्प्टन विश्वविद्यालय ब्रिटेन के रक्षा मंत्रालय (यूनाइटेड किंगडम) के प्रायोजन के साथ में तैयार किया गया था। पास्कल प्रोग्रामिंग लैंग्वेज के सबसेट के संदर्भ में स्पार्क नाम स्पाडे एडीए करनेल से लिया गया था।^[1]

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

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

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

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

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

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

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

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

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

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

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

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

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

यह भी देखें

संदर्भ

↑ "चिंगारी - कुदाल एडा कर्नेल (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.

बाहरी संबंध

[spark_lang_ref_manual-1] "चिंगारी - कुदाल एडा कर्नेल (RavenSPARK सहित)". AdaCore. Retrieved 30 June 2021.

[2] Handy, Alex (24 August 2010). "एडा-व्युत्पन्न स्केन क्रिप्टो स्पार्क दिखाता है". SD Times. BZ Media LLC. Retrieved 31 August 2010.

[3] "एंबेडेड सॉफ़्टवेयर की सुरक्षा और सुरक्षा के भविष्य को सुरक्षित करना". 8 January 2020.

[4] "स्पार्कनासीएल". GitHub. 8 October 2021.

[1]

[2]

[3]

[4]

@@ Line 1: / Line 1: @@
 {{Short description|Programming language}}
-{{About|प्रोग्रामिंग लैंग्वेज |क्लस्टर कंप्यूटिंग फ्रेमवर्क के लिए जो स्कैला प्रोग्रामिंग लैंग्वेज, जावा प्रोग्रामिंग लैंग्वेज और पायथन प्रोग्रामिंग पर चल सकता है। |जैसे अपाचे स्पार्क में देख सकते है।}}
 {{Use dmy dates|date=April 2022}}
-{{multiple issues|
-{{More footnotes needed|date=September 2010}}
-{{third-party|date=May 2014}}
-}}
 {{Infobox programming language
-| name = SPARK
+| name = स्पार्क
 | logo = [[File:Sparkada.jpg|250px]]
-| paradigm = [[Multi-paradigm programming language|Multi-paradigm]]
+| paradigm = [[बहु-प्रतिमान प्रोग्रामिंग भाषा|बहु-प्रतिमान]]
-| developer = [[Altran]] and [[AdaCore]]
+| developer = [[अल्ट्रान]] और [[एडाकोर]]
-| latest_release_version = Community 2021
+| latest_release_version = समुदाय 2021
 | latest_release_date = {{Start date and age|2021|06|01}}
-| typing = [[static typing|static]], [[Strongly typed programming language|strong]], [[type safety|safe]], [[nominative type system|nominative]]
+| typing = [[स्थैतिक टाइपिंग|स्थैतिक]], [[मज़बूती से टाइप की गई प्रोग्रामिंग भाषा|मजबूत]], [[प्रकार की सुरक्षा|सुरक्षित]], [[नाममात्र प्रकार की प्रणाली|नामकारक]]
-| implementations = SPARK Pro, SPARK GPL Edition, SPARK Community
+| implementations = स्पार्क प्रो, स्पार्क जीपीएल संस्करण, स्पार्क समुदाय
 | dialects =
-| influenced_by = [[Ada (programming language)|Ada]], [[Eiffel (programming language)|Eiffel]]
+| influenced_by = [[एडा (प्रोग्रामिंग लैंग्वेज)|एडा]], [[एफिल (प्रोग्रामिंग लैंग्वेज)|एफिल]]
 | influenced =
-| operating_system = [[Cross-platform]]: [[Linux]], [[Microsoft Windows]], [[Mac OS X]]
+| operating_system = [[क्रॉस-प्लेटफ़ॉर्म]]: [[लिनक्स]], [[माइक्रोसॉफ्ट विंडोज़]], [[मैक ओएस एक्स]]
-| license = [[GNU General Public License|GPLv3]]
+| license = [[जीएनयू जनरल पब्लिक लाइसेंस|जीपीएलवी3]]
 | website = [http://www.adacore.com/about-spark About SPARK]
 | file_ext =
 }}
-स्पार्क एडा ([[ प्रोग्रामिंग भाषा ]]) प्रोग्रामिंग लैंग्वेज पर आधारित प्रोग्रामिंग लैंग्वेज [[कंप्यूटर]] प्रोग्रामिंग लैंग्वेज का एक औपचारिक शब्दार्थ है, जिसका उद्देश्य सिस्टम में उपयोग किए जाने वाले [[उच्च अखंडता सॉफ्टवेयर]] के विकास के लिए है जहां पूर्वानुमान योग्य और अत्यधिक विश्वसनीय संचालन आवश्यक है। यह उन अनुप्रयोगों के विकास की सुविधा प्रदान करता है जो सुरक्षा, सुरक्षा या व्यावसायिक अखंडता की मांग करते हैं।
+स्पार्क एडीए ([[ प्रोग्रामिंग भाषा |प्रोग्रामिंग लैंग्वेज]]) प्रोग्रामिंग लैंग्वेज पर आधारित एक औपचारिक रूप से परिभाषित कंप्यूटर प्रोग्रामिंग लैंग्वेज होती है, जिसका उद्देश्य प्रणालियों में उपयोग किए जाने वाले [[उच्च अखंडता सॉफ्टवेयर|उच्च इंटेग्रिटी सॉफ्टवेयर]] के विकास के लिए उद्धिष्ट होती है, जहां अपेक्षा के योग्य और अत्यधिक विश्वसनीय संचालन आवश्यक होता है। यह सुरक्षा तथा व्यावसायिक सत्यनिष्ठा की मांग करने वाले अनुप्रयोगों के विकास की सुविधा प्रदान करते है।
-मूल रूप से, क्रमशः Ada 83, Ada 95 और Ada 2005 पर आधारित SPARK भाषा (SPARK83, SPARK95, SPARK2005) के तीन संस्करण थे।
+मूल रूप से, स्पार्क लैंग्वेज के तीन संस्करण क्रमशः स्पार्क83, स्पार्क95, स्पार्क2005 थे जो क्रमशः एडीए 83, एडीए 95, एडीए 2005 पर आधारित थे।
-स्पार्क भाषा का चौथा संस्करण, स्पार्क 2014, एडा 2012 पर आधारित, 30 अप्रैल 2014 को जारी किया गया था। स्पार्क 2014 भाषा और सहायक [[सॉफ्टवेयर सत्यापन]] उपकरणों का एक पूर्ण पुन: डिजाइन है।
+एडीए 2012 पर आधारित स्पार्क लैंग्वेज, स्पार्क 2014 का चौथा संस्करण 30 अप्रैल 2014 को रिलीज़ किया गया। स्पार्क 2014 लैंग्वेज का एक पूर्ण पुन: डिजाइन और [[सॉफ्टवेयर सत्यापन]] उपकरण का समर्थन है।
-स्पार्क भाषा में एडा भाषा का एक अच्छी तरह से परिभाषित उपसमुच्चय होता है जो स्थिर और गतिशील सत्यापन दोनों के लिए उपयुक्त रूप में घटकों के विनिर्देश का वर्णन करने के लिए [[अनुबंध (सॉफ्टवेयर)]] का उपयोग करता है।
+स्पार्क लैंग्वेज में एडीए लैंग्वेज का एक अच्छी तरह से परिभाषित उपसमुच्चय होता है, जो स्थिर और गतिशील सत्यापन दोनों के लिए उपयुक्त रूप में घटकों के विनिर्देश का वर्णन करने के लिए [[अनुबंध (सॉफ्टवेयर)]] का उपयोग करता है।
-SPARK83/95/2005 में, अनुबंधों को Ada टिप्पणियों में एन्कोड किया गया है और इसलिए किसी भी मानक Ada संकलक द्वारा अनदेखा किया जाता है, लेकिन SPARK परीक्षक और उससे जुड़े उपकरणों द्वारा संसाधित किया जाता है।
+स्पार्क83/स्पार्क95/स्पार्क2005 में, अनुबंधों को एडीए टिप्पणियों में एन्कोड किया गया है और इसलिए किसी भी मानक एडीए कम्पाइलर द्वारा अनदेखा किया जाता है, लेकिन स्पार्क परीक्षक और उससे जुड़े उपकरणों द्वारा संसाधित किया जाता है।
-इसके विपरीत, स्पार्क 2014, अनुबंधों को व्यक्त करने के लिए एडा 2012 के बिल्ट-इन आस्पेक्ट सिंटैक्स का उपयोग करता है, उन्हें भाषा के मूल में लाता है। स्पार्क 2014 (जीएनएटीप्रोव) के लिए मुख्य टूल जीएनएटी|जीएनएटी/जीसीसी इंफ्रास्ट्रक्चर पर आधारित है, और जीएनएटी एडा 2012 फ्रंट-एंड की लगभग संपूर्णता का पुन: उपयोग करता है।
+इसके विपरीत, स्पार्क 2014, अनुबंधों को व्यक्त करने के लिए एडीए 2012 के बिल्ट-इन एस्पेक्ट सिंटैक्स का उपयोग करता है, उन्हें लैंग्वेज के मूल रूप में लाता है। स्पार्क 2014 जीएनएटीप्रोव के लिए मुख्य टूल जीएनएटी|जीएनएटी/जीसीसी इंफ्रास्ट्रक्चर पर आधारित होता है और जीएनएटी एडीए 2012 फ्रंट-एंड की लगभग संपूर्णता का पुन: उपयोग करता है।
-== तकनीकी सिंहावलोकन ==
+== प्रोद्योगिकीय संक्षिप्त विवरण ==
-स्पार्क अपनी सभी संभावित अस्पष्टताओं और असुरक्षित निर्माणों को खत्म करने की कोशिश करते हुए एडा की ताकत का उपयोग करता है। स्पार्क प्रोग्राम डिज़ाइन द्वारा स्पष्ट होने के लिए हैं, और उनके व्यवहार को एडा [[ संकलक ]] की पसंद से अप्रभावित होना आवश्यक है। इन लक्ष्यों को आंशिक रूप से एडा की कुछ अधिक समस्याग्रस्त विशेषताओं (जैसे अप्रतिबंधित [[कार्य समानता]]) को छोड़ कर और आंशिक रूप से उन अनुबंधों को प्रारंभ  करके प्राप्त किया जाता है जो प्रोग्राम के कुछ घटकों के लिए एप्लिकेशन डिज़ाइनर के इरादों और आवश्यकताओं को कूटबद्ध करते हैं।
+स्पार्क एडीए की क्षमताओं का उपयोग करते हुए अपनी सभी संभावित अस्पष्टताओं और असुरक्षित निर्माणों को खत्म करने का प्रयास करता है। स्पार्क प्रोग्राम डिज़ाइन द्वारा स्पष्ट होता है और एडीए [[कंपाइलर]] के चयन से उनके व्यवहार को अप्रभावित रखना आवश्यक होता है। इन लक्ष्यों को आंशिक रूप से एडीए की कुछ अधिक समस्याग्रस्त विशेषताओं जैसे अप्रतिबंधित [[कार्य समानता]] को छोड़ कर और आंशिक रूप से उन अनुबंधों को प्रारंभ करके प्राप्त किया जाता है जो प्रोग्राम के कुछ घटकों के लिए अनुप्रयोग डिज़ाइनर के प्रयोजन और आवश्यकताओं को कूटबद्ध या एन्कोड करते हैं।
-इन दृष्टिकोणों का संयोजन स्पार्क को अपने डिजाइन उद्देश्यों को पूरा करने की अनुमति देता है, जो हैं:
+इन दृष्टिकोणों का संयोजन स्पार्क को अपने डिजाइन उद्देश्यों को पूरा करने की अनुमति देता है, जो इस प्रकार है
 * तार्किक सु[[दृढ़ता]]
 * कठोर औपचारिक परिभाषा
@@ Line 45: / Line 41: @@
 * सुरक्षा
 * [[अभिव्यंजक शक्ति (कंप्यूटर विज्ञान)]]
-* [[सत्यापन और सत्यापन]]
+* [[सत्यापन और सत्यापन|सत्यापनीयता]]
-* सीमित संसाधन (अंतरिक्ष और समय) आवश्यकताएँ।
+* सीमित संसाधन क्षेत्र और समय की आवश्यकताओ के रूप में होती है।
-* न्यूनतम रनटाइम सिस्टम आवश्यकताएँ
+* न्यूनतम रनटाइम प्रणाली आवश्यकताओ के रूप में होती है।
 == अनुबंध उदाहरण ==
 <!-- this is a how-to .. delete? -->
-नीचे एडीए सबप्रोग्राम विनिर्देश पर विचार करें:
+नीचे एडीए सबप्रोग्राम विनिर्देश पर विचार करते है, जो इस प्रकार है
- प्रक्रिया वृद्धि (एक्स: बाहर काउंटर_टाइप में);
-शुद्ध एडा में यह चर को बढ़ा सकता है <code>X</code> एक या एक हजार से; या यह कुछ वैश्विक काउंटर सेट कर सकता है <code>X</code> और काउंटर का मूल मान वापस करें <code>X</code>; या यह बिल्कुल कुछ नहीं कर सकता है <code>X</code> बिलकुल।
-स्पार्क 2014 के साथ, एक उपप्रोग्राम वास्तव में क्या करता है, इसके बारे में अतिरिक्त जानकारी प्रदान करने के लिए अनुबंध को कोड में जोड़ा जाता है। उदाहरण के लिए, हम उपरोक्त विनिर्देश को कहने के लिए बदल सकते हैं:
- प्रक्रिया वृद्धि (एक्स: बाहर काउंटर_टाइप में)
-   वैश्विक => अशक्त के साथ,
-        निर्भर करता है => (एक्स => एक्स);
-यह निर्दिष्ट करता है कि <code>Increment</code> प्रक्रिया किसी भी वैश्विक चर का उपयोग नहीं करती (न तो अपडेट करती है और न ही पढ़ती है) और वह एकमात्र डेटा आइटम है जिसका उपयोग नए मूल्य की गणना में किया जाता है <code>X</code> है <code>X</code> अपने आप।
-वैकल्पिक रूप से, डिजाइनर निर्दिष्ट कर सकता है:
+ '''procedure''' Increment (X : '''in out''' Counter_Type);
- प्रक्रिया वृद्धि (एक्स: बाहर काउंटर_टाइप में)
+शुद्ध एडीए में यह चर <code>X</code> है को एक या एक हजार से बढ़ा सकता है या यह कुछ वैश्विक काउंटर सेट <code>X</code> के लिए और <code>X</code> में काउंटर के मूल मान को वापस कर सकते हैं, यह <code>X</code> के साथ बिल्कुल कुछ भी नहीं कर सकता है।
-   वैश्विक => (In_Out => गणना) के साथ,
-        निर्भर करता है => (गणना => (गणना, एक्स),
-                    एक्स => अशक्त);
-यह निर्दिष्ट करता है <code>Increment</code> वैश्विक चर का उपयोग करेगा <code>Count</code> के रूप में एक ही पैकेज में <code>Increment</code>, कि निर्यात मूल्य <code>Count</code> के आयातित मूल्यों पर निर्भर करता है <code>Count</code> और <code>X</code>, और यह कि निर्यात मूल्य <code>X</code> किसी भी चर पर बिल्कुल भी निर्भर नहीं करता है और यह केवल स्थिर डेटा से ही प्राप्त होगा।
+स्पार्क 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),
-        पोस्ट => एक्स = एक्स'ओल्ड + 1;
+       Pre     => X < Counter_Type'Last,
+       Post    => X = X'Old + 1;
-यह, अब, न केवल यह निर्दिष्ट करता है <code>X</code> अकेले स्वयं से ही प्राप्त होता है, लेकिन उससे पहले भी <code>Increment</code> कहा जाता है <code>X</code> अपने प्रकार के अंतिम संभावित मूल्य से कड़ाई से कम होना चाहिए (यह सुनिश्चित करने के लिए कि परिणाम कभी भी अतिप्रवाह नहीं होगा) और उसके बाद <code>X</code> के प्रारंभिक मूल्य के बराबर होगा <code>X</code> मैं भी सहमत हूं।
+</syntaxhighlight>यह अब न केवल यह निर्दिष्ट करता है कि <code>X</code> केवल स्वयं से ही प्राप्त होता है, लेकिन उससे पहले भी इन्क्रीमेंट को <code>X</code> कहा जाता है, जो अपने प्रकार के अंतिम संभावित मूल्य से कम होना चाहिए, ताकि यह सुनिश्चित करने के लिए कि परिणाम कभी भी अतिप्रवाह नहीं होता है और उसके बाद में <code>X</code> के बराबर होगा जो <code>X</code> प्लस वन के प्रारंभिक मूल्य के बराबर होता है।
 == सत्यापन की शर्तें ==
-GNATprove [[सत्यापन स्थिति जनरेटर]] या वीसी का एक सेट भी उत्पन्न कर सकता है। इन शर्तों का उपयोग यह स्थापित करने के लिए किया जाता है कि क्या कुछ गुण किसी दिए गए सबप्रोग्राम के लिए हैं। कम से कम, GNATprove कुलपतियों को यह स्थापित करने के लिए उत्पन्न करेगा कि सभी रन-टाइम त्रुटियाँ एक सबप्रोग्राम के भीतर नहीं हो सकती हैं, जैसे:
+जीएनएटी प्रोव [[सत्यापन स्थिति जनरेटर]] या वीसी का एक सेट उत्पन्न कर सकता है। इन शर्तों का उपयोग यह स्थापित करने के लिए किया जाता है कि क्या कुछ गुण किसी दिए गए सबप्रोग्राम के लिए हैं। कम से कम, जीएनएटी प्रोव वीसी को यह स्थापित करने के लिए उत्पन्न करता है कि सभी रन-टाइम त्रुटियाँ एक सबप्रोग्राम के भीतर नहीं हो सकती हैं, जैसे कि,
-* सरणी सूचकांक सीमा से बाहर
+* सरणी सूचकांक सीमा से बाहर होती है
-* टाइप रेंज उल्लंघन
+* टाइप रेंज उल्लंघन के रूप में होती है
-* शून्य से विभाजन
+* शून्य से विभाजन होता है
-* संख्यात्मक अतिप्रवाह।
+* संख्यात्मक अतिप्रवाह के रूप में होती है।
-यदि कोई पोस्टकंडिशन या कोई अन्य अभिकथन एक सबप्रोग्राम में जोड़ा जाता है, तो GNATprove वीसी भी उत्पन्न करेगा जिसके लिए उपयोगकर्ता को यह दिखाने की आवश्यकता होती है कि ये गुण सबप्रोग्राम के माध्यम से सभी संभावित पथों के लिए हैं।
+यदि कोई पोस्टकंडिशन या कोई अन्य अभिकथन एक सबप्रोग्राम में जोड़ा जाता है, तो जीएनएटी प्रोव वीसी उत्पन्न करता है, जिसके लिए उपयोगकर्ता को यह दिखाने की आवश्यकता होती है कि ये गुण सबप्रोग्राम के माध्यम से सभी संभावित पथों के लिए होते है।
-हुड के अनुसार , GNATprove वीसी को डिस्चार्ज करने के लिए Why3 इंटरमीडिएट लैंग्वेज और VC जेनरेटर, और [[CVC4]], [[Z3 प्रमेय प्रस्तावक]] और [[Alt-Ergo]] प्रमेय का उपयोग करता है। Why3 टूलसेट के अन्य घटकों के माध्यम से अन्य प्रोवर (इंटरैक्टिव प्रूफ चेकर्स सहित) का उपयोग भी संभव है।
+हुड के अनुसार, जीएनएटी प्रोव वीसी को डिस्चार्ज करने के लिए वाई3 इंटरमीडिएट लैंग्वेज और वीसी जेनरेटर और [[सीवीसी4, जेड3]] और [[ऑल्ट एर्गो]] प्रमेय का उपयोग करता है। वाई3 टूलसेट के अन्य घटकों के माध्यम से इंटरैक्टिव प्रूफ चेकर्स सहित अन्य प्रोवर का उपयोग भी संभव होता है।
 == इतिहास ==
-स्पार्क का पहला संस्करण (एडा 83 पर आधारित) बर्नार्ड कैरे और ट्रेवर जेनिंग्स द्वारा [[साउथेम्प्टन विश्वविद्यालय]] (ब्रिटेन के [[रक्षा मंत्रालय (यूनाइटेड किंगडम)]] के प्रायोजन के साथ) में तैयार किया गया था। SPARK नाम SPADE Ada Kernel से लिया गया था, [[पास्कल प्रोग्रामिंग भाषा]] के SPADE उपसमुच्चय के संदर्भ में।<ref name=spark_lang_ref_manual>{{cite web |url=https://docs.adacore.com/sparkdocs-docs/SPARK_LRM.htm |title=चिंगारी - कुदाल एडा कर्नेल (RavenSPARK सहित)|publisher=AdaCore |access-date=2021-06-30}}</ref>
+स्पार्क का पहला संस्करण एडीए 83 पर आधारित बर्नार्ड कैरे और ट्रेवर जेनिंग्स द्वारा [[साउथेम्प्टन विश्वविद्यालय]] ब्रिटेन के [[रक्षा मंत्रालय (यूनाइटेड किंगडम)]] के प्रायोजन के साथ में तैयार किया गया था। [[पास्कल प्रोग्रामिंग भाषा|पास्कल प्रोग्रामिंग]] लैंग्वेज के सबसेट के संदर्भ में स्पार्क नाम स्पाडे एडीए करनेल से लिया गया था।<ref name=spark_lang_ref_manual>{{cite web |url=https://docs.adacore.com/sparkdocs-docs/SPARK_LRM.htm |title=चिंगारी - कुदाल एडा कर्नेल (RavenSPARK सहित)|publisher=AdaCore |access-date=2021-06-30}}</ref>
-बाद में प्रोग्राम वैलिडेशन लिमिटेड द्वारा और फिर प्रैक्सिस क्रिटिकल सिस्टम्स लिमिटेड द्वारा भाषा को उत्तरोत्तर विस्तारित और परिष्कृत किया गया। 2004 में, प्रैक्सिस क्रिटिकल सिस्टम्स लिमिटेड ने अपना नाम बदलकर प्रैक्सिस हाई इंटीग्रिटी सिस्टम्स लिमिटेड कर दिया। जनवरी 2010 में, कंपनी [[ अल्ट्रॉन अधिनियम ]] बन गई।
+बाद में प्रोग्राम वैलिडेशन लिमिटेड द्वारा और फिर प्रैक्सिस क्रिटिकल प्रणाली लिमिटेड द्वारा लैंग्वेज को उत्तरोत्तर विस्तारित और परिष्कृत किया गया। 2004 में, प्रैक्सिस क्रिटिकल प्रणाली लिमिटेड ने अपना नाम बदलकर प्रैक्सिस हाई इंटीग्रिटी प्रणाली लिमिटेड कर दिया। जनवरी 2010 में, कंपनी [[ अल्ट्रॉन अधिनियम |अल्ट्रॉन अधिनियम]] बन गई।
-की शुरुआत में, प्रैक्सिस ने AdaCore के साथ साझेदारी की, और GPL की शर्तों के अनुसार  स्पार्क प्रो जारी किया। इसके बाद जून 2009 में स्पार्क GPL संस्करण 2009 आया, जिसका लक्ष्य [[FOSS]] और अकादमिक समुदाय था।
+के प्रारम्भ में, प्रैक्सिस ने एडीए कोर के साथ साझेदारी की और जीपीएल की शर्तों के अनुसार स्पार्क प्रो जारी किया। इसके बाद जून 2009 में स्पार्क जीपीएल संस्करण 2009 में आया, जिसका लक्ष्य एफओएसएस और अकादमिक कम्युनिटीज के रूप में उपयोग में लाया गया था ।
-जून 2010 में, अल्ट्रान-प्रैक्सिस ने घोषणा की कि यूएस लूनर प्रोजेक्ट [[क्यूबसैट]] के सॉफ़्टवेयर में स्पार्क प्रोग्रामिंग भाषा का उपयोग किया जाएगा, जिसके 2015 में पूरा होने की उम्मीद है।
+जून 2010 में, अल्ट्रान-प्रैक्सिस ने घोषणा की कि यूएस लूनर प्रोजेक्ट [[क्यूबसैट]] के सॉफ़्टवेयर में स्पार्क प्रोग्रामिंग लैंग्वेज का उपयोग किया जाएगा, जिसके 2015 में पूरा होने की उम्मीद है।
-जनवरी 2013 में, अल्ट्रान-प्रैक्सिस ने अपना नाम बदलकर अल्ट्रान कर लिया, जो अप्रैल 2021 में [[कैंपजेमिनी इंजीनियरिंग]] ([[ इसे पकड़ लो ]] के साथ अल्ट्रान के विलय के बाद) बन गया।
+जनवरी 2013 में अल्ट्रान-प्रैक्सिस ने अपना नाम बदलकर अल्ट्रान कर लिया, जो अप्रैल 2021 में कैपजेमिनी के साथ अल्ट्रान के विलय के बाद [[कैपजेमिनी इंजीनियरिंग]] बन गया।
-स्पार्क 2014 की पहली प्रो रिलीज़ की घोषणा 30 अप्रैल, 2014 को की गई थी, और [[दाँत साफ करने का धागा]] और अकादमिक समुदायों के उद्देश्य से स्पार्क 2014 जीपीएल संस्करण के तुरंत बाद इसका अनुसरण किया गया।
+स्पार्क 2014 की पहली प्रो रिलीज़ की घोषणा 30 अप्रैल 2014 को की गई थी, [[फ्लॉस]] और अकादमिक समुदायों के उद्देश्य से स्पार्क 2014 जीपीएल संस्करण के तुरंत बाद इसका अनुसरण किया गया।
 == औद्योगिक अनुप्रयोग ==
 === सुरक्षा संबंधी प्रणालियाँ ===
-SPARK का उपयोग कई हाई प्रोफाइल सुरक्षा-महत्वपूर्ण प्रणालियों में किया गया है, जिसमें वाणिज्यिक विमानन ([[रोल्स-रॉयस ट्रेंट]] श्रृंखला जेट इंजन, ARINC ACAMS सिस्टम, [[लॉकहीड मार्टिन C-130J सुपर हरक्यूलिस]]), सैन्य विमानन ([[यूरोफाइटर टाइफून]], [[हैरियर GR9]], Aermacchi) सम्मलित  हैं। M-346), वायु-यातायात प्रबंधन (UK [[NATS iFACTS]] सिस्टम), रेल (अनेक सिग्नलिंग अनुप्रयोग), चिकित्सा (लाइफफ्लो [[वेंट्रिकुलर असिस्ट डिवाइस]]), और अंतरिक्ष अनुप्रयोग ([[वर्मोंट लूनर क्यूबसैट]])।{{citation needed|date=May 2022}}
+स्पार्क का उपयोग कई हाई प्रोफाइल सुरक्षा महत्वपूर्ण प्रणालियों में किया गया है, जिसमें वाणिज्यिक उड्‌डयन, [[रोल्स-रॉयस ट्रेंट]] श्रृंखला जेट इंजन, एआरआईएनसी एसीएएमएस प्रणाली, [[लॉकहीड मार्टिन C-130J सुपर हरक्यूलिस|लॉकहीड मार्टिन सी-130जे सुपर हरक्यूलिस]], सैन्य विमानन [[यूरोफाइटर टाइफून]], [[हैरियर GR9]], एयरमाची एम346 के रूप में सम्मलित हैं। वायु-यातायात प्रबंधन [[यूके एनएटीएस आईफैक्ट्स]] प्रणाली, रेल कई सिग्नलिंग अनुप्रयोग, चिकित्सा लाइफफ्लो [[वेंट्रिकुलर असिस्ट डिवाइस|वेंट्रिकुलर असिस्ट उपकरण]] और अंतरिक्ष अनुप्रयोग [[वर्मोंट लूनर क्यूबसैट]] के रूप में सम्मलित हैं।
 === सुरक्षा संबंधी प्रणालियाँ ===
-स्पार्क का उपयोग सुरक्षित सिस्टम डेवलपमेंट में भी किया गया है। उपयोगकर्ताओं में सम्मलित  हैं [[रॉकवेल कॉलिन्स]] (टर्नस्टाइल और सिक्योरवन क्रॉस-डोमेन समाधान), मूल [[ अनेक ]] सीए का विकास, एनएसए [[टोकनर]] डिमॉन्स्ट्रेटर, सेक्यूनेट मल्टी-लेवल वर्कस्टेशन, म्यूएन सेपरेशन कर्नेल और [[जीनोड]] ब्लॉक-डिवाइस एनक्रिप्टर।
+स्पार्क का उपयोग सुरक्षित प्रणाली डेवलपमेंट में किया जाता है। उपयोगकर्ताओं में [[रॉकवेल कॉलिन्स]] टर्नस्टाइल और सिक्योरवन क्रॉस डोमेन समाधान के रूप में सम्मलित हैं। जो [[मूल]] मल्टीस सीए एनएसए [[टोकनर]] डिमॉन्स्ट्रेटर सेक्युनेट मल्टी लेवल वर्कस्टेशन म्यूएन सेपरेशन कर्नेल और [[जेनोड]] ब्लॉक उपकरण एनक्रिप्टर का विकास करते हैं।
+अगस्त 2010 में, अल्ट्रान प्रैक्सिस के प्रमुख इंजीनियर रॉड चैपमैन ने स्पार्क में [[Sha-3|एसएचए-3]] के उम्मीदवारों में से एक स्केन हैश फंक्शन को लागू किया। स्पार्क और सी कार्यान्वयन के प्रदर्शन की तुलना में और सावधानीपूर्वक अनुकूलन के बाद वह स्पार्क संस्करण को सी की तुलना में केवल 5 से 10% धीमी गति से चलाने में कामयाब रहा। और प्रदर्शन में सी से मेल खाने वाले स्पार्क कोड के साथ अंतर को बंद कर दिया।<ref>{{cite news|url=http://www.sdtimes.com/link/34579|title=एडा-व्युत्पन्न स्केन क्रिप्टो स्पार्क दिखाता है|last=Handy|first=Alex|date=August 24, 2010|work=[[SD Times]]|publisher=BZ Media LLC|accessdate=2010-08-31}}</ref>
+सुरक्षा-महत्वपूर्ण फर्मवेयर के कार्यान्वयन के लिए एनवीआईडीआईए ने स्पार्क को भी अपनाया है।<ref>{{Cite web|url=https://www.slideshare.net/AdaCore/securing-the-future-of-safety-and-security-of-embedded-software|title = एंबेडेड सॉफ़्टवेयर की सुरक्षा और सुरक्षा के भविष्य को सुरक्षित करना|date = 8 January 2020}}</ref>
-अगस्त 2010 में, अल्ट्रान प्रैक्सिस के प्रमुख अभियंता रॉड चैपमैन ने SPARK में [[Sha-3]]|SHA-3 के उम्मीदवारों में से एक स्केन (हैश फंक्शन) को लागू किया। स्पार्क और सी कार्यान्वयन के प्रदर्शन की तुलना में और सावधानीपूर्वक अनुकूलन के बाद, वह स्पार्क संस्करण को सी की तुलना में केवल 5 से 10% धीमी गति से चलाने में कामयाब रहा। ) प्रदर्शन में C से मेल खाने वाले स्पार्क कोड के साथ अंतर को बंद कर दिया।<ref>{{cite news|url=http://www.sdtimes.com/link/34579|title=एडा-व्युत्पन्न स्केन क्रिप्टो स्पार्क दिखाता है|last=Handy|first=Alex|date=August 24, 2010|work=[[SD Times]]|publisher=BZ Media LLC|accessdate=2010-08-31}}</ref>
+में, रॉड चैपमैन ने स्पार्क 2014 में [[TweetNaCl|ट्वीट एनएसीएल]] क्रिप्टोग्राफ़िक लाइब्रेरी को फिर से लागू किया।<ref>{{Cite web|url=https://github.com/rod-chapman/स्पार्कनासीएल|title = स्पार्कनासीएल| website=[[GitHub]] |date = 8 October 2021}}</ref> लाइब्रेरी के स्पार्क संस्करण में टाइप-सेफ्टी, मेमोरी-सेफ्टी और कुछ शुद्धता गुणों का एक पूर्ण ऑटो-एक्टिव प्रूफ है और निरंतर समय के कलनविधि को बनाए रखता है। स्पार्क कोड भी ट्वीट एनएसीएल से अधिक तेज होता है।
-सुरक्षा-महत्वपूर्ण फर्मवेयर के कार्यान्वयन के लिए NVIDIA ने स्पार्क को भी अपनाया है।<ref>{{Cite web|url=https://www.slideshare.net/AdaCore/securing-the-future-of-safety-and-security-of-embedded-software|title = एंबेडेड सॉफ़्टवेयर की सुरक्षा और सुरक्षा के भविष्य को सुरक्षित करना|date = 8 January 2020}}</ref>
-में, रॉड चैपमैन ने स्पार्क 2014 में [[TweetNaCl]] क्रिप्टोग्राफ़िक लाइब्रेरी को फिर से लागू किया।<ref>{{Cite web|url=https://github.com/rod-chapman/स्पार्कनासीएल|title = स्पार्कनासीएल| website=[[GitHub]] |date = 8 October 2021}}</ref> लाइब्रेरी के स्पार्क संस्करण में टाइप-सेफ्टी, मेमोरी-सेफ्टी और कुछ शुद्धता गुणों का एक पूर्ण ऑटो-एक्टिव प्रूफ है, और निरंतर-समय के एल्गोरिदम को बनाए रखता है। स्पार्क कोड भी TweetNaCl से अधिक  तेज है।
 == यह भी देखें ==
 {{Portal|Free and open-source software}}
-* [[जेड अंकन]]
+* [[जेड अंकन|जेड नोटेशन]]
-* [[जावा मॉडलिंग भाषा]]
+* [[जावा मॉडलिंग भाषा|जावा मॉडलिंग लैंग्वेज]]
 == संदर्भ ==
@@ Line 165: / Line 157: @@
 ==बाहरी संबंध==
-* [http://www.spark-2014.org/ SPARK 2014 community site]
+* [http://www.spark-2014.org/ स्पार्क 2014 community site]
-* [http://www.adacore.com/sparkpro/ SPARK Pro website]
+* [http://www.adacore.com/sparkpro/ स्पार्क Pro website]
-* [http://libre.adacore.com/ SPARK Libre (GPL) Edition website]
+* [http://libre.adacore.com/ स्पार्क Libre (जीपीएल) Edition website]
 * [http://www.altran.com/ Altran]
 * [http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf Correctness by Construction: A Manifesto for High-Integrity Software] {{Webarchive|url=https://web.archive.org/web/20121030153055/http://www.crosstalkonline.org/storage/issue-archives/2005/200512/200512-Croxford.pdf |date=30 October 2012 }}
@@ Line 179: / Line 171: @@
 {{Authority control}}
-{{DEFAULTSORT:Spark (Programming Language)}}[[Category: एडा (प्रोग्रामिंग भाषा)]] [[Category: एडीए प्रोग्रामिंग भाषा परिवार]] [[Category: अल्गोल प्रोग्रामिंग भाषा परिवार]] [[Category: समवर्ती प्रोग्रामिंग भाषाएँ]] [[Category: औपचारिक विनिर्देश भाषाएँ]] [[Category: उच्च अखंडता प्रोग्रामिंग भाषा]] [[Category: यूनाइटेड किंगडम में कंप्यूटिंग का इतिहास]] [[Category: प्रक्रियात्मक प्रोग्रामिंग भाषाएँ]] [[Category: 20वीं सदी में बनाई गई प्रोग्रामिंग लैंग्वेज]] [[Category: हैम्पशायर में विज्ञान और प्रौद्योगिकी]] [[Category: वैधानिक रूप से टाइप की गई प्रोग्रामिंग भाषाएँ]] [[Category: सिस्टम प्रोग्रामिंग भाषाएं]] [[Category: साउथेम्प्टन विश्वविद्यालय]]
+{{DEFAULTSORT:Spark (Programming Language)}}
-[[Category: Machine Translated Page]]
+[[Category:20वीं सदी में बनाई गई प्रोग्रामिंग लैंग्वेज|Spark (Programming Language)]]
-[[Category:Created On 02/03/2023]]
+[[Category:Articles with invalid date parameter in template|Spark (Programming Language)]]
+[[Category:Created On 02/03/2023|Spark (Programming Language)]]
+[[Category:Machine Translated Page|Spark (Programming Language)]]
+[[Category:Pages with broken file links|Spark (Programming Language)]]
+[[Category:Pages with empty portal template|Spark (Programming Language)]]
+[[Category:Pages with script errors|Spark (Programming Language)]]
+[[Category:Portal templates with redlinked portals|Spark (Programming Language)]]
+[[Category:Short description with empty Wikidata description|Spark (Programming Language)]]
+[[Category:Template documentation pages|Short description/doc]]
+[[Category:Vigyan Ready]]

Anonymous

Search

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

Namespaces

More

Page actions

Latest revision as of 06:48, 19 October 2023

Contents

प्रोद्योगिकीय संक्षिप्त विवरण

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

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

इतिहास

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

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

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

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

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

Latest revision as of 06:48, 19 October 2023

प्रोद्योगिकीय संक्षिप्त विवरण

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

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

इतिहास

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

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

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

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories