סמנטיקה

חשוב שנדע להבדיל בין סינתקס של שפה לבין שמייצג את המבנה של השפה, סדר מילים וסימנים והרכבת משפטים שמהווים תוכנית מבחינת נכונות שלהם בסדר המילים.
הסמנטיקה היא המשמעות של אותם המילים, מה הן אומרות מבחינת התוכנית שלנו.

למשל נסתכל על הקוד הבא:

מבחינת ניתוח סינתקס של התוכנית נוכל להבין שיש כאן 3 הצהרות (לפי ההפרדה של התו ;). כל אחת מהן מכילה משתנה בצד אחד עם אופרטור = ולאחר מכן מה שנראה כ expression שהוא בעצמו משתנה.

הסמנטיקה מתעסקת עם המשמעות הדקדוקית והנכונות הדקדוקית של תוכניות. כלומר, הסמנטיקה תבין שהמשמעות של התוכנית היא החלפת הערכים $x,y$ תוך השמה של $z$ להיות הערך הסופי של $y$.

ישנם מספר דרכים לפרמל את ההצהרה הנ״ל בגדול יש 3 דרכים עיקריות
- סמנטיקה תפעולית (Operational Semantic): המשמעות של מבנה מוגדרת על ידי החישוב שלו כאשר הוא מורץ על ידי מחשב.
- _סמנטיקה דנוטציונית משמעויות מעוצבות על ידי אובייקטים מתמטיים המייצגים את ההשפעה של ביצוע המבנים (למשל על ידי פונקציות).
- סמנטיקה אקסיומטית: מושפעת מ assertions. התוכנית יכולה להיות נכונה באופן חלקי אבל מוסיפים לה תכונות של preconditions ו postconditions כך שאם התוכנית מסתיימת אנחנו יודעים שהתנאים האלו התקיימו וקיבלנו תוצאה רצויה.

שפת while

שפה אימפרטיבית פשוטה שעוזרת להדגים ולהסביר עקרונות סמנטיים כפי שציינו למעלה.
התחביר האבסטרקטי של while מחולק לקטגוריות הבאות
- Num- קבוצת המספרים השלמים
- Var- קבוצת המשתנים
- Aexp- קבוצת הביטויים האריתמטיים
- ${\mathrm{\forall }}_{n\in Num}:n\in Aexp$
- ${\mathrm{\forall }}_{x\in Var}:x\in Aexp$
- ${\mathrm{\forall }}_{a_1,a_2\in Aexp}:a_1+a_2,a_1-a_2,a_1\cdot a_2\in Aexp$
- Bexp- קבוצת המשתנים הבוליאנים נגדיר ביטוי בוליאני להיות $b::=true|false|a_1=a_2|a_1\le a_2|\mathrm{\neg }b|b_1\wedge b_2$
- Stm- קבוצת הפקודות
- אם $x\in Var$ ו $a\in Aexp$ אז $x:=a\in Stm$
- $skip\in Stm$
- ${\mathrm{\forall }}_{S_1,S_2\in Stm}:S_1;S_2\in Stm$
- if b then S1 else S2.
- while b do S
הערה: בזכות הסעיף השלישי Stm זאת קבוצת התוכניות.

חשוב לשים לב שזהו סינתקס אבל את הסמנטיקה אנחנו יכולים לקבוע, למשל יכלנו לקבוע ש $n::=0|1|n0|n1$ כלומר $n$ הוא מחרוזות המספרים הבינאריים. מגדירים זאת באמצעות פונקציות סמנטיות ובמקרה של מספרים $N:Num\to Z$.

AST

התחביר האבסטרקטי מתאר איך לבנות expressions בשפה מבלי לרדת לפרטים של keywords , הזחות וכו׳. מתחביר אבסטרקטי אפשר לבנות Abstract Syntax Trees שמייצג את המבנה הבסיסי ביותר של התוכנית. אפשר לבנות אותו מבלי לבדוק כל פרט שרלוונטי ל concrete syntax אם כי יכול להיות מצב שיווצרו לנו שתי AST מאותה תוכנית והסינתקס הקונקרטי יצטרך להכריע.

