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

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

4.1. הגדרות

תיאור לא פורמלי של הפקודות:

אתחול, start: מציינת את נקודת ההתחלה של התוכנית. לתוכנית ישנה נקודת התחלה יחידה.
הצבה $plot:$\bar x: = \bar e$$ : יהי $plot:$\bar x$$ וקטור משתנים ממשתני התוכנית, בלי חזרות. יהי $plot:$\bar e$$ ווקטור באותו אורך של ביטויים מעל משתני התוכנית, וקבועים. ערכי הביטויים מחושבים לפי המצב הנוכחי, ולאחר מכן מוצבים ל- $plot:$\bar x$$ סימולטנית. דוגמא: יהיה מצב: $plot:$\sigma \left( x \right) = 2,\sigma \left( y \right) = 4$$ , ותהא השמה $plot:$\left( {x,y} \right): = \left( {x + 2,y \cdot x} \right)$$ , אזי מצב התוצאה הוא $plot:$\sigma '\left( x \right) = 4,\sigma '\left( y \right) = 8$$ .
בדיקה $plot:$B\left( {\bar x} \right)$$ : ביטוי בוליאני מעל משתני התוכנית במצב נתון $plot:$\sigma $$ . הביטוי $plot:$\sigma \vDash B$$ מחושב ואנחנו ממשיכים לקשת true/false לפי ערכו של החישוב.
עצירה, halt: נקודת סיום של התוכנית. יכולה להיות יותר מנקודת עצירה אחת.

הגדרה מדוייקת של תרשים זרימה (כגרף):

תכנית P בשפת תרשימי הזרימה PLF הינה גרף סופי מכוון שבצמתיו פקודות. לכל צומת מותאמת תווית המופרדת מהפקודה בנקודותיים. בנוסף על הגרף לספק את המגבלות הבאות: