Formal specification
کمپیوٹر سائنس میں، رسمی وضاحتیں ریاضیاتی طور پر مبنی تکنیکیں ہیں جن کا مقصد نظام اور سافٹ ویئر کے نفاذ میں مدد کرنا ہے۔ ان کا استعمال کسی نظام کو بیان کرنے، اس کے رویے کا تجزیہ کرنے اور سخت اور موثر استدلال کے اوزاروں کے ذریعے دلچسپی کی کلیدی خصوصیات کی تصدیق کرکے اس کے ڈیزائن میں مدد کرنے کے لیے کیا جاتا ہے۔ یہ وضاحتیں اس لحاظ سے رسمی ہیں کہ ان کا نحو ہے، ان کے الفاظ ایک ڈومین کے اندر آتے ہیں، اور وہ مفید معلومات کا اندازہ لگانے کے لیے استعمال کیے جا سکتے ہیں۔ تحریک ہر گزرتی دہائی میں کمپیوٹر سسٹم تیزی سے زیادہ طاقتور ہوتے گئے ہیں اور اس کے نتیجے میں وہ معاشرے پر زیادہ اثر انداز ہوتے گئے ہیں۔ اس کی وجہ سے، قابل اعتماد سافٹ ویئر کے ڈیزائن اور نفاذ میں مدد کے لیے بہتر تکنیکوں کی ضرورت ہے۔ قائم شدہ انجینئرنگ کے شعبے ریاضیاتی تجزیہ کو پروڈکٹ ڈیزائن بنانے اور اس کی توثیق کرنے کی بنیاد کے طور پر استعمال کرتے ہیں۔ رسمی وضاحتیں سافٹ ویئر انجینئرنگ کی وشوسنییتا میں اسے حاصل کرنے کا ایک ایسا طریقہ ہے جیسا کہ ایک بار پیش گوئی کی گئی تھی۔ کوڈ کے معیار کو بڑھانے کے لیے جانچ جیسے دیگر طریقے زیادہ عام طور پر استعمال کیے جاتے ہیں۔ استعمال اس طرح کی تفصیلات کو دیکھتے ہوئے، رسمی تصدیق کی تکنیکوں کو استعمال کرنا ممکن ہے تاکہ یہ ظاہر کیا جا سکے کہ سسٹم کا ڈیزائن اس کی تفصیلات کے حوالے سے درست ہے۔ یہ کسی حقیقی نفاذ میں کسی بھی بڑی سرمایہ کاری سے پہلے غلط نظام کے ڈیزائن پر نظر ثانی کرنے کی اجازت دیتا ہے۔ ایک اور نقطہ نظر یہ ہے کہ کسی تفصیلات کو ڈیزائن میں تبدیل کرنے کے لیے ممکنہ طور پر درست اصلاح کے اقدامات کا استعمال کیا جائے، جو بالآخر ایک ایسے نفاذ میں تبدیل ہو جاتا ہے جو تعمیر کے ذریعے درست ہو۔ یہ نوٹ کرنا ضروری ہے کہ ایک رسمی وضاحت عمل درآمد نہیں ہے، بلکہ اسے عمل درآمد کو تیار کرنے کے لیے استعمال کیا جا سکتا ہے۔ رسمی وضاحتیں بیان کرتی ہیں کہ نظام کو کیا کرنا چاہیے، نہ کہ نظام کو یہ کیسے کرنا چاہیے۔ ایک اچھی وضاحت میں درج ذیل میں سے کچھ صفات ہونی چاہئیں: کافی، اندرونی طور پر مستقل، غیر واضح، مکمل، مطمئن، کم سے کم ایک اچھی وضاحت ہوگی: تعمیر پذیری، انتظام پذیری اور ارتقا پذیری استعمال پذیری طاقتور اور موثر تجزیہ رسمی وضاحتوں میں دلچسپی کی ایک اہم وجہ یہ ہے کہ وہ سافٹ ویئر کے نفاذ پر ثبوت انجام دینے کی صلاحیت فراہم کریں گے۔ ان ثبوتوں کا استعمال کسی تفصیلات کی توثیق کرنے، ڈیزائن کی درستگی کی تصدیق کرنے، یا یہ ثابت کرنے کے لیے کیا جا سکتا ہے کہ کوئی پروگرام کسی تفصیلات کو مطمئن کرتا ہے۔ حدود ایک ڈیزائن (یا عمل درآمد) کو کبھی بھی اپنے طور پر "درست" قرار نہیں دیا جا سکتا۔ یہ صرف "دی گئی وضاحت کے حوالے سے درست" ہو سکتا ہے۔ آیا رسمی وضاحت حل کیے جانے والے مسئلے کو صحیح طریقے سے بیان کرتی ہے، یہ ایک الگ مسئلہ ہے۔ اسے حل کرنا بھی ایک مشکل مسئلہ ہے کیونکہ یہ بالآخر ایک غیر رسمی ٹھوس مسئلہ ڈومین کی تجریدی رسمی نمائندگی کی تعمیر کے مسئلے سے متعلق ہے، اور اس طرح کا تجریدی قدم رسمی ثبوت کے قابل نہیں ہے۔ تاہم، خصوصیات سے متعلق "چیلنج" تھیوریمز کو ثابت کرکے کسی وضاحت کی توثیق کرنا ممکن ہے جس کی وضاحت سے توقع کی جاتی ہے۔ اگر درست ہے تو، یہ نظریات تفصیلات کے بارے میں وضاحت کنندہ کی سمجھ اور بنیادی مسئلہ ڈومین کے ساتھ اس کے تعلقات کو تقویت دیتے ہیں۔ اگر نہیں، تو تفصیلات کو بہتر طور پر ظاہر کرنے کے لیے تفصیلات کو تبدیل کرنے کی ضرورت ہے تاکہ تفصیلات کو تیار کرنے (اور نافذ کرنے) میں شامل افراد کی ڈومین تفہیم کی بہتر عکاسی ہو۔ سافٹ ویئر کی ترقی کے رسمی طریقے صنعت میں بڑے پیمانے پر استعمال نہیں ہوتے ہیں۔ زیادہ تر کمپنیاں اپنے سافٹ ویئر ڈویلپمنٹ کے عمل میں ان کا اطلاق کرنا لاگت سے موثر نہیں سمجھتی ہیں۔ یہ مختلف وجوہات کی بناء پر ہو سکتا ہے، جن میں سے کچھ یہ ہیں: کم پیمائش کے قابل منافع کے ساتھ ٹائم ہائی ابتدائی اسٹارٹ اپ لاگت لچک بہت سی سافٹ ویئر کمپنیاں فرتیلی طریقوں کا استعمال کرتی ہیں جو لچک پر توجہ مرکوز کرتی ہیں۔ پورے نظام کی باضابطہ وضاحت کرنا اکثر لچکدار کے برعکس سمجھا جاتا ہے۔ تاہم، "چالاک" ترقی کی پیچیدگی کے ساتھ رسمی وضاحتیں استعمال کرنے کے فوائد کے بارے میں کچھ تحقیق موجود ہے۔ انہیں سمجھنے اور مؤثر طریقے سے ان کا اطلاق کرنے کے لیے اعلی سطح کی ریاضیاتی مہارت اور تجزیاتی مہارت کی ضرورت ہوتی ہے۔ اس کا حل ایسے ٹولز اور ماڈل تیار کرنا ہوگا جو ان تکنیکوں کو نافذ کرنے کی اجازت دیتے ہیں لیکن بنیادی ریاضی کے محدود دائرہ کار کو چھپاتے ہیں۔ وہ پروجیکٹ میں تمام اسٹیک ہولڈرز کے لیے دلچسپی کی خصوصیات پر قبضہ نہیں کرتے ہیں۔ وہ صارف انٹرفیس اور صارف کے تعامل کی وضاحت کرنے کا اچھا کام نہیں کرتے ہیں۔ یہ مکمل طور پر سچ نہیں ہے، ان کے استعمال کو صرف اہم نظاموں کے بنیادی حصوں تک محدود کرکے جو انہوں نے سرمایہ کاری مؤثر ثابت کیا ہے۔ دیگر حدود: آئسولیشن لو لیول آنٹولوجیز ناقص رہنمائی خدشات کی ناقص علیحدگی فیڈ بیک ٹول پیراڈائمز رسمی وضاحتی تکنیک مختلف ڈومینز میں موجود ہیں۔ رسمی وضاحتیں کے نفاذ اس بات پر منحصر ہوں گے کہ وہ کس قسم کے نظام کو ماڈل کرنے کی کوشش کر رہے ہیں، ان کا اطلاق کیسے کیا جاتا ہے اور سافٹ ویئر لائف سائیکل کے کس مقام پر انہیں متعارف کرایا گیا ہے۔ اس قسم کے ماڈلز کو مندرجہ ذیل وضاحتی نمونوں میں درجہ بندی کیا جا سکتا ہے: نظام کی تاریخ پر مبنی تاریخ پر مبنی وضاحتی رویے کے دعووں کی تشریح وقت کے ساتھ ساتھ ریاست پر مبنی وضاحتی رویے کی بنیاد پر نظام ریاستوں کی ترتیب وار مراحل کی سیریز پر کی جاتی ہے، (مثال کے طور پر۔ مالیاتی لین دین) زیڈ، وی ڈی ایم یا بی جیسی زبانیں اس پیراڈائم ٹرانزیشن پر مبنی تفصیلات کے رویے پر انحصار کرتی ہیں جو نظام کی ریاست سے ریاست میں منتقلی پر مبنی ہوتی ہیں جو ایک رد عمل والے نظام کی زبانوں جیسے اسٹیٹ چارٹ، پرومیلا، ایس ٹی ای پی-ایس پی ایل، آر ایس ایم ایل یا ایس سی آر کے ساتھ بہترین طور پر استعمال ہوتی ہیں۔ فنکشنل تفصیلات اس پیراڈائم پر انحصار کرتی ہیں۔ فنکشنل تفصیلات کسی نظام کو ریاضیاتی افعال کے ڈھانچے کے طور پر بیان کرتی ہیں۔ او بی جے، اے ایس ایل، پلس، ایل اے آر سی ایچ، ایچ او ایل یا پی وی ایس اس پیراڈائم آپریشنل تفصیلات پر انحصار کرتی ہیں۔ ابتدائی زبانیں جیسے پیسلی، جی آئی ایس ٹی، پیٹری نیٹ یا پروسیس الجیبرا اس پیراڈائم پر انحصار کرتی ہیں۔ یہاں جس مقالے کا حوالہ دیا گیا ہے اس میں وضاحت کو ڈیزائن کرتے وقت استعمال کرنے کے لیے ہیورسٹکس پر بہترین بحث کی گئی ہے۔ وہ تقسیم اور فتح کے نقطہ نظر کو لاگو کرکے ایسا کرتے ہیں۔ سافٹ ویئر ٹولز زیڈ نوٹیشن ایک معروف رسمی تفصیلات کی زبان کی ایک مثال ہے۔ دیگر میں ویانا ڈویلپمنٹ میتھڈ کی اسپیسیفیکیشن لینگویج (وی ڈی ایم-ایس ایل) اور بی-میتھڈ کی ایبسٹرکٹ مشین نوٹیشن (اے ایم این) شامل ہیں۔ ویب سروسز کے علاقے میں، رسمی تفصیلات اکثر غیر فعال خصوصیات (ویب سروسز کوالٹی آف سروس) کو بیان کرنے کے لیے استعمال ہوتی ہیں۔ کچھ ٹولز یہ ہیں: الجبرائی لارچ او بی جے لوٹوس ماڈل پر مبنی زیڈ بی وی ڈی ایم سی ایس پی پیٹری نیٹ ٹی ایل اے + یہ بھی دیکھیں الجبرائی تفصیلات رسمی طریقے ماڈل پر مبنی تفصیلات سافٹ ویئر انجینئرنگ تفصیلات زبان کی تفصیلات (تکنیکی معیار) حوالہ جات بیرونی لنکس ایک کیس برائے رسمی تفصیلات (ٹیکنالوجی) بذریعہ کوریوتھ 2005-07-30 رسمی طریقے رسمی تفصیلات