iContract: תכנון לפי חוזה בג'אווה

זה לא יהיה נחמד אם כל שיעורי Java שבהם אתה משתמש, כולל שלך, יעמדו בהבטחותיהם? למעשה, זה לא יהיה נחמד אם באמת הייתם יודעים בדיוק מה מבטיח שיעור נתון? אם אתה מסכים, המשך לקרוא - Design by Contract ו- iContract נחלצים להצלה.

הערה: ניתן להוריד את מקור הקוד לדוגמאות במאמר זה מ- Resources.

תכנון לפי חוזה

טכניקת פיתוח התוכנה Design by Contract (DBC) מבטיחה תוכנה באיכות גבוהה בכך שהיא מבטיחה שכל רכיב במערכת יעמוד בציפיותיו. כמפתח המשתמש ב- DBC, אתה מציין חוזי רכיבים כחלק מממשק הרכיב. החוזה מציין מה רכיב זה מצפה מלקוחות ואילו לקוחות יכולים לצפות ממנו.

ברטרנד מאייר פיתח את DBC כחלק משפת התכנות שלו באייפל. ללא קשר למוצאו, DBC היא טכניקת עיצוב יקרת ערך לכל שפות התכנות, כולל Java.

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

התפיסה המרכזית של DBC קשורה במידה מסוימת #assertלמאקרו בשפת התכנות C ו- C ++. עם זאת DBC לוקח טענות ברמה של זיליון.

ב- DBC אנו מזהים שלושה סוגים שונים של ביטויים:

  • תנאים מוקדמים
  • תנאי פוסט
  • משתנים

בואו נבחן כל אחד בפירוט רב יותר.

תנאים מוקדמים

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

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

תנאי פוסט

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

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

משתנים

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

קביעות, ירושה וממשקים

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

iContract - DBC עם Java

עד כה דיברנו על DBC באופן כללי. כנראה שיש לך מושג עד עכשיו על מה אני מדבר, אבל אם אתה חדש ב- DBC, הדברים עדיין עשויים להיות ערפילים.

בחלק זה הדברים יהיו קונקרטיים יותר. iContract, שפותח על ידי Reto Kamer, מוסיף קונסטרוקציות ל- Java המאפשרות לך לציין את קביעות ה- DBC עליהם דיברנו קודם.

יסודות iContract

iContract הוא מעבד מקדים עבור Java. כדי להשתמש בו, תחילה אתה מעבד את קוד הג'אווה שלך באמצעות iContract, ומייצר קבוצה של קבצי Java מעוטרים. ואז אתה קומפילציה של קוד Java המעוטר כרגיל עם מהדר Java.

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

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

תנאים מוקדמים

ב- iContract, אתה מציב תנאים מוקדמים בכותרת שיטה באמצעות @preההנחיה. הנה דוגמה:

/ ** * @pre f> = 0.0 * / sqrt לצוף sqrt (לצוף f) {...} 

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

הביטוי אחרי ה- @preהוא ביטוי בוליאני של ג'אווה.

תנאי פוסט

כמו כן מתווספים לתגובות הכותרת לתגובת הכותרת של השיטה אליה הם שייכים. ב- iContract, @postההנחיה מגדירה את התנאים הבאים:

/ ** * @pre f> = 0.0 * @post Math.abs ((return * return) - f) <0.001 * / public float sqrt (float f) {...} 

בדוגמה שלנו, הוספנו תנאי לאחר שמבטיח sqrt()שהשיטה מחשבת את השורש הריבועי fבתוך שולי שגיאה ספציפיים (+/- 0.001).

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

בתנאים שלאחר התנאי , לעיתים קרובות קיים צורך להבדיל בין ערך הטיעון לפני ביצוע השיטה ואחר כך, הנתמך ב- iContract עם @preהמפעיל. אם תצרף @preלביטוי בתנאי שלאחר מכן, הוא יוערך על סמך מצב המערכת לפני ביצוע השיטה:

/ ** * הוסף אלמנט לאוסף. * * @post c.size () = [email protected] () + 1 * @post c.contains (o) * / public public void (Collection c, Object o) {...}

בקוד לעיל, התנאי שלאחר מכן מציין שגודל האוסף חייב לצמוח ב -1 כאשר אנו מצרפים אלמנט. הביטוי [email protected]מתייחס לאוסף cלפני ביצוע appendהשיטה.

משתנים

עם iContract, אתה יכול לציין משתנים בתגובת הכותרת של הגדרת הכיתה:

/ ** * מספר חיובי הוא שלם שמובטח שהוא חיובי. * * @inv intValue ()> 0 * / class PositiveInteger מרחיב שלם {...}

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

Object Constraint Language (OCL)

Although the assertion expressions in iContract are valid Java expressions, they are modeled after a subset of the Object Constraints Language (OCL). OCL is one of the standards maintained and coordinated by the Object Management Group, or OMG. (OMG takes care of CORBA and related stuff, in case you miss the connection.) OCL was intended to specify constraints within object modeling tools that support the Unified Modeling Language (UML), another standard guarded by OMG.

