🎉 ✋🏽 ✨ यूआई के लिए औपचारिक मॉडल सत्यापन विधियों का अनुप्रयोग ⤵️ 🗼 👩🏼‍🏫

नमस्कार, हेब्र! मैं आपके लिए Hillel Wayne के लेख "FORMALLY SPECIFYING UIS" का अनुवाद प्रस्तुत करता हूँ।

लेखक से

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

चेतावनी :

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

औपचारिक UI विशिष्टता

एक अच्छा उपयोगकर्ता इंटरफ़ेस सही सॉफ्टवेयर बनाने के लिए आवश्यक है। और अगर उपयोगकर्ताओं को प्रोग्राम का उपयोग करने में समस्या है, तो वे कुछ गलत करने की संभावना रखते हैं। मैं उपयोगकर्ता इंटरफ़ेस पर काम नहीं करना पसंद करता हूं - मैं खुद को इस से ऊपर नहीं मानता, लेकिन यह "मेरा नहीं" है। दृश्य प्रभाव और इंटरफेस मुझे चिंता का कारण बनाते हैं, और जो लोग इस सब से निपटने में सक्षम हैं वे मुझे पागल सम्मान देते हैं।

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

समस्या

एडमोडो में वापस, मैं हमारे स्नैपशॉट एप्लिकेशन के लिए एक यूजर इंटरफेस पर काम कर रहा था। यह पैसा बनाने का हमारा ~~पहला~~ दूसरा प्रयास था: हमने सभी शिक्षकों को एक निशुल्क कार्यक्रम देकर शुरुआत की, और फिर दान या ऐसा कुछ माँगना शुरू किया। जैसा कि आप देख सकते हैं, तब एडमोडो के पास बहुत अधिक व्यापारिक कौशल नहीं थे। ²

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

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

जब सिस्टम अधिक जटिल होने लगता है, तो हमें सावधान रहने की जरूरत है। इसका मतलब स्पेसिफिकेशन लिखना है। तो हम इसे कैसे निर्दिष्ट कर सकते हैं? मैं देखता हूं कि शिक्षक एप्लिकेशन की एक विशिष्ट स्क्रीन पर हो सकता है और दूसरी स्क्रीन पर जाने के लिए कार्रवाई कर सकता है। यह मुझे इस विचार की ओर ले जाता है कि हम शिक्षक के कार्यों को एक परिमित राज्य मशीन के रूप में मान सकते हैं।

राज्य की मशीनें

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

मॉडल हमारे उपयोगकर्ता इंटरफ़ेस के साथ दो समस्याएं दिखाता है। सबसे पहले, सभी परिमित राज्य मशीनों को एक प्रारंभिक राज्य की आवश्यकता होती है, लेकिन हमारे पास यह नहीं है। जब कोई शिक्षक रिपोर्ट पृष्ठ पर जाता है, तो उसे किस रिपोर्ट को देखना चाहिए? दूसरे, हम यह नहीं दर्शाते हैं कि जब आप उस रिपोर्ट के बटन पर क्लिक करते हैं जो आप पहले से देख रहे हैं तो क्या होता है। यह मिश्रित है, क्योंकि कई व्यवहार हैं:

यदि आप एक सारांश रिपोर्ट में हैं, तो सारांश बटन दिखाई नहीं देता है या कुछ भी नहीं करता है।
यदि आप एक सारांश रिपोर्ट में हैं, तो सारांश बटन रिपोर्ट को रीसेट करता है।

हमने दूसरा विकल्प चुना है। हमारी प्रारंभिक स्थिति "सारांश" रिपोर्ट थी। अद्यतित मॉडल:

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

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

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

हरेल स्टेटस चार्ट

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

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

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

आप ग्राफविज़ में हरल स्टेट चार्ट विकसित कर सकते हैं और हर बार कई कोने, किनारों, और ग्राफिकल ग्राफ़ के प्रसन्नता से भयभीत हो सकते हैं। हम Sketch.systems से बहुत अच्छे उपयोगकर्ता इंटरफ़ेस का उपयोग करेंगे:

Snapshot logout -> Login Page Reports summary -> Summary students -> Students standards -> Standards Summary* Students answer -> Answers Standards Answers close -> Students Login Page login -> Snapshot

_{स्रोत}

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

चार्ट का अध्ययन करते समय, मुझे एक गलती मिली: आप "उत्तर" से सीधे "मानकों" पर जा सकते हैं। यह "उत्तर" को "रिपोर्ट" के बजाय "इनपुट" का सीधा वंशज बनाकर तय किया जा सकता है:

_{स्रोत}

आदर्श रूप से, आरेख पर ऐसी समस्याओं को स्पष्ट रूप से देखना अच्छा होगा, जो मॉडल सत्यापन के कुछ स्वचालन का अर्थ है।

