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

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

5.1.1. שפת תוכניות while

נגדיר את השפה על ידי כלל הגזירה הבא:

$plot:$S:: & x: = e|skip|{S_1};{S_2}|{\text{if }}B{\text{ then }}{S_1}{\text{ else }}{S_2}{\text{ fi}}|{\text{while }}B{\text{ do }}S{\text{ od}}$$

הפעולות:

- הצבה.
- פקודה שאינה עושה דבר. (שימושי למשל בתנאי ה-if הדורשים לפי התחביר else, ולא בכל מקרה נרצה לבצע פעולה במקרה כזה).
$plot:${S_1};{S_2}$$ - שרשור של שתי פקודות אחת אחרי השניה.
$plot:${\text{if }}B{\text{ then }}{S_1}{\text{ else }}{S_2}{\text{ fi}}$$ - משפט תנאי. כל חלקי המשפט הם חובה.
$plot:${\text{while }}B{\text{ do }}S{\text{ od}}$$ - לולאה.

כאשר:

מכיוון ששפת התכנות מודולרית אנחנו יכולים להשתמש במערכת הוכחה מודולרית.

סמנטיקה אופרטיבית של תוכניות while:

$plot:$\sigma $$ הינו מצב התוכנית, פונקציה בין משתני התוכנית לערכיהם.
קונפיגורציה $plot:$C = \left\langle {{S_i},\sigma } \right\rangle $$ כאשר $plot:${S_i}$$ היא תוכנית while, ומתארת את המשך החישוב (בכל רגע $plot:${S_i}$$ היא יתרת התוכנית לביצוע).
עבור הגדרת הסמנטיקה נגדיר תוכנית ריקה E המקיימת: . התוכנית היא תוכנית שאינה עושה דבר – אם נשרשר אותה לפני או אחרי תוכנית אחרת כלשהי, נקבל את אותה תוכנית.
קונפיגורציה עוצרת היא קונפיגורציה מהצורה $plot:$\left\langle {E,\sigma } \right\rangle $$ .