Because the iContract expressions language is modeled after OCL, it provides some advanced logical operators beyond Java's own logic operators.

Quantifiers: forall and exists

iContract supports forall and exists quantifiers. The forall quantifier specifies that a condition should hold true for every element in a collection:

/* * @invariant forall IEmployee e in getEmployees() | * getRooms().contains(e.getOffice()) */ 

The above invariant specifies that every employee returned by getEmployees() has an office in the collection of rooms returned by getRooms(). Except for the forall keyword, the syntax is the same as that of an exists expression.

Here is an example using exists:

/** * @post exists IRoom r in getRooms() | r.isAvailable() */ 

That postcondition specifies that after the associated method executes, the collection returned by getRooms() will contain at least one available room. The exists proceeds the Java type of the collection element -- IRoom in the example. r is a variable that refers to any element in the collection. The in keyword is followed by an expression that returns a collection (Enumeration, Array, or Collection). That expression is followed by a vertical bar, followed by a condition involving the element variable, r in the example. Employ the exists quantifier when a condition must hold true for at least one element in a collection.

Both forall and exists can be applied to different kinds of Java collections. They support Enumerations, Arrays, and Collections.

Implications: implies

iContract provides the implies operator to specify constraints of the form, "If A holds, then B must hold as well." We say, "A implies B." Example:

/** * @invariant getRooms().isEmpty() implies getEmployees().isEmpty() // no rooms, no employees */ 

That invariant expresses that when the getRooms() collection is empty, the getEmployees() collection must be empty as well. Note that it does not specify that when getEmployees() is empty, getRooms() must be empty as well.

You can also combine the logical operators just introduced to form complex assertions. Example:

/** * @invariant forall IEmployee e1 in getEmployees() | * forall IEmployee e2 in getEmployees() | * (e1 != e2) implies e1.getOffice() != e2.getOffice() // a single office per employee */ 

Constraints, inheritance, and interfaces

iContract propagates constraints along inheritance and interface implementation relationships between classes and interfaces.

Suppose class B extends class A. Class A defines a set of invariants, preconditions, and postconditions. In that case, the invariants and preconditions of class A apply to class B as well, and methods in class B must satisfy the same postconditions that class A satisfies. You may add more restrictive assertions to class B.

The aforementioned mechanism works for interfaces and implementations as well. Suppose A and B are interfaces and class C implements both. In that case, C is subject to invariants, preconditions, and postconditions of both interfaces, A and B, as well as those defined directly in class C.

Beware of side effects!

iContract will improve the quality of your software by allowing you to catch many possible bugs early on. But you can also shoot yourself in the foot (that is, introduce new bugs) using iContract. That can happen when you invoke functions in your iContract assertions that engender side effects that alter your system's state. That leads to unpredictive behavior because the system will behave differently once you compile your code without iContract instrumentation.

The stack example

Let us take a look at a complete example. I have defined the Stack interface, which defines the familiar operations of my favorite data structure:

/** * @inv !isEmpty() implies top() != null // no null objects are allowed */ public interface Stack { /** * @pre o != null * @post !isEmpty() * @post top() == o */ void push(Object o); /** * @pre !isEmpty() * @post @return == top()@pre */ Object pop(); /** * @pre !isEmpty() */ Object top(); boolean isEmpty(); } 

We provide a simple implementation of the interface:

import java.util.*; /** * @inv isEmpty() implies elements.size() == 0 */ public class StackImpl implements Stack { private final LinkedList elements = new LinkedList(); public void push(Object o) { elements.add(o); } public Object pop() { final Object popped = top(); elements.removeLast(); return popped; } public Object top() { return elements.getLast(); } public boolean isEmpty() { return elements.size() == 0; } } 

As you can see, the Stack implementation does not contain any iContract assertions. Rather, all assertions are made in the interface, meaning that the component contract of the Stack is defined in the interface in its entirety. Just by looking at the Stack interface and its assertions, the Stack's behavior is fully specified.

Now we add a small test program to see iContract in action:

public class StackTest { public static void main(String[] args) { final Stack s = new StackImpl(); s.push("one"); s.pop(); s.push("two"); s.push("three"); s.pop(); s.pop(); s.pop(); // causes an assertion to fail } } 

Next, we run iContract to build the stack example:

java -cp% CLASSPATH%; src; _contract_db; instr com.reliablesystems.iContract.Tool -Z -a -v -minv, pre, post> -b "javac -classpath% CLASSPATH%; src" -c "javac -classpath % CLASSPATH%; instr "> -n" javac -classpath% CLASSPATH%; _ contract_db; instr "-oinstr / @ p / @ f. @ E -k_contract_db / @ p src / *. Java 

ההצהרה לעיל מצדיקה מעט הסבר.