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

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

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

7.2. מערכת ההוכחה H

אקסיומות:

(ASS)                          plot:$\left\{ {p\left[ {x \leftarrow e} \right]} \right\}x: = e\left\{ p \right\}$

(SKIP)                                     plot:$\left\{ p \right\}skip\left\{ p \right\}$

(ARITH)                      plot:$q \to q'$ אמת לוגית

כללי היסק:

)SEQ(                          plot:\[\frac{{\left\{ p \right\}{s_1}\left\{ r \right\}\, & \,\left\{ r \right\}{s_2}\left\{ q \right\}}}{{\left\{ p \right\}{s_1};{s_2}\left\{ q \right\}}}\]

(IF)                              plot:\[\frac{{\left\{ {p \wedge B} \right\}{S_1}\left\{ q \right\}\,\, &  & \,\left\{ {p \wedge \neg B} \right\}{S_2}\left\{ q \right\}}}{{\left\{ p \right\}if\,B\,then\,\,{S_1}\,else\,{S_2}\,\,\,fi\,\,\left\{ q \right\}}}\,\]

(REP)                          plot:\[\frac{{\left\{ {p \wedge B} \right\}S\left\{ p \right\}}}{{\left\{ p \right\}while\,\,B\,\,do\,\,S\,\,\,od\,\left\{ {p \wedge \neg B} \right\}}}\]

(CONS)                      plot:$\frac{{p \to {p_1}\, & \left\{ {{p_1}} \right\}S\left\{ {{q_1}} \right\}\,\, & {q_1} \to q}}{{\left\{ p \right\}S\left\{ q \right\}}}$



תגיות המסמך:

לפרק הקודם7.1. למת החישובים
לפרק הבא7.3. מערכת ההוכחה H*
אין תגובות!
שיתוף:
| עוד