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

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

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

3.4. תכונה של תוכנית - נכונות מלאה

תוכנית P נכונה באופן מלא (Total correctness) אם ורק אם כל חישוב plot:$\pi $ שמתחיל ממצב plot:${\sigma _0}$ שמספק את plot:${q_1}\left( {\bar x} \right)$ עוצר, ומצבו הסופי מספק את plot:${q_2}\left( {\bar x} \right)$.

ניסוח מתמטי: plot:${\sigma _0}| = {q_1}\left( {\bar x} \right) \to Val\left( {\pi \left( {p,{\sigma _0}} \right)} \right)| = {q_2}\left( {\bar x} \right)$

סימון: plot:$ < {q_1} > P < {q_2} > $.

מתקיים: נכונות מלאה plot:$ \Leftarrow $ נכונות חלקית.

הערה: כאשר מביטים בביטוי plot:$\left\langle {{q_1}\left( {\bar x} \right),{q_2}\left( {\bar x} \right)} \right\rangle $ עבור מפרט נתון, plot:$\bar x$ מתייחס לערכי המשתנים בשני זמנים שונים של התוכנית (שני מצבים שונים).



תגיות המסמך:

לפרק הקודם3.3.2. דוגמא למצב בעייתי
לפרק הבא4. תרשימי זרימה – Flowcharts
אין תגובות!
שיתוף:
| עוד