Formal specification
કોમ્પ્યુટર વિજ્ઞાનમાં, ઔપચારિક સ્પષ્ટીકરણો ગાણિતિક રીતે આધારિત તકનીકો છે જેનો હેતુ સિસ્ટમો અને સોફ્ટવેરના અમલીકરણમાં મદદ કરવાનો છે. તેનો ઉપયોગ પ્રણાલીનું વર્ણન કરવા, તેના વર્તનનું વિશ્લેષણ કરવા અને સખત અને અસરકારક તર્ક સાધનો દ્વારા રસના મુખ્ય ગુણધર્મોની ચકાસણી કરીને તેની રચનામાં મદદ કરવા માટે થાય છે. આ સ્પષ્ટીકરણો એ અર્થમાં ઔપચારિક છે કે તેમની પાસે વાક્યરચના છે, તેમના શબ્દાર્થ એક ડોમેનમાં આવે છે, અને તેઓ ઉપયોગી માહિતીને અનુમાન કરવા માટે ઉપયોગમાં લેવા માટે સક્ષમ છે. પ્રેરણા દરેક પસાર થતા દાયકામાં કોમ્પ્યુટર પ્રણાલીઓ વધુને વધુ શક્તિશાળી બની છે અને પરિણામે તે સમાજ માટે વધુ અસરકારક બની છે. આ કારણે, વિશ્વસનીય સોફ્ટવેરની રચના અને અમલીકરણમાં મદદ કરવા માટે વધુ સારી તકનીકોની જરૂર છે. સ્થાપિત ઇજનેરી શાખાઓ ઉત્પાદન ડિઝાઇન બનાવવા અને માન્ય કરવાના પાયા તરીકે ગાણિતિક વિશ્લેષણનો ઉપયોગ કરે છે. એકવાર આગાહી કરવામાં આવી હતી તેમ સોફ્ટવેર એન્જિનિયરિંગની વિશ્વસનીયતામાં આ હાંસલ કરવા માટે ઔપચારિક સ્પષ્ટીકરણો એક એવી રીત છે. પરીક્ષણ જેવી અન્ય પદ્ધતિઓનો ઉપયોગ સામાન્ય રીતે કોડની ગુણવત્તા વધારવા માટે થાય છે. ઉપયોગો આવા સ્પષ્ટીકરણને જોતાં, સિસ્ટમ ડિઝાઇન તેના સ્પષ્ટીકરણના સંદર્ભમાં સાચી છે તે દર્શાવવા માટે ઔપચારિક ચકાસણી તકનીકોનો ઉપયોગ કરવો શક્ય છે. આ વાસ્તવિક અમલીકરણમાં કોઈપણ મોટા રોકાણો કરવામાં આવે તે પહેલાં ખોટી સિસ્ટમ ડિઝાઇનમાં સુધારો કરવાની મંજૂરી આપે છે. બીજો અભિગમ એ છે કે સ્પષ્ટીકરણને ડિઝાઇનમાં રૂપાંતરિત કરવા માટે કદાચ યોગ્ય શુદ્ધિકરણ પગલાંનો ઉપયોગ કરવો, જે આખરે અમલીકરણમાં રૂપાંતરિત થાય છે જે બાંધકામ દ્વારા સાચું છે. એ નોંધવું અગત્યનું છે કે ઔપચારિક સ્પષ્ટીકરણ એ અમલીકરણ નથી, પરંતુ તેનો ઉપયોગ અમલીકરણ વિકસાવવા માટે થઈ શકે છે. ઔપચારિક સ્પષ્ટીકરણો વર્ણવે છે કે પ્રણાલીએ શું કરવું જોઈએ, નહીં કે પ્રણાલીએ તે કેવી રીતે કરવું જોઈએ. એક સારા સ્પષ્ટીકરણમાં નીચેનામાંથી કેટલાક લક્ષણો હોવા જોઈએઃ પર્યાપ્ત, આંતરિક રીતે સુસંગત, અસંદિગ્ધ, સંપૂર્ણ, સંતુષ્ટ, ન્યૂનતમ એક સારા સ્પષ્ટીકરણમાં હશેઃ રચનાક્ષમતા, વ્યવસ્થાપનક્ષમતા અને વિકાસક્ષમતા ઉપયોગીતા સંચારક્ષમતા શક્તિશાળી અને કાર્યક્ષમ વિશ્લેષણ ઔપચારિક સ્પષ્ટીકરણમાં રસ હોવાનું એક મુખ્ય કારણ એ છે કે તેઓ સોફ્ટવેર અમલીકરણ પર પુરાવા કરવાની ક્ષમતા પ્રદાન કરશે. આ પુરાવાઓનો ઉપયોગ સ્પષ્ટીકરણને માન્ય કરવા, ડિઝાઇનની ચોકસાઈની ચકાસણી કરવા અથવા પ્રોગ્રામ સ્પષ્ટીકરણને સંતોષે છે તે સાબિત કરવા માટે થઈ શકે છે. મર્યાદાઓ ડિઝાઇન (અથવા અમલીકરણ) ને તેના પોતાના પર ક્યારેય "સાચું" જાહેર કરી શકાતી નથી. તે ફક્ત "આપેલ સ્પષ્ટીકરણના સંદર્ભમાં સાચું" હોઈ શકે છે. ઔપચારિક સ્પષ્ટીકરણ ઉકેલવાની સમસ્યાનું યોગ્ય રીતે વર્ણન કરે છે કે કેમ તે એક અલગ મુદ્દો છે. તે સંબોધવા માટે પણ એક મુશ્કેલ મુદ્દો છે કારણ કે તે આખરે અનૌપચારિક નક્કર સમસ્યા ક્ષેત્રની અમૂર્ત ઔપચારિક રજૂઆતો બનાવવાની સમસ્યાની ચિંતા કરે છે, અને આવા અમૂર્ત પગલું ઔપચારિક પુરાવા માટે યોગ્ય નથી. જો કે, સ્પષ્ટીકરણ દ્વારા પ્રદર્શિત થવાની અપેક્ષા હોય તેવા ગુણધર્મોને લગતા "પડકાર" પ્રમેયોને સાબિત કરીને સ્પષ્ટીકરણને માન્ય કરવું શક્ય છે. જો સાચું હોય, તો આ પ્રમેયો સ્પષ્ટીકરણની સ્પષ્ટકર્તાની સમજણ અને અંતર્ગત સમસ્યા ક્ષેત્ર સાથેના તેના સંબંધને મજબૂત કરે છે. જો નહીં, તો સ્પષ્ટીકરણના ઉત્પાદન (અને અમલીકરણ) સાથે સંકળાયેલા લોકોની ક્ષેત્રની સમજણને વધુ સારી રીતે પ્રતિબિંબિત કરવા માટે સ્પષ્ટીકરણને કદાચ બદલવાની જરૂર છે. સોફ્ટવેર વિકાસની ઔપચારિક પદ્ધતિઓનો ઉદ્યોગમાં વ્યાપકપણે ઉપયોગ થતો નથી. મોટાભાગની કંપનીઓ તેમની સોફ્ટવેર વિકાસ પ્રક્રિયાઓમાં તેમને લાગુ કરવા માટે તેને ખર્ચ-અસરકારક માનતી નથી. આ વિવિધ કારણોસર હોઈ શકે છે, જેમાંથી કેટલાક આ પ્રમાણે છેઃ ઓછા માપી શકાય તેવા વળતર સાથે સમયની ઊંચી પ્રારંભિક શરૂઆતની કિંમત લવચીકતા ઘણી સોફ્ટવેર કંપનીઓ ચપળ પદ્ધતિઓનો ઉપયોગ કરે છે જે લવચીકતા પર ધ્યાન કેન્દ્રિત કરે છે. આગળ સમગ્ર પ્રણાલીનું ઔપચારિક સ્પષ્ટીકરણ કરવું ઘણીવાર લવચીકની વિરુદ્ધ હોવાનું માનવામાં આવે છે. જો કે, "ચપળ" વિકાસ જટિલતા સાથે ઔપચારિક સ્પષ્ટીકરણોના ઉપયોગના ફાયદાઓમાં કેટલાક સંશોધન છે તેમને ઉચ્ચ સ્તરની ગાણિતિક કુશળતા અને તેમને અસરકારક રીતે સમજવા અને લાગુ કરવા માટે વિશ્લેષણાત્મક કુશળતાની જરૂર છે આનો ઉકેલ એવા સાધનો અને નમૂનાઓ વિકસાવવા માટે હશે જે આ તકનીકોને અમલમાં મૂકવા માટે પરવાનગી આપે છે પરંતુ અંતર્ગત ગણિતના મર્યાદિત અવકાશને છુપાવે છે તેઓ પ્રોજેક્ટમાં તમામ હિસ્સેદારો માટે રસના ગુણધર્મોને કબજે કરતા નથી તેઓ વપરાશકર્તા ઇન્ટરફેસો અને વપરાશકર્તા ક્રિયાપ્રતિક્રિયાને સ્પષ્ટ કરવાનું સારું કામ કરતા નથી. ઔપચારિક સ્પષ્ટીકરણોના અમલીકરણ તેઓ કેવા પ્રકારની પ્રણાલીનું મોડેલ બનાવવાનો પ્રયાસ કરી રહ્યા છે, તે કેવી રીતે લાગુ કરવામાં આવે છે અને સોફ્ટવેર જીવન ચક્રના કયા તબક્કે રજૂ કરવામાં આવ્યા છે તેના આધારે અલગ અલગ હશે. આ પ્રકારના મોડેલોને નીચેના સ્પષ્ટીકરણના દાખલાઓમાં વર્ગીકૃત કરી શકાય છેઃ સિસ્ટમ ઇતિહાસના દાવાઓ પર આધારિત ઇતિહાસ-આધારિત સ્પષ્ટીકરણ વર્તનનું સમય જતાં અર્થઘટન કરવામાં આવે છે, સિસ્ટમ સ્ટેટ્સ શ્રેણીબદ્ધ ક્રમિક પગલાઓ પર આધારિત રાજ્ય-આધારિત સ્પષ્ટીકરણ વર્તન, (દા. ત. નાણાકીય વ્યવહાર) ઝેડ, વી. ડી. એમ. અથવા બી. જેવી ભાષાઓ સ્ટેટચાર્ટ્સ, પ્રોમેલા, એસ. ટી. ઇ. પી.-એસ. પી. એલ., આર. એસ. એમ. એલ. અથવા એસ. સી. આર. જેવી પ્રતિક્રિયાશીલ પ્રણાલી ભાષાઓ સાથે શ્રેષ્ઠ રીતે ઉપયોગમાં લેવાતી પ્રણાલીના રાજ્ય-થી-રાજ્યમાં સંક્રમણોના આધારે આ નમૂનારૂપ સંક્રમણ-આધારિત સ્પષ્ટીકરણ વર્તણૂક પર આધાર રાખે છે. કાર્યાત્મક સ્પષ્ટીકરણ આ દાખલા પર આધાર રાખે છે. ઓ. બી. જે., એ. એસ. એલ., પી. એલ. યુ. એસ. એસ., એલ. એ. આર. સી. એચ., એચ. ઓ. એલ. અથવા પી. વી. એસ. ગાણિતિક કાર્યોની રચના તરીકે પ્રણાલીને નિર્દિષ્ટ કરે છે. આ દાખલા પર આધાર રાખે છે. પેસલે, જી. આઈ. એસ. ટી., પેટ્રી નેટ અથવા પ્રક્રિયા બીજગણિત જેવી પ્રારંભિક ભાષાઓ આ દાખલા પર આધાર રાખે છે. અહીં સંદર્ભિત પેપર સ્પષ્ટીકરણની રચના કરતી વખતે ઉપયોગમાં લેવા માટેના હ્યુરિસ્ટિક્સની શ્રેષ્ઠ ચર્ચા કરે છે. તેઓ વિભાજીત કરો અને જીતી લો અભિગમ લાગુ કરીને આમ કરે છે. સોફ્ટવેર સાધનો ઝેડ નોટેશન એ અગ્રણી ઔપચારિક સ્પષ્ટીકરણ ભાષાનું ઉદાહરણ છે. અન્યમાં વિયેના વિકાસ પદ્ધતિની સ્પષ્ટીકરણ ભાષા (વી. ડી. એમ.-એસ. એલ.) અને બી-પદ્ધતિની એબ્સ્ટ્રેક્ટ મશીન નોટેશન (એ. એમ. એન.) નો સમાવેશ થાય છે. વેબ સેવાઓ ક્ષેત્રમાં, ઔપચારિક સ્પષ્ટીકરણનો ઉપયોગ ઘણીવાર બિન-કાર્યાત્મક ગુણધર્મો (વેબ સેવાઓની સેવાની ગુણવત્તા) નું વર્ણન કરવા માટે થાય છે. કેટલાક સાધનો છેઃ બીજગણિત લર્ચ ઓબીજે લોટોસ મોડેલ-આધારિત ઝેડ બી વીડીએમ સીએસપી પેટ્રી નેટ્સ ટીએલએ + બીજગણિત સ્પષ્ટીકરણ ઔપચારિક પદ્ધતિઓ પણ જુઓ મોડેલ-આધારિત સ્પષ્ટીકરણ સોફ્ટવેર એન્જિનિયરિંગ સ્પષ્ટીકરણ ભાષા સ્પષ્ટીકરણ (તકનીકી ધોરણ) સંદર્ભો બાહ્ય કડીઓ કોરિઓથ દ્વારા ઔપચારિક સ્પષ્ટીકરણ (તકનીકી) માટે એક કેસ ઔપચારિક પદ્ધતિઓ ઔપચારિક સ્પષ્ટીકરણ