Predicative programming
پیشن گوئی پروگرامنگ پروگرام کی تفصیلات اور اصلاح کے لیے ایک رسمی طریقہ کار کا اصل نام ہے، جسے حال ہی میں پروگرامنگ کا عملی نظریہ کہا جاتا ہے، جسے ایرک ہیہنر نے ایجاد کیا تھا۔ مرکزی خیال یہ ہے کہ ہر وضاحت ایک بائنری (بولین) اظہار ہے جو کمپیوٹر کے قابل قبول طرز عمل کے بارے میں درست ہے اور ناقابل قبول طرز عمل کے بارے میں غلط ہے۔ اس سے پتہ چلتا ہے کہ اصلاح صرف مضمر ہے۔ یہ سب سے آسان رسمی طریقہ ہے، اور سب سے عام، ترتیب وار، متوازی، اسٹینڈ اکیلے، بات چیت کرنے، ختم کرنے، غیر ختم کرنے، قدرتی وقت، حقیقی وقت، تعیناتی، اور ممکنہ پروگراموں پر لاگو ہوتا ہے، اور اس میں وقت اور جگہ کی حدود شامل ہیں۔ پروگرامنگ زبان میں کمانڈوں کو تفصیلات کا ایک خاص معاملہ سمجھا جاتا ہے-وہ وضاحتیں جو مرتب کی جا سکتی ہیں۔ مثال کے طور پر، اگر پروگرام متغیر ہیں، اور، کمانڈ: = + 1 تفصیلات کے مساوی ہے (بائنری اظہار) = + 1 ¥ = ¥ = جس میں، اور تفویض سے پہلے پروگرام متغیرات کی اقدار کی نمائندگی کرتا ہے، اور، اور تفویض کے بعد پروگرام متغیرات کی اقدار کی نمائندگی کرتا ہے۔ اگر وضاحت> ہے، تو ہم آسانی سے ثابت کرتے ہیں (: = + 1) ⇒ (>)، جو کہتا ہے کہ: = + 1 کا مطلب ہے، یا بہتر کرتا ہے، یا لاگو کرتا ہے>۔ لوپ پروف بہت آسان ہیں۔ مثال کے طور پر، اگر ایک انٹیجر متغیر ہے، یہ ثابت کرنے کے لیے کہ جب کہ> 0 کرو: =-1 od کو بہتر بناتا ہے، یا تفصیلات کو لاگو کرتا ہے، تو ثابت کریں کہ اگر> 0 تو: =-1 ؛ (≤0 ियम = 0) ورنہ فائی ν (≤0 ν = 0) جہاں = (=) خالی ہے، یا کچھ نہ کرنے والی کمانڈ ہے۔ لوپ غیر متغیر یا کم سے کم فکسڈ پوائنٹ کی ضرورت نہیں ہے۔ متعدد انٹرمیڈیٹ اتلی اور گہرے اخراج والے لوپس اسی طرح کام کرتے ہیں۔ ثبوت کی یہ آسان شکل ممکن ہے کیونکہ پروگرام کمانڈز اور وضاحتیں معنی خیز طور پر ایک ساتھ ملایا جا سکتا ہے۔ پھانسی کا وقت (اوپری حدود، نچلی حدود، عین وقت) اسی طرح ثابت کیا جا سکتا ہے، صرف وقت متغیر کو متعارف کروا کر۔ منسوخی کو ثابت کرنے کے لیے ثابت کریں کہ پھانسی کا وقت محدود ہے۔ عدم خاتمے کو ثابت کرنے کے لیے ثابت کریں کہ پھانسی کا وقت لامحدود ہے۔ مثال کے طور پر، اگر وقت متغیر ہے، اور وقت کو تکرار کی گنتی کے ذریعے ماپا جاتا ہے، تو یہ ثابت کرنے کے لیے کہ پچھلے وہیل لوپ کے نفاذ میں وقت لگتا ہے جب ابتدائی طور پر غیر منفی ہوتا ہے، اور جب ابتدائی طور پر منفی ہوتا ہے تو ہمیشہ کے لیے وقت لگتا ہے، ثابت کریں کہ اگر> 0 تو: =-1 ؛: = + 1 ؛ (≤0 * = +) ≤ (<0 * = ≤) ورنہ ≤ (≤0 * = +) ≤ (<0 * = ≤) جہاں = (= ≤ =)۔ کتابچہ ای۔ سی۔ آر ہیہنر، پروگرامنگ کا ایک عملی نظریہ، سپرنگر-ورلاگ 1993۔ پریکٹیکل تھیوری آف پروگرامنگ کا حالیہ ایڈیشن آن لائن۔ بیرونی روابط اشاعت بذریعہ ایرک ہیہنر۔ رسمی طریقے رسمی تفصیلات کی زبانیں منطقی حساب کتاب