Runtime verification
رن ٹائم تصدیق ایک کمپیوٹنگ سسٹم کا تجزیہ اور عمل درآمد کا نقطہ نظر ہے جو چل رہے سسٹم سے معلومات نکالنے پر مبنی ہے اور اسے مشاہدہ شدہ طرز عمل کا پتہ لگانے اور ممکنہ طور پر رد عمل ظاہر کرنے کے لیے استعمال کرتا ہے جو کچھ خصوصیات کو مطمئن یا خلاف ورزی کرتا ہے۔ کچھ بہت ہی خاص خصوصیات، جیسے ڈیٹیرس اور ڈیڈ لاک فریڈم، عام طور پر تمام نظاموں کے ذریعہ مطمئن ہونے کی خواہش رکھتے ہیں اور الگورتھم کے لحاظ سے بہترین طریقے سے نافذ کیے جا سکتے ہیں۔ دیگر خصوصیات کو رسمی وضاحتیں کے طور پر زیادہ آسانی سے پکڑا جا سکتا ہے۔ رن ٹائم تصدیق کی وضاحتیں عام طور پر ٹریس پیش گوئی کے رسمی طریقوں میں ظاہر کی جاتی ہیں، جیسے کہ محدود ریاستی مشینیں، باقاعدہ تاثرات، سیاق و سباق سے پاک نمونے، لکیری عارضی منطق وغیرہ، یا ان کی توسیع۔ یہ عام جانچ سے کم ایڈہاک نقطہ نظر کی اجازت دیتا ہے۔ تاہم، عمل درآمد کرنے والے نظام کی نگرانی کے لیے کسی بھی طریقہ کار کو رن ٹائم تصدیق سمجھا جاتا ہے، جس میں ٹیسٹ اوریکلز اور حوالہ جات کے نفاذ کے خلاف تصدیق شامل ہے۔ جب رسمی ضروریات کی وضاحتیں فراہم کی جاتی ہیں، تو مانیٹروں کو ان سے ترکیب کیا جاتا ہے اور آلات کے ذریعے نظام کے اندر داخل کیا جاتا ہے۔ رن ٹائم تصدیق کو بہت سے مقاصد کے لیے استعمال کیا جا سکتا ہے، جیسے سیکیورٹی یا سیفٹی پالیسی کی نگرانی، ڈیبگنگ، ٹیسٹنگ، تصدیق، توثیق، پروفائلنگ، فالٹ پروٹیکشن، رویے میں ترمیم (مثال کے طور پر، بازیابی) وغیرہ۔ رن ٹائم تصدیق روایتی رسمی تصدیق کی تکنیکوں کی پیچیدگی سے بچتی ہے، جیسے کہ ماڈل چیکنگ اور تھیوریم ثابت کرنا، صرف ایک یا چند عمل کے نشانات کا تجزیہ کرکے اور اصل نظام کے ساتھ براہ راست کام کرکے، اس طرح نسبتا اچھی طرح سے اسکیلنگ کرنا اور نتائج میں زیادہ اعتماد دینا تجزیہ (کیونکہ یہ کم کوریج کی قیمت پر نظام کو باضابطہ طور پر ماڈلنگ کرنے کے تکلیف دہ اور غلطی سے دوچار مرحلے سے بچتا ہے)۔ مزید برآں، اس کی عکاسی کرنے والی صلاحیتوں کے ذریعے رن ٹائم تصدیق کو ٹارگٹ سسٹم کا ایک لازمی حصہ بنایا جا سکتا ہے، تعیناتی کے دوران اس کے نفاذ کی نگرانی اور رہنمائی کی جا سکتی ہے۔ سسٹم یا پروگراموں کو چلانے کے خلاف باضابطہ یا غیر رسمی طور پر مخصوص خصوصیات کی جانچ کرنا ایک پرانا موضوع ہے (قابل ذکر مثالیں سافٹ ویئر میں متحرک ٹائپنگ، یا ہارڈ ویئر میں فیل سیف ڈیوائسز یا واچ ڈاگ ٹائمرز ہیں)، جن کی عین مطابق جڑوں کی شناخت کرنا مشکل ہے۔ اصطلاحات رن ٹائم تصدیق کو باضابطہ طور پر 2001 کی ورکشاپ کے نام سے متعارف کرایا گیا تھا جس کا مقصد رسمی تصدیق اور جانچ کے درمیان کے مسائل کو حل کرنا تھا۔ بڑے کوڈ بیسز کے لیے، دستی طور پر ٹیسٹ کیس لکھنا بہت وقت طلب ثابت ہوتا ہے۔ اس کے علاوہ، ترقی کے دوران تمام غلطیوں کا پتہ نہیں لگایا جا سکتا۔ خلائی جہاز، روورز اور ایوینکس ٹیکنالوجی میں اعلی حفاظتی معیارات کو محفوظ کرنے کے لیے کلاؤس ہیولینڈ اور گریگور روزو کے ذریعے ناسا ایمس ریسرچ سینٹر میں خودکار تصدیق میں ابتدائی شراکت کی گئی تھی۔ انہوں نے عارضی منطق میں وضاحتیں کی تصدیق کرنے اور واحد عمل کے راستوں کا تجزیہ کرکے جاوا پروگراموں میں ریس کے حالات اور ڈیڈ لاک کا پتہ لگانے کے لیے ایک ٹول کی تجویز پیش کی۔ فی الحال، رن ٹائم تصدیق کی تکنیکوں کو اکثر مختلف متبادل ناموں کے ساتھ پیش کیا جاتا ہے، جیسے رن ٹائم کی نگرانی، رن ٹائم چیکنگ، رن ٹائم ریفلیکشن، رن ٹائم تجزیہ، متحرک تجزیہ، رن ٹائم/متحرک علامتی تجزیہ، ٹریس تجزیہ، لاگ فائل تجزیہ وغیرہ، یہ سب ایک ہی اعلی سطح کے تصور کی مثالوں کا حوالہ دیتے ہیں جو یا تو مختلف علاقوں پر یا مختلف برادریوں کے اسکالرز کے ذریعہ لاگو ہوتے ہیں۔ رن ٹائم تصدیق کا دیگر اچھی طرح سے قائم علاقوں سے گہرا تعلق ہے، جیسے کہ تعیناتی سے پہلے استعمال ہونے پر جانچ (خاص طور پر ماڈل پر مبنی جانچ) اور تعیناتی کے دوران استعمال ہونے پر غلطی برداشت کرنے والے نظام۔ رن ٹائم تصدیق کے وسیع شعبے میں، کوئی بھی کئی زمروں میں فرق کر سکتا ہے، جیسے: "تفصیلات سے کم" نگرانی جو زیادہ تر ہم آہنگی سے متعلق خصوصیات جیسے ایٹمائٹی کے ایک مقررہ سیٹ کو نشانہ بناتی ہے۔ اس شعبے میں اہم کام سیویج اور دیگر کا ہے۔ عارضی منطق کی خصوصیات کے حوالے سے ایرسر الگورتھم کی نگرانی کے ساتھ ؛ اس سمت میں ابتدائی شراکت لی، کنن، اور ان کے ساتھیوں، اور ہیولینڈ اور روسو نے کی ہے۔ بنیادی نقطہ نظر رن ٹائم تصدیق کے طریقوں کے وسیع میدان کو تین جہتوں کے ذریعے درجہ بند کیا جا سکتا ہے: عمل کے دوران (آن لائن) یا عمل کے بعد جیسے نظام کی نگرانی کی جا سکتی ہے۔ لاگ تجزیہ کی شکل میں (آف لائن)۔ تصدیق کرنے والا کوڈ سسٹم میں ضم کیا جاتا ہے (جیسا کہ پہلو پر مبنی پروگرامنگ میں کیا جاتا ہے) یا بیرونی وجود کے طور پر فراہم کیا جاتا ہے۔ مانیٹر مطلوبہ تفصیلات کی خلاف ورزی یا توثیق کی اطلاع دے سکتا ہے۔ اس کے باوجود، رن ٹائم تصدیق میں بنیادی عمل ایک جیسا رہتا ہے: ایک مانیٹر کچھ رسمی تفصیلات سے بنایا جاتا ہے۔ یہ عمل عام طور پر خود بخود کیا جا سکتا ہے اگر رسمی زبان کے فارمولوں کے لیے مساوی آٹومیٹا موجود ہوں جس میں پراپرٹی کی وضاحت کی گئی ہے۔ باقاعدہ اظہار کو تبدیل کرنے کے لیے، ایک محدود ریاستی مشین استعمال کی جا سکتی ہے۔ لکیری عارضی منطق میں ایک خاصیت کو بوچی آٹومیٹن میں تبدیل کیا جا سکتا ہے (بوچی آٹومیٹن کے لیے لکیری عارضی منطق بھی دیکھیں)۔ اس نظام کو مانیٹر کو اس کے نفاذ کی حالت سے متعلق واقعات بھیجنے کے لیے تیار کیا گیا ہے۔ سسٹم پر عمل درآمد کیا جاتا ہے اور مانیٹر کے ذریعے اس کی تصدیق کی جاتی ہے۔ مانیٹر موصولہ ایونٹ ٹریس کی تصدیق کرتا ہے اور فیصلہ پیش کرتا ہے کہ آیا تفصیلات مطمئن ہیں یا نہیں۔ مزید برآں، مانیٹر ممکنہ طور پر غلط رویے کو درست کرنے کے لیے سسٹم کو فیڈ بیک بھیجتا ہے۔ آف لائن نگرانی کا استعمال کرتے وقت سسٹم آف کاز کو کوئی فیڈ بیک نہیں مل سکتا، کیونکہ تصدیق بعد میں کی جاتی ہے۔ مثالیں نیچے دی گئی مثالیں کچھ سادہ خصوصیات پر تبادلہ خیال کرتی ہیں جن پر اس تحریر (اپریل 2011) کے وقت تک کئی رن ٹائم تصدیق گروپوں کے ذریعہ ممکنہ طور پر چھوٹی تبدیلیوں کے ساتھ غور کیا گیا ہے۔ انہیں مزید دلچسپ بنانے کے لیے، نیچے دی گئی ہر خاصیت ایک مختلف وضاحتی رسم الخط کا استعمال کرتی ہے اور یہ سب پیرامیٹرک ہیں۔ پیرامیٹرک خصوصیات پیرامیٹرک واقعات کے ساتھ بننے والے نشانات کے بارے میں خصوصیات ہیں، جو ایسے واقعات ہیں جو اعداد و شمار کو پیرامیٹرز سے باندھتے ہیں۔ یہاں ایک پیرامیٹرک پراپرٹی کی شکل ہوتی ہے، جہاں عام (غیر مصدقہ) پیرامیٹرک واقعات کا حوالہ دیتے ہوئے کچھ مناسب رسم الخط میں ایک وضاحت ہوتی ہے۔ اس طرح کی پیرامیٹرک خصوصیات کے لیے انترجشتھان یہ ہے کہ جس خاصیت کا اظہار کیا گیا ہے وہ مشاہدہ شدہ ٹریس میں (پیرامیٹرک واقعات کے ذریعے) درپیش تمام پیرامیٹر مثالوں کے لیے ہونا چاہیے۔ مندرجہ ذیل میں سے کوئی بھی مثال کسی خاص رن ٹائم تصدیق کے نظام کے لیے مخصوص نہیں ہے، حالانکہ پیرامیٹرز کے لیے سپورٹ کی واضح طور پر ضرورت ہے۔ مندرجہ ذیل مثالوں میں جاوا نحو فرض کیا گیا ہے، اس طرح "= =" منطقی مساوات ہے، جبکہ "=" تفویض ہے۔ کچھ طریقے (مثال کے طور پر، ان سیف اینم ایکسمپل میں اپ ڈیٹ ()) ڈمی طریقے ہیں، جو جاوا اے پی آئی کا حصہ نہیں ہیں، جو وضاحت کے لیے استعمال ہوتے ہیں۔ جاوا آئیٹرٹر انٹرفیس کے لیے ضروری ہے کہ نیکسٹ () طریقہ کو کال کیا جائے اور اگلا () طریقہ کال کرنے سے پہلے درست واپس کیا جائے۔ اگر ایسا نہیں ہوتا ہے، تو یہ بہت ممکن ہے کہ صارف کلیکشن کے "آف اینڈ" کو دہرائے۔ دائیں طرف کی شکل ایک محدود ریاستی مشین کو دکھاتی ہے جو رن ٹائم تصدیق کے ساتھ اس پراپرٹی کو چیک کرنے اور نافذ کرنے کے لیے ممکنہ مانیٹر کی وضاحت کرتی ہے۔ نامعلوم حالت سے، اگلے () طریقہ کو کال کرنا ہمیشہ ایک غلطی ہوتی ہے کیونکہ اس طرح کا آپریشن غیر محفوظ ہو سکتا ہے۔ اگر ہے نیکسٹ () کو کال کیا جاتا ہے اور سچ آتا ہے، تو نیکسٹ () کو کال کرنا محفوظ ہے، لہذا مانیٹر زیادہ حالت میں داخل ہوتا ہے۔ اگر، تاہم، ہے نیکسٹ () طریقہ غلط واپسی کرتا ہے، تو مزید عناصر نہیں ہیں، اور مانیٹر کوئی حالت میں داخل نہیں ہوتا ہے۔ زیادہ اور کوئی نہیں ریاستوں میں، ہیز نیکسٹ () طریقہ کال کرنے سے کوئی نئی معلومات فراہم نہیں ہوتی ہیں۔ مزید ریاست سے اگلے () طریقہ کو کال کرنا محفوظ ہے، لیکن اگر مزید عناصر موجود ہیں تو یہ نامعلوم ہو جاتا ہے، لہذا مانیٹر ابتدائی نامعلوم حالت میں دوبارہ داخل ہوتا ہے۔ آخر میں، کوئی حالت نہیں سے اگلے () طریقہ کو کال کرنے کے نتیجے میں غلطی کی حالت میں داخل ہوتا ہے۔ پیرامیٹرک ماضی کے وقت لکیری عارضی منطق کا استعمال کرتے ہوئے اس پراپرٹی کی نمائندگی مندرجہ ذیل ہے۔ یہ فارمولا کہتا ہے کہ اگلے () طریقہ پر کسی بھی کال سے فوری طور پر پہلے کال ٹو ہیز نیکسٹ () طریقہ ہونا چاہیے جو درست آتا ہے۔ یہاں پراپرٹی Iterator i میں پیرامیٹرک ہے۔ تصوراتی طور پر، اس کا مطلب یہ ہے کہ ٹیسٹ پروگرام میں ہر ممکنہ آئیٹریٹر کے لیے مانیٹر کی ایک کاپی ہوگی، حالانکہ رن ٹائم تصدیق کے نظام کو اپنے پیرامیٹرک مانیٹر کو اس طرح نافذ کرنے کی ضرورت نہیں ہے۔ اس پراپرٹی کے لیے مانیٹر کو فارمولے کی خلاف ورزی ہونے پر ہینڈلر کو متحرک کرنے کے لیے سیٹ کیا جائے گا (مساوی طور پر جب فائنیٹ اسٹیٹ مشین ایرر اسٹیٹ میں داخل ہوتی ہے)، جو اس وقت ہوگا جب یا تو نیکسٹ () کو پہلے کال کیے بغیر نیکسٹ () کال کیا جائے، یا جب نیکسٹ () کو نیکسٹ () سے پہلے کال کیا جائے، لیکن غلط واپس کیا جائے۔ ان سیف اینم جاوا میں ویکٹر کلاس کے پاس اپنے عناصر پر تکرار کرنے کے دو ذرائع ہیں۔ جیسا کہ پچھلی مثال میں دیکھا گیا ہے، کوئی بھی آئیٹرٹر انٹرفیس استعمال کر سکتا ہے، یا کوئی اینومریشن انٹرفیس استعمال کر سکتا ہے۔ Iterator انٹرفیس کے لیے ہٹانے کے طریقہ کار کے اضافے کے علاوہ، بنیادی فرق یہ ہے کہ Iterator "فیل فاسٹ" ہے جبکہ گنتی نہیں ہے۔ اس کا مطلب یہ ہے کہ اگر کوئی ویکٹر میں ترمیم کرتا ہے (آئیٹرٹر ہٹانے کے طریقہ کار کے استعمال کے علاوہ) جب کوئی آئیٹرٹر کا استعمال کرتے ہوئے ویکٹر پر دہرا رہا ہوتا ہے، تو ایک کنکرنٹ موڈیفیکیشن ایکسسیپشن پھینک دیا جاتا ہے۔ تاہم، گنتی کا استعمال کرتے وقت یہ معاملہ نہیں ہے، جیسا کہ ذکر کیا گیا ہے۔ اس کے نتیجے میں کسی پروگرام سے غیر متعین نتائج سامنے آسکتے ہیں کیونکہ ویکٹر کو گنتی کے نقطہ نظر سے متضاد حالت میں چھوڑ دیا جاتا ہے۔ میراث پروگراموں کے لیے جو اب بھی گنتی انٹرفیس استعمال کرتے ہیں، کوئی یہ نافذ کرنا چاہے گا کہ جب ان کے بنیادی ویکٹر میں ترمیم کی جاتی ہے تو گنتی کا استعمال نہیں کیا جاتا ہے۔ اس رویے کو نافذ کرنے کے لیے درج ذیل پیرامیٹرک باقاعدہ نمونہ استعمال کیا جا سکتا ہے: β ویکٹر v، گنتی e: (e = v.elements ()) (e.nextElement ()) * v.update () e.nextElement () یہ نمونہ گنتی اور ویکٹر دونوں میں پیرامیٹرک ہے۔ بدیہی طور پر، اور جیسا کہ اوپر رن ٹائم تصدیق کے نظام کو اپنے پیرامیٹرک مانیٹروں کو اس طرح سے نافذ کرنے کی ضرورت نہیں ہے، کوئی بھی اس پراپرٹی کے لیے پیرامیٹرک مانیٹر کو ویکٹر اور گنتی کے ہر ممکنہ جوڑے کے لیے غیر پیرامیٹرک مانیٹر کی مثال بنانے اور اس پر نظر رکھنے کے طور پر سوچ سکتا ہے۔ کچھ واقعات ایک ہی وقت میں کئی مانیٹروں سے متعلق ہو سکتے ہیں، جیسے کہ v.update ()، لہذا رن ٹائم تصدیق کے نظام کو (دوبارہ تصوراتی طور پر) انہیں تمام دلچسپی رکھنے والے مانیٹروں کو بھیجنا چاہیے۔ یہاں پراپرٹی کی وضاحت کی گئی ہے تاکہ یہ پروگرام کے برے طرز عمل کو بیان کرے۔ اس پراپرٹی کی، پھر، پیٹرن کے مماثلت کے لیے نگرانی کی جانی چاہیے۔ دائیں طرف کی شکل جاوا کوڈ کو دکھاتی ہے جو اس پیٹرن سے میل کھاتا ہے، اس طرح پراپرٹی کی خلاف ورزی کرتا ہے۔ ویکٹر، v، کو گنتی کے بعد اپ ڈیٹ کیا جاتا ہے، e، بنایا جاتا ہے، اور پھر e استعمال کیا جاتا ہے۔ سیف لاک پچھلی دو مثالیں محدود ریاستی خصوصیات کو ظاہر کرتی ہیں، لیکن رن ٹائم تصدیق میں استعمال ہونے والی خصوصیات بہت زیادہ پیچیدہ ہو سکتی ہیں۔ سیف لاک پراپرٹی اس پالیسی کو نافذ کرتی ہے کہ (ری اینٹرنٹ) لاک کلاس کے حصول اور ریلیز کی تعداد ایک دی گئی میتھڈ کال کے اندر مل جاتی ہے۔ یہ، یقینا، لاک کو حاصل کرنے والے طریقوں کے علاوہ دیگر طریقوں سے جاری کرنے کی اجازت نہیں دیتا ہے، لیکن یہ ممکنہ طور پر تجربہ شدہ نظام کے حصول کے لیے ایک مطلوبہ ہدف ہے۔ ذیل میں ایک پیرامیٹرک سیاق و سباق سے پاک پیٹرن کا استعمال کرتے ہوئے اس پراپرٹی کی ایک وضاحت ہے: تھریڈ t، لاک l: S → ε | S شروع (t) S اختتام (t) | S l.acquire (t) S l.release (t) پیٹرن ہر تھریڈ اور لاک (خالی ترتیب ہے) کے لیے نیسٹڈ اسٹارٹ/اینڈ اور ایکوائر/ریلیز جوڑوں کے متوازن ترتیب کی وضاحت کرتا ہے۔ یہاں شروع اور اختتام پروگرام میں ہر طریقہ کے آغاز اور اختتام کا حوالہ دیتے ہیں (سوائے خود کو حاصل کرنے اور جاری کرنے کی کالوں کے)۔ وہ تھریڈ میں پیرامیٹرک ہیں کیونکہ طریقوں کے آغاز اور اختتام کو جوڑنا ضروری ہے اگر اور صرف اس صورت میں جب وہ ایک ہی تھریڈ سے تعلق رکھتے ہوں۔ حاصل کرنے اور جاری کرنے کے واقعات بھی اسی وجہ سے تھریڈ میں پیرامیٹرک ہیں۔ وہ، اضافی طور پر، لاک میں پیرامیٹرک ہیں کیونکہ ہم ایک لاک کی ریلیز کو دوسرے کے حصول سے جوڑنا نہیں چاہتے ہیں۔ انتہائی حد تک، یہ ممکن ہے کہ تھریڈ کے ساتھ لاک کے ہر ممکنہ امتزاج کے لیے پراپرٹی کی ایک مثال ہو، یعنی سیاق و سباق سے پاک تجزیہ کے طریقہ کار کی ایک کاپی ؛ ایسا ایک بار پھر، بدیہی طور پر ہوتا ہے، کیونکہ رن ٹائم تصدیق کے نظام ایک ہی فعالیت کو مختلف طریقے سے نافذ کر سکتے ہیں۔ مثال کے طور پر، اگر کسی سسٹم میں تھریڈز ہیں، اور لاکس اور کے ساتھ، تو جوڑوں کے لیے پراپرٹی کے مثالوں کو برقرار رکھنا ممکن ہے <،>، <،>، <،>، <،>، <،>، <،>، اور <،>۔ اس خاصیت کی نگرانی پیٹرن سے ملنے میں ناکامیوں کے لیے کی جانی چاہیے کیونکہ پیٹرن صحیح رویے کی وضاحت کرتا ہے۔ دائیں طرف کی شکل ایک نشان دکھاتی ہے جو اس پراپرٹی کی دو خلاف ورزیاں پیدا کرتی ہے۔ شکل میں نیچے کے اقدامات کسی طریقہ کار کے آغاز کی نمائندگی کرتے ہیں، جبکہ اوپر کے اقدامات اختتام ہوتے ہیں۔ شکل میں سرمئی تیر اسی لاک کے دیئے گئے حصول اور ریلیز کے درمیان مماثلت کو ظاہر کرتے ہیں۔ سادگی کے لیے، ٹریس صرف ایک تھریڈ اور ایک لاک دکھاتا ہے۔ تحقیقی چیلنجز اور ایپلی کیشنز رن ٹائم تصدیق کی زیادہ تر تحقیق ذیل میں درج کردہ ایک یا زیادہ موضوعات سے خطاب کرتی ہے۔ رن ٹائم اوور ہیڈ کو کم کرنا ایک ایگزیکٹو سسٹم کا مشاہدہ کرنے میں عام طور پر کچھ رن ٹائم اوور ہیڈ ہوتا ہے (ہارڈ ویئر مانیٹر اس سے مستثنی ہو سکتے ہیں)۔ رن ٹائم تصدیقی ٹولز کے اوور ہیڈ کو زیادہ سے زیادہ کم کرنا ضروری ہے، خاص طور پر جب تیار کردہ مانیٹر سسٹم کے ساتھ تعینات ہوں۔ رن ٹائم اوور ہیڈ کم کرنے کی تکنیکوں میں شامل ہیں: بہتر آلات سازی۔ انجام دینے والے نظام سے واقعات کو نکالنا اور انہیں مانیٹروں کو بھیجنا اگر بے وقوفی سے کیا جائے تو ایک بڑا رن ٹائم اوور ہیڈ پیدا کر سکتا ہے۔ کسی بھی رن ٹائم تصدیق کے ٹول کے لیے اچھا سسٹم انسٹرومینٹیشن اہم ہے، جب تک کہ ٹول واضح طور پر موجودہ عمل درآمد کے لاگ کو نشانہ نہ بنائے۔ موجودہ استعمال میں آلات سازی کے بہت سے طریقے ہیں، جن میں سے ہر ایک کے اپنے فوائد اور نقصانات ہیں، جو اپنی مرضی کے مطابق یا دستی آلات سازی سے لے کر خصوصی کتب خانوں تک، پہلو پر مبنی زبانوں میں تالیف کرنے، ورچوئل مشین کو بڑھانے، ہارڈ ویئر سپورٹ پر تعمیر کرنے تک ہیں۔ جامد تجزیہ کے ساتھ امتزاج۔ جامد اور متحرک تجزیوں کا ایک عام مجموعہ، خاص طور پر مرتب کرنے والوں میں درپیش، ان تمام ضروریات کی نگرانی کرنا ہے جنہیں مستحکم طور پر خارج نہیں کیا جا سکتا۔ ایک دوہری اور بالآخر مساوی نقطہ نظر رن ٹائم تصدیق میں معمول بن جاتا ہے، یعنی جامد تجزیہ کا استعمال کرنا تاکہ بصورت دیگر مکمل نگرانی کی مقدار کو کم کیا جا سکے۔ جامد تجزیہ نگرانی کے لیے پراپرٹی اور نگرانی کے لیے سسٹم دونوں پر کیا جا سکتا ہے۔ نگرانی کے لیے جائیداد کا جامد تجزیہ یہ ظاہر کر سکتا ہے کہ بعض واقعات کی نگرانی کرنا غیر ضروری ہے، کہ بعض مانیٹروں کی تخلیق میں تاخیر ہو سکتی ہے، اور یہ کہ کچھ موجودہ مانیٹر کبھی متحرک نہیں ہوں گے اور اس طرح کچرا جمع کیا جا سکتا ہے۔ نگرانی کے لیے نظام کا جامد تجزیہ ایسے کوڈ کا پتہ لگا سکتا ہے جو مانیٹر کو کبھی متاثر نہیں کر سکتا۔ مثال کے طور پر، اوپر کی ہاس نیکسٹ پراپرٹی کی نگرانی کرتے وقت، کسی کو کوڈ کے انسٹرومنٹ حصوں کی ضرورت نہیں ہے جہاں ہر کال i.next () کسی بھی راستے پر فوری طور پر کال i.hasnext () سے پہلے ہوتی ہے جو درست واپسی کرتی ہے (کنٹرول فلو گراف پر نظر آتی ہے)۔ موثر نگرانی کی پیداوار اور انتظام۔ پیرامیٹرک خصوصیات کی نگرانی کرتے وقت جیسے کہ اوپر کی مثالوں میں، نگرانی کے نظام کو ہر پیرامیٹر کی مثال کے حوالے سے نگرانی کی گئی پراپرٹی کی حیثیت پر نظر رکھنے کی ضرورت ہے۔ اس طرح کی مثالوں کی تعداد نظریاتی طور پر لامحدود ہے اور عملی طور پر بہت زیادہ ہوتی ہے۔ ایک اہم تحقیقی چیلنج یہ ہے کہ مشاہدہ شدہ واقعات کو مؤثر طریقے سے ان مثالوں تک کیسے پہنچایا جائے جن کی انہیں ضرورت ہے۔ ایک متعلقہ چیلنج یہ ہے کہ اس طرح کی مثالوں کی تعداد کو کس طرح کم رکھا جائے (تاکہ ترسیل تیز ہو)، یا دوسرے لفظوں میں، جب تک ممکن ہو غیر ضروری مثالوں کو بنانے سے کیسے بچا جائے اور دو طرح سے، پہلے سے پیدا شدہ مثالوں کو جیسے ہی وہ غیر ضروری ہو جائیں کیسے ہٹا دیا جائے۔ آخر میں، پیرامیٹرک نگرانی الگورتھم عام طور پر غیر پیرامیٹرک مانیٹر تیار کرنے کے لیے اسی طرح کے الگورتھم کو عام کرتے ہیں۔ اس طرح، پیدا شدہ غیر پیرامیٹرک مانیٹروں کا معیار نتیجے میں آنے والے پیرامیٹرک مانیٹروں کے معیار کا تعین کرتا ہے۔ تاہم، تصدیق کے دوسرے طریقوں (مثال کے طور پر، ماڈل چیکنگ) کے برعکس، رن ٹائم تصدیق میں ریاستوں کی تعداد یا تیار کردہ مانیٹر کا سائز کم اہم ہے۔ درحقیقت، کچھ مانیٹروں میں لامحدود طور پر بہت سی ریاستیں ہو سکتی ہیں، جیسے کہ اوپر سیف لاک پراپرٹی کے لیے، حالانکہ کسی بھی وقت صرف ایک محدود تعداد میں ریاستیں واقع ہو سکتی ہیں۔ اہم بات یہ ہے کہ مانیٹر کسی ریاست سے اس کی اگلی حالت میں کتنی مؤثر طریقے سے منتقل ہوتا ہے جب اسے عمل درآمد کے نظام سے کوئی واقعہ موصول ہوتا ہے۔ خصوصیات کی وضاحت تمام رسمی طریقوں کی ایک بڑی عملی رکاوٹ یہ ہے کہ ان کے صارفین اس سے گریزاں ہیں، یا نہیں جانتے اور وضاحتیں پڑھنا یا لکھنا نہیں سیکھنا چاہتے ہیں۔ کچھ معاملات میں وضاحتیں مضمر ہوتی ہیں، جیسے کہ ڈیڈ لاک اور ڈیٹا ریس کے لیے، لیکن زیادہ تر معاملات میں انہیں تیار کرنے کی ضرورت ہوتی ہے۔ ایک اضافی تکلیف، خاص طور پر رن ٹائم تصدیق کے تناظر میں، یہ ہے کہ بہت سی موجودہ وضاحتی زبانیں مطلوبہ خصوصیات کو حاصل کرنے کے لیے کافی اظہار نہیں کرتی ہیں۔ بہتر رسمی کارروائیاں۔ رن ٹائم توثیقی کمیونٹی میں ایک قابل ذکر کام تفصیلات کی رسمی کارروائیوں کو ڈیزائن کرنے میں لگایا گیا ہے جو روایتی تفصیلات کی رسمی کارروائیوں سے بہتر رن ٹائم تصدیق کے لیے مطلوبہ ایپلی کیشن ڈومینز میں فٹ ہوتے ہیں۔ ان میں سے کچھ روایتی رسم الخط میں معمولی یا کوئی نحو تبدیلیوں پر مشتمل نہیں ہیں، لیکن صرف ان کے الفاظ میں تبدیلیوں پر مشتمل ہیں (مثال کے طور پر، محدود ٹریس بمقابلہ لامحدود ٹریس الفاظ، وغیرہ)۔ اور ان کے نفاذ کے لیے (بوچی آٹومیٹا وغیرہ کے بجائے بہتر محدود ریاستی مشینیں)۔ دوسرے موجودہ رسمی کارروائیوں کو ایسی خصوصیات کے ساتھ توسیع دیتے ہیں جو رن ٹائم تصدیق کے لیے قابل قبول ہیں لیکن تصدیق کے دیگر طریقوں کے لیے آسانی سے نہیں ہو سکتے، جیسے کہ پیرامیٹرز کو شامل کرنا، جیسا کہ اوپر کی مثالوں میں دیکھا گیا ہے۔ آخر میں، تفصیلات کی رسمیں ہیں جو خاص طور پر رن ٹائم تصدیق کے لیے ڈیزائن کی گئی ہیں، اس ڈومین کے لیے اپنی بہترین کارکردگی حاصل کرنے کی کوشش کر رہی ہیں اور دوسرے ایپلیکیشن ڈومینز کے بارے میں بہت کم پرواہ کر رہی ہیں۔ رن ٹائم تصدیق کے لیے عالمگیر طور پر بہتر یا ڈومین-خاص طور پر بہتر تفصیلات کی رسمی کارروائیوں کو ڈیزائن کرنا اس کے بڑے تحقیقی چیلنجوں میں سے ایک ہے اور رہے گا۔ مقداری خصوصیات۔ دیگر تصدیق کے طریقوں کے مقابلے میں، رن ٹائم تصدیق سسٹم اسٹیٹ متغیرات کی ٹھوس اقدار پر کام کرنے کے قابل ہے، جس سے پروگرام کے نفاذ کے بارے میں شماریاتی معلومات اکٹھا کرنا اور اس معلومات کو پیچیدہ مقداری خصوصیات کا اندازہ کرنے کے لیے استعمال کرنا ممکن ہوتا ہے۔ مزید اظہار خیال کی خصوصیات والی زبانوں کی ضرورت ہے جو ہمیں اس صلاحیت کو مکمل طور پر استعمال کرنے کی اجازت دیں۔ بہتر انٹرفیس۔ غیر ماہرین کے لیے جائیداد کی وضاحتیں پڑھنا اور لکھنا آسان نہیں ہے۔ یہاں تک کہ ماہرین بھی اکثر نسبتا چھوٹے عارضی منطق فارمولوں (خاص طور پر جب انہوں نے "تک" آپریٹرز کو نیسٹ کیا ہو) پر منٹ تک گھورتے رہتے ہیں۔ ایک اہم تحقیقی شعبہ مختلف تفصیلات کی رسمی کارروائیوں کے لیے طاقتور یوزر انٹرفیس تیار کرنا ہے جو صارفین کو زیادہ آسانی سے سمجھنے، لکھنے اور شاید خصوصیات کو تصور کرنے کی اجازت دے۔ کان کنی کی وضاحتیں۔ اس بات سے کوئی فرق نہیں پڑتا کہ صارفین کو وضاحتیں تیار کرنے میں مدد کے لیے کون سا ٹول سپورٹ دستیاب ہے، وہ تقریبا ہمیشہ اس بات پر زیادہ خوش ہوں گے کہ انہیں کوئی وضاحتیں نہیں لکھنی پڑیں گی، خاص طور پر جب وہ معمولی ہوں۔ خوش قسمتی سے، وہاں بہت سارے پروگرام موجود ہیں جو ان اعمال/واقعات کا صحیح استعمال کرتے ہیں جن کے بارے میں کوئی شخص خصوصیات رکھنا چاہتا ہے۔ اگر ایسا ہے، تو یہ قابل فہم ہے کہ کوئی خود بخود ان سے مطلوبہ خصوصیات سیکھ کر ان درست پروگراموں کا استعمال کرنا چاہے گا۔ یہاں تک کہ اگر خود بخود کان کنی کی گئی وضاحتیں کا مجموعی معیار دستی طور پر تیار کردہ وضاحتیں سے کم ہونے کی توقع کی جاتی ہے، تو وہ مؤخر الذکر کے لیے ایک ابتدائی نقطہ کے طور پر یا خودکار رن ٹائم تصدیق کے ٹولز کی بنیاد کے طور پر کام کر سکتے ہیں جس کا مقصد خاص طور پر کیڑے تلاش کرنا ہے (جہاں ناقص تفصیلات غلط مثبت یا منفی میں بدل جاتی ہیں، جو اکثر جانچ کے دوران قابل قبول ہوتی ہیں)۔ عمل کے نمونے اور پیشین گوئی کا تجزیہ غلطیوں کا پتہ لگانے کے لیے رن ٹائم تصدیق کنندہ کی صلاحیت کا سختی سے انحصار عمل کے نشانات کا تجزیہ کرنے کی اس کی صلاحیت پر ہوتا ہے۔ جب مانیٹر کو سسٹم کے ساتھ تعینات کیا جاتا ہے، تو آلات عام طور پر کم سے کم ہوتے ہیں اور رن ٹائم اوور ہیڈ کو کم رکھنے کے لیے ان پر عمل درآمد کے نشانات ہر ممکن حد تک آسان ہوتے ہیں۔ جب رن ٹائم تصدیق کو جانچ کے لیے استعمال کیا جاتا ہے، تو کوئی بھی زیادہ جامع آلات کا متحمل ہو سکتا ہے جو اہم نظام کی معلومات کے ساتھ واقعات کو بڑھاتا ہے جسے مانیٹر کے ذریعے عمل درآمد کے نظام کے زیادہ بہتر ماڈلز کی تعمیر اور تجزیہ کے لیے استعمال کیا جا سکتا ہے۔ مثال کے طور پر، ویکٹر گھڑی کی معلومات کے ساتھ اور ڈیٹا اور کنٹرول فلو کی معلومات کے ساتھ واقعات کو بڑھانا مانیٹروں کو چلانے والے نظام کا ایک کازل ماڈل بنانے کی اجازت دیتا ہے جس میں مشاہدہ شدہ عمل صرف ایک ممکنہ مثال تھی۔ واقعات کی کوئی بھی دوسری ترتیب جو ماڈل کے مطابق ہو، نظام کا ایک قابل عمل عمل ہے، جو ایک مختلف دھاگے کے درمیان ہو سکتا ہے۔ اس طرح کی قیاس شدہ پھانسیوں میں جائیداد کی خلاف ورزیوں کا پتہ لگانے سے (ان کی نگرانی کرکے) مانیٹر ان غلطیوں کی پیش گوئی کرتا ہے جو مشاہدہ شدہ پھانسیوں میں نہیں ہوئیں، لیکن جو اسی نظام کے دوسرے پھانسیوں میں ہو سکتی ہیں۔ ایک اہم تحقیقی چیلنج پھانسی کے نشانات سے ماڈل نکالنا ہے جو زیادہ سے زیادہ دوسرے پھانسی کے نشانات پر مشتمل ہوتے ہیں۔ طرز عمل میں ترمیم جانچ یا مکمل تصدیق کے برعکس، رن ٹائم تصدیق نظام کو دریافت شدہ خلاف ورزیوں سے بازیافت کرنے کی اجازت دینے کا وعدہ رکھتی ہے، دوبارہ تشکیل، مائیکرو ریسیٹ، یا باریک مداخلت کے طریقہ کار کے ذریعے جسے بعض اوقات ٹیوننگ یا اسٹیئرنگ کہا جاتا ہے۔ رن ٹائم تصدیق کے سخت فریم ورک کے اندر ان تکنیکوں کا نفاذ اضافی چیلنجوں کو جنم دیتا ہے۔ اعمال کی وضاحت۔ کسی کو تجریدی انداز میں کی جانے والی ترمیم کی وضاحت کرنے کی ضرورت ہے جس کے لیے صارف کو غیر متعلقہ نفاذ کی تفصیلات جاننے کی ضرورت نہیں ہے۔ اس کے علاوہ، نظام کی سالمیت کو برقرار رکھنے کے لیے اس طرح کی ترمیم کب ہو سکتی ہے اس کی وضاحت کرنے کی ضرورت ہے۔ مداخلت کے اثرات کے بارے میں استدلال کرنا۔ یہ جاننا ضروری ہے کہ مداخلت صورت حال کو بہتر بناتی ہے، یا کم از کم صورت حال کو بدتر نہیں بناتی۔ ایکشن انٹرفیس۔ نگرانی کے آلات کی طرح، ہمیں نظام کو عمل کی دعوتوں کو حاصل کرنے کے قابل بنانے کی ضرورت ہے۔ دعوت کے طریقہ کار کا انحصار لازمی طور پر نظام کے نفاذ کی تفصیلات پر ہوگا۔ تاہم، تفصیلات کی سطح پر، ہمیں صارف کو سسٹم کو فیڈ بیک فراہم کرنے کا ایک اعلانیہ طریقہ فراہم کرنے کی ضرورت ہے جس میں یہ واضح کیا جائے کہ کن حالات میں کن اقدامات کا اطلاق کیا جانا چاہیے۔ متعلقہ کام پہلو پر مبنی پروگرامنگ رن ٹائم تصدیق میں محققین نے پہلو پر مبنی پروگرامنگ کو ماڈیولر طریقے سے پروگرام کے آلات کی وضاحت کے لیے ایک تکنیک کے طور پر استعمال کرنے کی صلاحیت کو تسلیم کیا۔ پہلو پر مبنی پروگرامنگ (اے او پی) عام طور پر کراس کٹنگ کے خدشات کی ماڈیولرائزیشن کو فروغ دیتا ہے۔ رن ٹائم تصدیق قدرتی طور پر ایسی ہی ایک تشویش ہے اور اس لیے اے او پی کی کچھ خصوصیات سے فائدہ اٹھا سکتی ہے۔ پہلو پر مبنی مانیٹر کی تعریفیں بڑی حد تک اعلانیہ ہوتی ہیں، اور اس لیے لازمی پروگرامنگ زبان میں لکھے گئے پروگرام کی تبدیلی کے ذریعے اظہار کردہ آلات کے مقابلے میں استدلال کرنا آسان ہوتا ہے۔ مزید برآں، جامد تجزیے پروگرام کے آلات کی دیگر شکلوں کے مقابلے میں نگرانی کے پہلوؤں کے بارے میں زیادہ آسانی سے استدلال کر سکتے ہیں، کیونکہ تمام آلات ایک ہی پہلو میں موجود ہیں۔ بہت سے موجودہ رن ٹائم تصدیقی ٹولز اس لیے تفصیلات مرتب کرنے والوں کی شکل میں بنائے گئے ہیں، جو ایک اظہار خیال اعلی سطح کی تفصیلات کو ان پٹ کے طور پر لیتے ہیں اور کچھ پہلو پر مبنی پروگرامنگ زبان (جیسے پہلو جے) میں لکھے گئے آؤٹ پٹ کوڈ کے طور پر تیار کرتے ہیں۔ رسمی تصدیق کے ساتھ امتزاج رن ٹائم تصدیق، اگر ثابت درست ریکوری کوڈ کے ساتھ مل کر استعمال کیا جائے تو، پروگرام کی تصدیق کے لیے ایک انمول بنیادی ڈھانچہ فراہم کر سکتا ہے، جو مؤخر الذکر کی پیچیدگی کو نمایاں طور پر کم کر سکتا ہے۔ مثال کے طور پر، ہیپ قسم الگورتھم کی باضابطہ طور پر تصدیق کرنا بہت مشکل ہے۔ اس کی تصدیق کرنے کے لیے ایک کم مشکل تکنیک یہ ہے کہ اس کے آؤٹ پٹ کو ترتیب دینے کی نگرانی کی جائے (ایک لکیری پیچیدگی مانیٹر) اور، اگر ترتیب نہیں دی گئی ہے، تو اسے آسانی سے قابل تصدیق طریقہ کار کا استعمال کرتے ہوئے ترتیب دیں، جیسے کہ اندراج کی ترتیب۔ نتیجے میں چھانٹنے کا پروگرام اب زیادہ آسانی سے قابل تصدیق ہے، ڈھیر کی قسم سے صرف ایک چیز درکار ہوتی ہے کہ وہ ملٹی سیٹ سمجھے جانے والے اصل عناصر کو تباہ نہ کرے، جسے ثابت کرنا بہت آسان ہے۔ دوسری سمت سے دیکھتے ہوئے، کوئی بھی رن ٹائم تصدیق کے اوور ہیڈ کو کم کرنے کے لیے رسمی تصدیق کا استعمال کر سکتا ہے، جیسا کہ رسمی تصدیق کے بجائے جامد تجزیہ کے لیے پہلے ہی ذکر کیا گیا ہے۔ درحقیقت، کوئی بھی مکمل طور پر تصدیق شدہ رن ٹائم کے ساتھ شروع کر سکتا ہے، لیکن شاید سست پروگرام۔ پھر کوئی بھی مانیٹر کو خارج کرنے کے لیے رسمی تصدیق (یا جامد تجزیہ) کا استعمال کر سکتا ہے، اسی طرح ایک مرتب قسم کی درستگی یا میموری کی حفاظت کے رن ٹائم چیک کو خارج کرنے کے لیے جامد تجزیہ کا استعمال کرتا ہے۔ زیادہ روایتی تصدیق کے طریقوں کے مقابلے میں، رن ٹائم تصدیق کا ایک فوری نقصان اس کی کم کوریج ہے۔ جب رن ٹائم مانیٹر سسٹم کے ساتھ تعینات کیے جاتے ہیں تو یہ پریشانی کا باعث نہیں ہوتا ہے (پراپرٹی کی خلاف ورزی ہونے پر مناسب ریکوری کوڈ کے ساتھ مل کر عمل میں لایا جاتا ہے)، لیکن جب سسٹم میں غلطیاں تلاش کرنے کے لیے استعمال کیا جاتا ہے تو یہ رن ٹائم تصدیق کی تاثیر کو محدود کر سکتا ہے۔ غلطی کا پتہ لگانے کے مقاصد کے لیے رن ٹائم تصدیق کی کوریج کو بڑھانے کی تکنیکوں میں شامل ہیں: ان پٹ جنریشن۔ یہ اچھی طرح سے جانا جاتا ہے کہ ان پٹ کا ایک اچھا سیٹ تیار کرنا (پروگرام ان پٹ متغیر اقدار، سسٹم کال اقدار، تھریڈ شیڈول وغیرہ)۔ جانچ کی تاثیر میں بہت زیادہ اضافہ کر سکتا ہے۔ یہ غلطی کا پتہ لگانے کے لیے استعمال ہونے والی رن ٹائم تصدیق کے لیے بھی درست ہے، لیکن ان پٹ جنریشن کے عمل کو چلانے کے لیے پروگرام کوڈ کو استعمال کرنے کے علاوہ، رن ٹائم تصدیق میں کوئی بھی پراپرٹی کی وضاحتیں بھی استعمال کر سکتا ہے، جب دستیاب ہو، اور مطلوبہ طرز عمل کو متاثر کرنے کے لیے نگرانی کی تکنیک بھی استعمال کر سکتا ہے۔ رن ٹائم تصدیق کا یہ استعمال اسے ماڈل پر مبنی جانچ سے قریب سے متعلق بناتا ہے، حالانکہ رن ٹائم تصدیق کی وضاحتیں عام طور پر عام مقصد کے لیے ہوتی ہیں، ضروری نہیں کہ جانچ کی وجوہات کے لیے تیار کی گئی ہوں۔ مثال کے طور پر، اس بات پر غور کریں کہ کوئی اوپر دی گئی عام مقصد کی UnsafeEnum پراپرٹی کی جانچ کرنا چاہتا ہے۔ سسٹم کے نفاذ کا غیر فعال طور پر مشاہدہ کرنے کے لیے صرف مذکورہ بالا مانیٹر تیار کرنے کے بجائے، کوئی بھی ایک ہوشیار مانیٹر تیار کر سکتا ہے جو دوسرے e.nextElement () ایونٹ کو پیدا کرنے کی کوشش کرنے والے تھریڈ کو منجمد کر دیتا ہے (اس کے پیدا ہونے سے ٹھیک پہلے)، دوسرے تھریڈز کو اس امید پر چلانے دیتا ہے کہ ان میں سے ایک v.update () ایونٹ پیدا کر سکتا ہے، ایسی صورت میں ایک غلطی پائی گئی ہے۔ متحرک علامتی عمل درآمد۔ علامتی عمل میں پروگراموں کو علامتی طور پر انجام دیا جاتا ہے اور ان کی نگرانی کی جاتی ہے، یعنی ٹھوس ان پٹ کے بغیر۔ نظام کا ایک علامتی نفاذ ٹھوس ان پٹ کے ایک بڑے سیٹ کا احاطہ کر سکتا ہے۔ آف دی شیلف رکاوٹ کو حل کرنے یا اطمینان بخش جانچ کی تکنیکیں اکثر علامتی سزائے موت کو چلانے یا ان کی جگہ کو منظم طریقے سے تلاش کرنے کے لیے استعمال کی جاتی ہیں۔ جب بنیادی اطمینان بخش چیکرس کسی چوائس پوائنٹ کو سنبھال نہیں سکتے ہیں، تو اس پوائنٹ کو پاس کرنے کے لیے ایک ٹھوس ان پٹ تیار کیا جا سکتا ہے۔ ٹھوس اور علامتی عمل کے اس امتزاج کو کانکولک ایگزیکیوشن بھی کہا جاتا ہے۔ متحرک پروگرام تجزیہ پروفائلنگ (کمپیوٹر پروگرامنگ) رن ٹائم ایرر ڈٹیکشن رن ٹائم ایپلی کیشن سیلف پروٹیکشن (آر اے ایس پی) حوالہ جات رسمی طریقے کمپیوٹر سائنس میں منطق