Unifying Theories of Programming
کمپیوٹر سائنس میں یونیفائنگ تھیوریز آف پروگرامنگ (یو ٹی پی) پروگرام سیمنٹکس سے متعلق ہے۔ یہ ظاہر کرتا ہے کہ کس طرح ڈینوٹیشنل سیمنٹکس، آپریشنل سیمنٹکس اور الجبرائی سیمنٹکس کو پروگراموں اور کمپیوٹر سسٹمز کی رسمی تفصیلات، ڈیزائن اور نفاذ کے لیے ایک متحد فریم ورک میں جوڑا جا سکتا ہے۔ سی اے آر کی اس عنوان کی کتاب۔ ہور اور ہی جیفینگ 1998 میں کمپیوٹر سائنس میں پرینٹس ہال انٹرنیشنل سیریز میں شائع ہوا تھا اور اب یہ ویب پر مفت دستیاب ہے۔ نظریہ یو ٹی پی کی بامعنی بنیاد فرسٹ آرڈر پریڈیکیٹ کیلکولس ہے، جو سیکنڈ آرڈر منطق سے فکسڈ پوائنٹ کنسٹرکٹس کے ساتھ بڑھا ہوا ہے۔ ایرک ہینر کی روایت کی پیروی کرتے ہوئے، یو ٹی پی میں پروگرام پیش گوئی کرتے ہیں، اور سیمنٹک سطح پر پروگراموں اور وضاحتیں کے درمیان کوئی فرق نہیں ہے۔ ہور کے الفاظ میں: ایک کمپیوٹر پروگرام کی شناخت سب سے مضبوط پیش گوئی کے ساتھ کی جاتی ہے جو اس پروگرام کو انجام دینے والے کمپیوٹر کے رویے سے متعلق ہر متعلقہ مشاہدے کو بیان کرتی ہے۔ یو ٹی پی کی بول چال میں، ایک نظریہ ایک مخصوص پروگرامنگ پیراڈائم کا نمونہ ہے۔ یو ٹی پی تھیوری تین اجزاء پر مشتمل ہوتی ہے: ایک حروف تہجی، جو متغیر ناموں کا ایک مجموعہ ہے جو نمونے کی صفات کی نشاندہی کرتا ہے جس کا مشاہدہ کسی بیرونی وجود کے ذریعہ کیا جاسکتا ہے۔ ایک دستخط، جو پروگرامنگ زبان کا مجموعہ ہے جو نمونے کے لیے اندرونی تعمیر کرتا ہے۔ اور صحت مند حالات کا مجموعہ، جو نمونے کے اندر فٹ ہونے والے پروگراموں کی جگہ کی وضاحت کرتا ہے۔ صحت کے ان حالات کو عام طور پر مونوٹونک آئیڈیمپوٹینٹ پریڈیکیٹ ٹرانسفارمرز کے طور پر ظاہر کیا جاتا ہے۔ یو ٹی پی میں پروگرام کی اصلاح ایک اہم تصور ہے۔ کسی پروگرام کو صرف اس صورت میں بہتر بنایا جاتا ہے جب ہر مشاہدہ جس سے بنایا جا سکتا ہے وہ بھی اس کا مشاہدہ ہو۔ ریفائنمنٹ کی تعریف یو ٹی پی کے نظریات میں عام ہے: جہاں حروف تہجی کے تمام متغیرات کی عالمگیر بندش کی نشاندہی ہوتی ہے۔ تعلقات سب سے بنیادی یو ٹی پی تھیوری حروف تہجی کی پیش گوئی کیلکولس ہے، جس میں حروف تہجی کی کوئی پابندیاں یا صحت کے حالات نہیں ہیں۔ تھیوری آف ریلیشنز قدرے زیادہ مخصوص ہے، کیونکہ کسی رشتے کا حروف تہجی صرف ان پر مشتمل ہو سکتا ہے: غیر تصدیق شدہ متغیرات ()، اس کے نفاذ کے آغاز میں پروگرام کے مشاہدے کی ماڈلنگ ؛ اور بنیادی متغیرات ()، اس کے نفاذ کے بعد کے مرحلے میں پروگرام کے مشاہدے کی ماڈلنگ۔ کچھ عام زبان کی تعمیرات کو تھیوری آف ریلیشنز میں مندرجہ ذیل طور پر بیان کیا جا سکتا ہے: اسکپ سٹیٹمنٹ، جو کسی بھی طرح سے پروگرام کی حالت کو تبدیل نہیں کرتا ہے، کو رشتہ دار شناخت کے طور پر ماڈل کیا جاتا ہے: متغیر کو قدر کی تفویض کو ترتیب دینے اور دیگر تمام متغیرات کو مستقل رکھنے کے طور پر ماڈل کیا جاتا ہے: دو پروگراموں کی ترتیب وار ترکیب صرف انٹرمیڈیٹ اسٹیٹ کی رشتہ دار ساخت ہے: پروگراموں کے درمیان غیر متعین انتخاب ان کی سب سے بڑی نچلی حد ہے: پروگراموں کے درمیان مشروط انتخاب انفکس نوٹیشن کا استعمال کرتے ہوئے لکھا جاتا ہے: تکرار کے لیے ایک سیمنٹکس ایک مونوٹونک پریڈیکیٹ ٹرانسفارمر کے کم سے کم فکسڈ پوائنٹ کے ذریعے دیا جاتا ہے: حوالہ جات مزید پڑھنے کے لیے بیرونی روابط یو ٹی پی کی ویب سائٹ یو ٹی پی بک Archive.org 1998 غیر افسانوی کتابوں پر