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

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

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

3.3.2. דוגמא למצב בעייתי

מפרט: "בסוף התוכנית ערכו של x כפול מערכו בהתחלה".

;

כתיבה שגויה למפרט: plot:$ < true,x = 2x > $ הביטוי אינו נכון מתמטית. לא ניתן להגיד ש-plot:$x = 2x$ (זו לא שפת תכנות אלא מתמטיקה).

שימוש במשתנה חדש: ביטוי נכון ניתן לכתוב באמצעות משתנה חדש y: plot:$ < y = x,x = 2y > $. לדוגמא: plot:$\left\{ {y = x} \right\}P\left\{ {x = 2y} \right\}$

משתנה לוגי הינו משתנה שאינו מופיע בתוכנית, ולכן אינו משנה את ערכו במהלך התוכנית.

נכתוב את הדוגמא כך: plot:$ < x = X,x = 2 \cdot X > $.

מוסכמה: משתנה לוגי עבור המשתנה plot:$x$ יסומן ב-plot:$X$, משתנה לוגי עבור plot:$y$ יסומן ב-plot:$Y$ וכו'.

הסימון plot:$\bar x$ - אוסף המשתנים של התוכנית, יכלול הן את משתני התוכנית והן את המשתנים הלוגיים.



תגיות המסמך:

לפרק הקודם3.3.1. הגדרה
לפרק הבא3.4. תכונה של תוכנית - נכונות מלאה
אין תגובות!
שיתוף:
| עוד