निरीक्षण

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

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

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

 open util/ordering[Time] sig Time { state: one State } abstract sig State {} abstract sig Login extends State {} abstract sig Reports extends Login {} one sig Logout extends State {} one sig Students, Summary, Standards extends Reports {} one sig Answers extends Login {} pred transition[t: Time, start: State, end: State] { t.state in start t.next.state in end } pred logout[t: Time] { transition[t, Login, Logout] } pred login[t: Time] { transition[t, Logout, Summary] } pred students[t: Time] { transition[t, Reports, Students] } pred summary[t: Time] { transition[t, Reports, Summary] } pred standards[t: Time] { transition[t, Reports, Standards] } pred answers[t: Time] { transition[t, Students, Answers] } pred close_answers[t: Time] { transition[t, Answers, Students] } fact Trace { first.state = Summary all t: Time - last | logout[t] or login[t] or students[t] or summary[t] or standards[t] or answers[t] or close_answers[t] }

अब हम अपने मॉडल के गुणों की जांच कर सकते हैं। उदाहरण के लिए, क्या "छात्रों" रिपोर्ट के माध्यम से "उत्तर" रिपोर्ट प्राप्त करना संभव है?

 check {all t: Time | t.state = Answers implies t.prev.state = Students} for 7 // valid

हम एक उदाहरण का अनुकरण भी कर सकते हैं जब कोई व्यक्ति फिर से बाहर निकलता है और लॉग करता है:

 run {some disj t1, t2: Time | logout[t1] and login[t2]} for 7

मिश्र धातु विनिर्देशों की एक विस्तृत श्रृंखला प्रदान करता है। कुछ गुणों के सत्यापन के साथ, उदाहरण के लिए, टुपिओकोव, कठिनाइयां पैदा हो सकती हैं। हालांकि, मैं यह देखने वाला पहला व्यक्ति नहीं हूं कि मिश्र धातु स्टेट डायग्राम के साथ कितनी अच्छी तरह काम करता है। प्रोफेसर नैन्सी डे ने हाल ही में DASH नामक एक मिश्र धातु संस्करण की घोषणा की, जो हरेल डायग्राम के प्रथम श्रेणी के शब्दार्थ को मिश्र धातु में जोड़ता है। आप इसके बारे में यहां पढ़ सकते हैं।

मूल्य

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

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

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

निष्कर्ष

हमने UI के साथ उपयोगकर्ता सहभागिता के औपचारिक विनिर्देश पर चर्चा की। क्या औपचारिक तरीकों से मेरा प्यार यूआई के मेरे डर को दूर कर सकता है? गोश सं। यदि आपने स्केच.सिस्टम के लिंक का अनुसरण किया है, तो आपने संभवतः देखा कि आप जावास्क्रिप्ट में एक प्रोटोटाइप को अपने राज्य आरेख में संलग्न कर सकते हैं। यह जादू है!

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

वैसे, मैं औपचारिक तरीकों पर सलाह देता हूं। अपने मालिक को बताओ!

चेतावनी, मैं अल्फा परीक्षण में से एक था। मेरी प्रतिक्रिया का अधिकांश हिस्सा ऐसा था, "आपको इसे और अधिक जटिल बनाना चाहिए!"। हां, मैं एक बहुत ही अल्फा परीक्षक हूं। ^{[वापसी]}
2017 में, उन्होंने 1 मिलियन प्राप्त किए और 20 मिलियन खो दिए। ^{[वापसी]}
एक परिमित राज्य मशीन एक नियतात्मक परिमित राज्य मशीन के साथ बहुत आम है, जो कंप्यूटर विज्ञान का एक महत्वपूर्ण घटक है। आवेदन के क्षेत्र में मुख्य अंतर: एक नियत परिमित राज्य मशीन का उपयोग "नियमित भाषाओं के सेट जो इसे पहचानता है" द्वारा उचित है, "विनिर्देशन संगति" द्वारा परिमित राज्य मशीन का उपयोग ^{[वापसी]}
मुख्य प्रतियोगी यूएमएल स्टेट डायग्राम है, जो मूल रूप से हरेर स्टेट डायग्राम का प्रतिनिधित्व करता है, जो अपने कोड विनिर्देशों के साथ पूरक है। यह अधिक अभिव्यंजक है, लेकिन विश्लेषण करना मुश्किल है। ^{[वापसी]}
यदि आप मिश्र धातु से परिचित नहीं हैं, तो मैंने इस पर और यहां कई लेख लिखे हैं ।

यूआई के लिए औपचारिक मॉडल सत्यापन विधियों का अनुप्रयोग