בגלל שלא נרצה לכתוב עצי סינתקס לכל תוכנית (ראו איך התוכנית הבסיסית הנ״ל יצרה עץ די גדול יחסית) נרצה לייצג אותם באמצעות תחביר ליניארי לשם כך נשתמש ב סוגריים. למשל

יבטא את העץ השמאלי בתמונה ו

יבטא את העץ הימני.

לדוגמה, נבנה עת סינתקס עבור התוכנית הבאה:

y:=1;
while not(x=1) do (
	y:=y*x;
	x:=x-1;
)

Semantic Functions

בסופו של דבר הסינתקס האבסטרקטי מורכב מexpressions אבל המשמעות של ביטוי כזה נקבע לפי הערך של המשתנים שנמצאים בתוך הביטוי הזה.

לשם כך נגדיר states שזאת תהיה פונקציה ממשתנה לערך שלו

אם $s$ הוא מצב ו $x$ הוא משתנה נסמן את $s(x)$ כ $sx$ . נשים לב שבגלל שאנחנו מגדירים את זה כפונקציה אנחנו בהכרח כופים על כל משתנה לקבל ערך אחד מהגדרה ח״ע.

סמנטיקה של ביטויים אריתמטיים:
כעת, בהינתן ביטוי אריתמטי $a$ ומצב $s$ נוכל כעת לקבוע את הערך של הביטוי.
נגדיר פונקציה שלמה $A:Aexp\to (State\to Num)$ באופן הבא:

a) ${\mathrm{\forall }}_{n\in Num}:A[n]s=n$
b) ${\mathrm{\forall }}_{x\in Var}:A[x]s=sx$
c) $A[a_1+a_2]s=A[a_1]s+A[a_2]s$
d) כפל וחיסור דומה לסעיף הקודם.

נשים לב להבדלה בין הסימנים בצד שמאל ולסימנים האריתמטיים בצד ימין. צד שמאל הם סימנים של חלק מהסינתקס האבסטרקטי ובצד ימין זה ביטויים אריתמטיים כפי שאנחנו מכירים.

דוגמה:
נניח שיש מצב $x$ המקיים $sx=3$ . נחשב את $A[x+1]s$. לפי הכללים הנ״ל מתקיים $A[x+1]s=A[x]s+A[1]s=s(x)+1=3+1=4$ .

