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

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

לדוגמה:

{x == 10}
בזמן (y! = 0):
    y = y - 1
x = 0
{x == 0}

זהו מפרט תקינות חלקי. אם y מאתחל עם מספר כלשהו שווה או גדול מ- 0, S יסתיים ואחרי זה x הוא 0. בעוד שאם y מתחיל במספר שלילי, S תעבור לולאה לנצח ומכיוון שהיא לא תסתיים, לא תגיע למצב ' לאחר הוצאתו להורג של ש '.

אכן, R יכול להיות כל דבר אם S היא לולאה מתה. לדוגמה, לכל שאלה ו- R:

{ש}
בעוד (נכון):
    y = y - 1
{R}

הוא תמיד מפרט תקינות חלקי.

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

למפרט נכונות מוחלטת {Q} S {R}, Q הוא חזק מספיק כדי להבטיח את סיום S, כך שתוכלו להסיק ש- תסתיים והמדינה הסופית מספקת את ר.

לדוגמה:

{x == 10}
בזמן (x! = 0):
    x = x - 1
{x == 0}

הוא מפרט מוחלט של נכונות.

BTW: אני לא בטוח אם התשובה נכונה מכיוון שהשאלה מתויגת עם התקינות הפוליטית. ואילו ההגדרה בשאלה נראית בדיוק זהה למדעי המחשב.