iContract: Reka Bentuk dengan Kontrak di Jawa

Bukankah lebih baik jika semua kelas Java yang anda gunakan, termasuk kelas anda sendiri, menepati janji mereka? Sebenarnya, bukankah lebih baik jika anda benar-benar tahu dengan tepat apa yang dijanjikan kelas tertentu? Sekiranya anda bersetuju, baca terus - Design by Contract dan iContract boleh membantu.

Catatan: Sumber kod untuk contoh dalam artikel ini boleh dimuat turun dari Sumber.

Reka bentuk mengikut Kontrak

Teknik pengembangan perisian Design by Contract (DBC) memastikan perisian berkualiti tinggi dengan menjamin bahawa setiap komponen sistem memenuhi harapannya. Sebagai pembangun yang menggunakan DBC, anda menentukan kontrak komponen sebagai bahagian antara muka komponen. Kontrak tersebut menentukan komponen yang diharapkan oleh pelanggan dan apa yang diharapkan pelanggan terhadapnya.

Bertrand Meyer mengembangkan DBC sebagai sebahagian daripada bahasa pengaturcaraan Eiffelnya. Terlepas dari asalnya, DBC adalah teknik reka bentuk yang berharga untuk semua bahasa pengaturcaraan, termasuk Java.

Pusat DBC adalah pengertian penegasan - ungkapan Boolean mengenai keadaan sistem perisian. Pada waktu runtime, kami menilai penegasan di pusat pemeriksaan tertentu semasa pelaksanaan sistem. Dalam sistem perisian yang sah, semua pernyataan dinilai menjadi benar. Dengan kata lain, jika ada pernyataan yang dinilai salah, kami menganggap sistem perisian tidak sah atau rosak.

Pengertian pusat DBC agak berkaitan dengan #assertmakro dalam bahasa pengaturcaraan C dan C ++. Walau bagaimanapun DBC menegaskan tahap lebih jauh.

Di DBC, kami mengenal pasti tiga jenis ungkapan:

  • Prasyarat
  • Pasca syarat
  • Invarian

Mari kita periksa dengan lebih terperinci.

Prasyarat

Prasyarat menentukan syarat yang mesti ada sebelum kaedah dapat dilaksanakan. Oleh itu, mereka dinilai sebelum kaedah dijalankan. Prasyarat melibatkan keadaan sistem dan argumen diteruskan ke dalam kaedah.

Prasyarat menentukan kewajipan yang mesti dipenuhi oleh pelanggan komponen perisian sebelum boleh menggunakan kaedah komponen tertentu. Sekiranya prasyarat gagal, bug ada pada klien komponen perisian.

Pasca syarat

Sebaliknya, syarat-syarat pasca menentukan syarat yang mesti ada setelah kaedah selesai. Akibatnya, pasca syarat dilaksanakan setelah kaedah selesai. Pasca syarat melibatkan keadaan sistem lama, keadaan sistem baru, argumen kaedah, dan nilai pengembalian kaedah.

Pasca syarat menentukan jaminan yang dibuat oleh komponen perisian kepada pelanggannya. Sekiranya pelanggaran syarat, komponen perisian mempunyai pepijat.

Invarian

Invarian menentukan keadaan yang mesti ditahan bila-bila masa klien dapat menggunakan kaedah objek. Invarian didefinisikan sebagai sebahagian daripada definisi kelas. Dalam praktiknya, invarian dinilai pada bila-bila masa sebelum dan selepas kaedah pada mana-mana kelas yang dijalankan. Pelanggaran invarian mungkin menunjukkan bug pada klien atau komponen perisian.

Tegasan, pewarisan, dan antara muka

Semua penegasan yang ditentukan untuk kelas dan kaedahnya juga berlaku untuk semua subkelas. Anda juga boleh menentukan penegasan untuk antara muka. Oleh itu, semua penegasan antara muka mesti berlaku untuk semua kelas yang melaksanakan antara muka.

iContract - DBC dengan Java

Setakat ini, kita telah membincangkan DBC secara umum. Anda mungkin mempunyai idea sekarang tentang apa yang saya bicarakan, tetapi jika anda baru menggunakan DBC, keadaan mungkin masih sedikit kelam kabut.

Dalam bahagian ini, perkara akan menjadi lebih konkrit. iContract, yang dikembangkan oleh Reto Kamer, menambah konstruk ke Java yang membolehkan anda menentukan pernyataan DBC yang telah kita bincangkan sebelumnya.

Asas iKontrak

iContract adalah preprocessor untuk Java. Untuk menggunakannya, pertama-tama Anda memproses kod Java dengan iContract, menghasilkan satu set fail Java yang dihiasi. Kemudian anda menyusun kod Java yang dihiasi seperti biasa dengan penyusun Java.

Semua arahan iContract dalam kod Java berada di kelas dan komen kaedah, seperti arahan Javadoc. Dengan cara ini, iContract memastikan keserasian mundur lengkap dengan kod Java yang ada, dan anda selalu dapat menyusun kod Java anda secara langsung tanpa pernyataan iContract.

In a typical program lifecycle, you would move your system from a development environment into a test environment, then into a production environment. In the development environment, you would instrument your code with iContract assertions and run it. That way you can catch newly introduced bugs early on. In the test environment you may still want to keep the bulk of the assertions enabled, but you should take them out of performance-critical classes. Sometimes it even makes sense to keep some assertions enabled in a production environment, but only in classes that definitely are in no way critical to your system's performance. iContract allows you to explicitly select the classes that you want to instrument with assertions.

Preconditions

In iContract, you place preconditions in a method header using the @pre directive. Here's an example:

/** * @pre f >= 0.0 */ public float sqrt(float f) { ... } 

The example precondition ensures that the argument f of function sqrt() is greater than or equal to zero. Clients who use that method are responsible for adhering to that precondition. If they don't, we as implementors of sqrt() are simply not responsible for the consequences.

The expression after the @pre is a Java Boolean expression.

Postconditions

Postconditions are likewise added to the header comment of the method they belong to. In iContract, the @post directive defines postconditions:

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

In our example, we have added a postcondition that ensures that the sqrt() method calculates the square root of f within a specific margin of error (+/- 0.001).

iContract introduces some specific notations for postconditions. First of all, return stands for the return value of the method. At runtime, that will be replaced by the method's return value.

Within postconditions, there often exists a need to differentiate between the value of an argument before execution of the method and afterwards, supported in iContract with the @pre operator. If you append @pre to an expression in a postcondition, it will be evaluated based on the system state before the method executes:

/** * Append an element to a collection. * * @post c.size() = [email protected]() + 1 * @post c.contains(o) */ public void append(Collection c, Object o) { ... } 

In the code above, the first postcondition specifies that the size of the collection must grow by 1 when we append an element. The expression [email protected] refers to the collection c before execution of the append method.

Invariants

With iContract, you can specify invariants in the header comment of a class definition:

/** * A PositiveInteger is an Integer that is guaranteed to be positive. * * @inv intValue() > 0 */ class PositiveInteger extends Integer { ... } 

In this example, the invariant guarantees that the PositiveInteger's value is always greater than or equal to zero. That assertion is checked before and after execution of any method of that class.

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 

Pernyataan di atas memerlukan sedikit penjelasan.