סמנטיקה של ביטויים בוליאנים:
נגדיר אותה כפונקציה $B:Bexp\to (s\to \{tt,ff\})$ על ידי:
a) $B[false]s=ff$
b) $B[true]s=tt$
c) $B[a_1=a_2]s=\{\begin{array}{ll}tt& A[a_1]s=A[a_2]s\\ ff& else\end{array}$
d) $B[a_1\le a_2]s=\{\begin{array}{ll}tt& A[a_1]s\le A[a_2]s\\ ff& else\end{array}$
e) $B[\mathrm{\neg }b]s=\{\begin{array}{ll}tt& B[b]s=ff\\ ff& else\end{array}$
f) $B[b_1\wedge b_2]s=\{\begin{array}{ll}tt& B[b_1]s=ttandB[b_2]s=tt\\ ff& else\end{array}$

Natural Semantic

סמנטיקה טבעית היא אחת הדרכים לתאר סמנטיקה של פקודות. בסמנטיקה של פעולות אנחנו מתעניינים בשינויי המצבים במהלך הרצה של תוכנית. הסמנטיקה הטבעית שמה בחשיבות עליונה את התוצאה הסופית של הריצה של התוכנית שלנו ואיך תוצאה זאת מושגת.

המטרה של statements ב while זה לשנות את הstates. למשל אם $x=3$ במצב $s$ ואנחנו מריצים את הפקודה $x:=x+1$ אז אנחנו מקבלים מצב חדש שבו $x=4$ . לכן, בעוד שסמנטיקה של ביטויים אריתמטיים ובוליאניים רק משקיפה על הstate ומאפשרת לנו לחשב אותו , הסמנטיקה של פעולות גם תשנה את הstate הזה. בסמנטיקה תפעולית (ובפרט גם טבעית) החשיבות היא גם על איך התוכנית רצה ולא רק התוצאות של הריצה. ליתר דיוק, העניין הוא סביב כיצד המצבים משתנים במהלך ריצת התוכנית.

בסמנטיקה טבעית מתעניינים בקשר בין המצב ההתחלתי של תוכנית למצב הסופי שלה.

נגדיר כמה כללים של סמנטיקה של פקודות (Operational Semantic)
יהי $s$ מצב , $y$ משתנה ו $v$ מספר, המצב $s[y\mapsto v]$ יוגדר על ידי :

המשמעות הסמנטית היא כאשר המשתנה $y$ ממופה לערך $v$ מה יהיה הפלט של הפונקציה $sx$

זה מבוסס על עקרון ההחלפה. זה בעצם $s$ רק ש $y$ כבול לערך $v$.

הסמנטיקה התפעולית מבוססת על היגדים מהצורה $⟨S,s⟩\to s^{\prime }$ האינטואיציה של זה היא שכאשר אנחנו במצב $s$ מפעילים את הפקודה $S$ ועוברים למצב $s^{\prime }$ .

נגדיר מספר כללי היסק עבור היחס $\to$ :

נוכל להוסיף כללים חדשים לסמנטיקה שלנו, למשל נגדיר if(x:=e) then S1 else S2 ככלל חדש ונוכל לכלול אותו בסמנטיקה שלנו כך :

נוסיף כלל נוסף גם case(b1:S1),(b2:S2),(else:S3)

לחוק (כפי שרשום למעלה) יש את התצורה הכללית :

כאשר $S_1,\dots S_n$ הם מרכיבים מידיים של $S$ או שהם פקודות שנוצרות מרכיבים מידיים של $S$.
לכלל יש הנחות (מה שרשום מעל הקו) ומסקנה אחת (מתחת לקו) כמו כן יכול להיות לכללים גם תנאים בוליאנים. אפשר להסתכל על החלק העליון כגזירה של החלק התחתון. בעצם  if, while, comp הם כללי גזירה ו ass, skip הם אקסיומות.

כללים ללא הנחות נקראים אקסיומות למשל $ass$ .

עצי גזירה

נגדיר את עץ הגזירה של $⟨S,s⟩\to s^{\prime }$ הוא עץ ששורשו הוא $⟨S,s⟩\to s^{\prime }$ העלים הם אקסיומות וכל קודקוד הוא מסקנה מילדיו לפי אחד מכללי הגזירה.

עצים גזירה מציירים כאשר השורש למטה.

הגדרה: ההיגד $⟨S,s⟩\to s^{\prime }$ מתקיים אם יש עץ גזירה ששורשו הוא $⟨S,s⟩\to s^{\prime }$.
נסתכל על הדוגמה הבאה:

יהי $s_0$ מצב כך ש $s_{0}x=5$ ו $s_{0}y=7$ .נסמן $s_1:s_0[z\mapsto 5],s_2:s_1[x\mapsto 7],s_3:s_2[y\mapsto 5]$ נסתכל על הפקודה הבאה

נרצה להראות שזאת תוביל אותנו ל $s_3$ .
נבנה עץ גזירה

משפט: אם $<S,s>\to s^{\prime }$ אז עבור $s^{\prime \prime }$ מתקיים שאם $<S,s>\to s^{\prime \prime }$ אז $s^{\prime }=s^{\prime \prime }$ .

הוכחה:
אפשר לעשות את זה ב אינדוקציה על מבנה עץ הגזירה של $<S,s>\to s^{\prime }$ .

בסיס: נבדוק על כל אחת מהאקסיומות.
a) אם הגזירה הנ״ל מובילה אותנו ל skip לאחר הפעלה יחידה, זה אומר ש $S=skip$ ולכן זה אומר $s^{\prime }=s$. כיוון ש $S=skip$ אז אם נניח $<S,s>\to s^{\prime \prime }$ נקבל $<skip,s>\to s^{\prime \prime }=s=s^{\prime }$ כדרוש.

