הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

4.3. למת ההפרדה

לכל תוכנית P ומפרט plot:$ < {q_1},{q_2} > $ מתקיים plot:$ < {q_1} > P < {q_2} > $ (נכונות מלאה) אם ורק אם plot:$ \vDash  < {q_1} > P < true > $ (כל החישובים שמתחילים ב-plot:${q_1}$ עוצרים) וגם plot:$ \vDash \left\{ {{q_1}} \right\}P\left\{ {{q_2}} \right\}$ (נכונות חלקית).

הלמה מאפשרת לנו לפרק הוכחת נכונות מלאה ל-2 הוכחות: 1. עצירה לכל חישוב. 2. נכונות חלקית.



תגיות המסמך:

לפרק הקודם4.2. סמנטיקה
לפרק הבא4.4. שיטת / כללי ההוכחה
אין תגובות!
שיתוף:
| עוד