असली दुनिया परियोजनाओं में मिश्र धातु का उपयोग करने के अनुभव

Question

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

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

मुझे आपकी परियोजनाओं में मिश्र धातु का उपयोग करने वाले लोगों के वास्तविक वास्तविक अनुभवों के बारे में सुनने में बहुत दिलचस्पी होगी। क्या आपको लगता है कि इससे आपको एक बेहतर डोमेन मॉडल तैयार करने में मदद मिली है? सत्यापन के दौरान आपके डोमेन मॉडल में त्रुटियां मिलीं? क्या आप इसे फिर से इस्तेमाल करेंगे?

Answer 1

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

Answer 2

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

2006 और 2007 में मैंने आंशिक बनाया डब्ल्यू 3 सी एक्सपीआरसी विनिर्देश के तत्कालीन वर्तमान मसौदे के लिए मिश्र धातु मॉडल; जहां तक ​​मैं कह सकता था, कार्यकारी समूह के अधिकांश सदस्यों ने मैंने जो पेपर लिखा था उसे कभी नहीं पढ़ा (http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html पर); उन्होंने कहा, "ओह, हमने पिछले हफ्ते spec के उस हिस्से को बदल दिया है, तो मॉडल क्या कहता है अब प्रासंगिक नहीं है"। लेकिन पेपर ने इस spec के संपादक को मनाने के लिए प्रबंधन किया था कि spec के पहले मसौदे में वर्णित सार 'घटक' स्तर को कम से कम निर्दिष्ट किया गया था और इसे पूरी तरह से निर्दिष्ट या गिरा दिया जाना चाहिए था। उन्होंने इसे छोड़ दिया, (मुझे लगता है) कल्पना की पठनीयता और प्रयोज्यता के लिए अच्छे परिणाम।

2010 में मैंने Alloy model of the XPath 1.0 data model बनाया, जिसने विनिर्देशन में कुछ ग्लिच खोले। सबसे इच्छुक पार्टियों की प्रतिक्रिया (XP3 1.0 spec को बनाए रखने के लिए जिम्मेदार डब्ल्यू 3 सी कार्यकारी समूह समेत) दुर्भाग्यवश, उत्साहजनक नहीं रहा है।

एक अनुसंधान परियोजना के साथ मैं मिश्र धातु का इस्तेमाल किया गया MLCD ओवरलैप कोर्पस, नमूना दस्तावेजों का संग्रह और संबंधित जानकारी हम पैदा कर रहे (अतः के आग्रह पर दबा दिया हाइपरलिंक) मॉडल करने के लिए सम्मिलित हूं; मिश्र धातु मॉडल को कॉर्पस कैटलॉग के लिए हमारे प्रारंभिक डिजाइन में कुछ त्रुटियां मिलीं, इसलिए यह प्रयास के लायक था।

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

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

वह आगे बढ़ता है: "लेकिन यदि आप उन्हें संबोधित नहीं करते हैं, तो छोटे मुद्दों में नॉनट्रिविअल बनने की एक बुरा आदत है।" मेरा अनुभव यह पुष्टि करता है। शुरुआती समस्याओं को दूर करने के लिए बहुत बेहतर है। तो हाँ, मैं फिर से मिश्र धातु का उपयोग करेंगे।

Answer 3

देर से ही सही इस सूत्र को जोड़ने ... Eunsuk कांग हाल ही में मिश्र सुरक्षा कुछ स्टार्ट अप (जैसे अपूर्व के analysis of OAuth और बार्थ एट अल के analysis of browser based security mechanisms CSRF आदि के लिए के रूप में सुरक्षा में मिश्र धातु के कई अनुप्रयोगों के बाद) के लिए वेब एपीआई का विश्लेषण करती है प्रदर्शन करने के लिए आवेदन किया है ; पामेला जेव impressive analysis of Chord पर काम कर रहा है, जो पीयर स्टोरेज सिस्टम के साथ एक सहकर्मी है, और हाल ही में मूल एल्गोरिदम के लिए एक फिक्स लिखा है।