b) אם $<S,s>\to s^{\prime }$ נגזר על ידי עץ הגזירה עם הפעלה יחידה של כלל ass. במקרה זה $S$ חייבת להיות מהצורה $x:=a$ ולכן מתקיים $s^{\prime }=s[x\mapsto A[a]s]$. כעת אם נניח ש $<S,s>\to s^{\prime \prime }$ נקבל באותה צורה $s^{\prime \prime }=s[x\mapsto A[a]s]=s^{\prime }$ כדרוש.

נשים לב ש $skip$ ו $whil{e}^{ff}$ דומים זה יוצא אותה הוכחה.

צעד 1:
ל $<S,S>\to s^{\prime }$ יש עץ גזירה שבו הכלל האחרון שהופעל הוא $Comp$ אז העץ הוא

עבור $s_0$ כלשהו.

כלומר קיימים $S_1;S_2$ כך ש $S=S_1;S_2$

כעת נניח ש $<S,s>\to s^{\prime \prime }$ עץ הגזירה ייראה כך

עבור $s_1$ כלשהו.

מהנחת האינדוקציה נוכל להסיק ש כיוון ש $<S_1,s>\to s_1$ וגם $<S_1,s>\to s_0$ אז $s_0=s_1$ ולכן $<S_2,s_{1,0}>\to s^{\prime \prime }=s^{\prime }$ כדרוש.

נשים לב שההנחה היא רק על עץ הגזירה הראשונה ולא השני.
יתר הכללים עובדים בצורה דומה.

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

לסיכום:
כדי להוכיח שמתקיימת תכונה מסוימת על סמנטיקה נשתמש באינדוקציה על צורת העץ כאשר הבסיס הוא התכונה המתקימת על האקסיומות ובצעד האינדוקציה לכל כלל גזירה נניח שמתקיימת התכונה ונוכיח למסקנה של הגזירה שהתכונה מתקיימת.

הוכחת שקילות סמנטית

נרצה להראות שקילות סמנטית בין שני קטעי קוד בשפת while
while b do S ~ if b then (S; while b do S) else skip

לשם כך נצטרך להוכיח את שתי הטענות הבאות :

מזכיר הוכחה של שיוויון על ידי הכלה דו כיוונית. נרצה להראות שאם אחד נגזר למצב $s^{\prime \prime }$ אז גם השני נגזר לאותו מצב.

נעשה כיוון אחד, הכיוון השני דומה. מתקיים אם כן, $<whilebdoS,s>\to s^{\prime \prime }$ אזי, ישנו עץ גזירה $T$ שגוזר את הכלל הזה. נחלק למקרים:

a) אם $B[b]s=tt$ במקרה זה עץ הגזירה נראה מהצורה

כאשר $T_1=<S,s>\to s^{\prime }$ ו $T_2$ הוא מהצורה $<\text{while b do S, }{s}^{\prime }>\to s^{\prime \prime }$.

נוכל לבצע comp על T1,T2 ונקבל :

כעת בגלל ש$b=tt$ נוכל להשתמש בכלל $i{f}^{tt}$ ונקבל

שמנו skip כי אין לו חשיבות כיוון ש $b$ הוא תמיד true.

b) כאשר $B[b]=ff$ העץ גזירה הוא מהצורה $<\text{while b do S, s}>\to s$  
במצב זה אנחנו נשארים באותו מצב ולכן נגדיר $s=s^{\prime \prime }$ . נוכל לנצל זאת כדי להשתמש ב $\text{<skip, s>}\to s$ ונשתמש בזה ובכלל $i{f}^{ff}$ כדי לגזור מהכלל הזה את $\text{<if b then S1 else S2,s>}\to s^{\prime }$ כדי לקבל

ֿ