4.2. סמנטיקההמטרה שלנו: הגדרת חישוב של תוכנית. לצורך כך נגדיר את מושג הקונפיגורציה ואת רלציית המעברים: קונפיגורציה – זוג כאשר תווית המציינת את הצומת בתוכנית בו נמצא החישוב. הינו מצב (השמה למשתנים). משמעות קונפיגורציה: הפקודה שנמצאת בצומת עם התווית מתבצעת ממצב . רלציית המעברים בין קונפיגורציות אמ"מ קיימת קשת מ- ל- בתוכנית ובנוסף מתקיים אחד מהתנאים הבאים:
בנוסף: כאשר ב- יש halt אין מעבר לאף קונפיגורציה אחרת. הארה: רלצית המעברים לוקחת את גרף תרשימי הזרימה ונותנת לנו את היכולת להשתמש בו ככלי לניתוח התוכנית. היא מאפשרת לנו לעשות בו צעדים רק בהתאם לתוכנית עצמה. הגדרת חישוב: חישוב של תוכנית P מקונפיגורציה C מסומן הינו סידרה מקסימלית של קונפיגורציות כך ש- ולכל מתקיים . חישוב סופי תמיד יסתיים בקונפיגורציה עוצרת. קונפיגורציה עוצרת: היא קונפיגורציה עוצרת אם מציינת צומת עצירה בתוכנית. קונפיגורציה התחלתית: היא קונפיגורציה התחלתית אם מציינת את צומת האתחול בתוכנית. עבור חישוב סופי המסתיים בקונפיגורציה (עוצרת) מגדירים את להיות . בהינתן חישוב בתוכנית יש מסלול יחיד שמתאים לו. בהינתן מסלול יכול להיות שאין חישוב שמתאים לו, או לחילופין יכולים להיות אין סוף חישובים מתאימים.
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |