التفسير التجريدي

البرنامج يدل على الحسابات في بعض عوالم الأشياء. يتكون التفسير التجريدي للبرامج من استخدام ذلك الدلالة لوصف الحسابات في عالم آخر من الأشياء المجردة، بحيث تعطي نتائج التنفيذ المجرد بعض المعلومات عن الحسابات الفعلية. مثال بديهي (نستعيره من Sintzoff 72) هو قاعدة الإشارات. يمكن فهم النص -1515 * 17 للإشارة إلى الحسابات في العالم المجرد (+)، (-)، (±) حيث يتم تعريف دلالات العمليات الحسابية بواسطة قاعدة الإشارات. التنفيذ المجرد -1515 * 17 → - (+) * (+) → (-) * (+) → (-)، يثبت أن -1515 * 17 هو رقم سالب. يهتم التفسير التجريدي ببنية أساسية معينة للعالم المعتاد للحسابات (الإشارة في مثالنا). يعطي ملخصًا لبعض جوانب التنفيذات الفعلية للبرنامج. بشكل عام، هذا الملخص سهل الحصول لكنه غير دقيق (مثلاً -1515 + 17 → - (+) + (+) → (-) + (+) → (±)). على الرغم من نتائجه الناقصة جوهريًا، يسمح التفسير التجريدي للمبرمج أو المترجم بالإجابة على أسئلة لا تحتاج لمعرفة كاملة بتنفيذات البرنامج أو التي تتسامح مع إجابة غير دقيقة (مثلاً إثباتات الصِّحّة الجزئية للبرامج مع تجاهل مشاكل الإنهاء، فحص النوع، تحسينات البرنامج التي لا تُجرى في غياب اليقين حول جدواها، ...).