iContract: Design by Contract di Jawa

Bukankah lebih baik jika semua kelas Java yang Anda gunakan, termasuk Anda sendiri, memenuhi janji mereka? Nyatanya, bukankah menyenangkan jika Anda benar-benar tahu persis apa yang dijanjikan kelas? Jika Anda setuju, baca terus - Design by Contract dan iContract datang untuk membantu.

Catatan: Sumber kode untuk contoh dalam artikel ini dapat diunduh dari Sumber.

Desain berdasarkan Kontrak

Teknik pengembangan perangkat lunak Design by Contract (DBC) memastikan perangkat lunak berkualitas tinggi dengan menjamin bahwa setiap komponen sistem memenuhi harapannya. Sebagai pengembang yang menggunakan DBC, Anda menetapkan kontrak komponen sebagai bagian dari antarmuka komponen. Kontrak menentukan apa yang diharapkan komponen itu dari klien dan apa yang dapat diharapkan klien darinya.

Bertrand Meyer mengembangkan DBC sebagai bagian dari bahasa pemrograman Eiffel. Terlepas dari asalnya, DBC adalah teknik desain yang berharga untuk semua bahasa pemrograman, termasuk Java.

Inti dari DBC adalah gagasan tentang pernyataan - ekspresi Boolean tentang keadaan sistem perangkat lunak. Saat runtime kami mengevaluasi pernyataan di checkpoint tertentu selama eksekusi sistem. Dalam sistem perangkat lunak yang valid, semua pernyataan dievaluasi sebagai benar. Dengan kata lain, jika ada pernyataan yang dinilai salah, kami menganggap sistem perangkat lunak tidak valid atau rusak.

Pengertian sentral DBC agak berkaitan dengan #assertmakro dalam bahasa pemrograman C dan C ++. Namun DBC mengambil pernyataan jutaan tingkat lebih jauh.

Di DBC, kami mengidentifikasi tiga jenis ekspresi:

  • Prasyarat
  • Kondisi pasca
  • Invarian

Mari kita periksa masing-masing lebih detail.

Prasyarat

Prasyarat menentukan kondisi yang harus dipertahankan sebelum metode dapat dijalankan. Dengan demikian, mereka dievaluasi tepat sebelum metode dijalankan. Prasyarat melibatkan status sistem dan argumen yang diteruskan ke dalam metode.

Prasyarat menentukan kewajiban yang harus dipenuhi klien komponen perangkat lunak sebelum dapat menjalankan metode komponen tertentu. Jika prasyarat gagal, bug ada di klien komponen perangkat lunak.

Kondisi pasca

Sebaliknya, kondisi pasca menentukan kondisi yang harus dipertahankan setelah metode selesai. Akibatnya, kondisi akhir dieksekusi setelah metode selesai. Kondisi akhir melibatkan status sistem lama, status sistem baru, argumen metode, dan nilai kembalian metode.

Postconditions menentukan jaminan yang diberikan komponen perangkat lunak kepada kliennya. Jika kondisi pasca dilanggar, komponen perangkat lunak memiliki bug.

Invarian

Sebuah invariant menetapkan kondisi yang harus dipertahankan setiap kali klien dapat memanggil metode objek. Invarian didefinisikan sebagai bagian dari definisi kelas. Dalam praktiknya, invarian dievaluasi kapan saja sebelum dan setelah metode pada setiap instance kelas dijalankan. Pelanggaran invarian dapat mengindikasikan bug di klien atau komponen perangkat lunak.

Pernyataan, warisan, dan antarmuka

Semua pernyataan yang ditentukan untuk kelas dan metodenya juga berlaku untuk semua subkelas. Anda juga dapat menentukan pernyataan untuk antarmuka. Dengan demikian, semua pernyataan antarmuka harus berlaku untuk semua kelas yang mengimplementasikan antarmuka.

iContract - DBC dengan Java

Sejauh ini, kita telah membicarakan tentang DBC secara umum. Sekarang Anda mungkin sudah tahu apa yang saya bicarakan, tetapi jika Anda baru mengenal DBC, semuanya mungkin masih sedikit berkabut.

Pada bagian ini, segalanya akan menjadi lebih konkret. iContract, yang dikembangkan oleh Reto Kamer, menambahkan konstruksi ke Java yang memungkinkan Anda menentukan pernyataan DBC yang kita bicarakan sebelumnya.

Dasar-dasar iContract

iContract adalah preprocessor untuk Java. Untuk menggunakannya, Anda terlebih dahulu memproses kode Java Anda dengan iContract, menghasilkan satu set file Java yang dihias. Kemudian Anda mengkompilasi kode Java yang dihias seperti biasa dengan compiler Java.

Semua arahan iContract dalam kode Java berada di komentar kelas dan metode, seperti arahan Javadoc. Dengan cara ini, iContract memastikan kompatibilitas mundur lengkap dengan kode Java yang ada, dan Anda selalu bisa langsung mengompilasi kode Java Anda tanpa pernyataan iContract.

Dalam siklus hidup program biasa, Anda akan memindahkan sistem dari lingkungan pengembangan ke lingkungan pengujian, lalu ke lingkungan produksi. Dalam lingkungan pengembangan, Anda akan melengkapi kode Anda dengan pernyataan iContract dan menjalankannya. Dengan begitu, Anda dapat menemukan bug yang baru diperkenalkan sejak dini. Di lingkungan pengujian, Anda mungkin masih ingin mengaktifkan sebagian besar pernyataan, tetapi Anda harus mengeluarkannya dari kelas yang mengutamakan performa. Kadang-kadang masuk akal untuk tetap mengaktifkan beberapa pernyataan dalam lingkungan produksi, tetapi hanya di kelas yang sama sekali tidak penting untuk kinerja sistem Anda. iContract memungkinkan Anda untuk secara eksplisit memilih kelas yang ingin Anda lengkapi dengan pernyataan.

Prasyarat

Di iContract, Anda menempatkan prasyarat di header metode menggunakan @predirektif. Berikut contohnya:

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

Contoh prasyarat memastikan bahwa argumen ffungsi sqrt()lebih besar dari atau sama dengan nol. Klien yang menggunakan metode tersebut bertanggung jawab untuk mematuhi prasyarat tersebut. Jika tidak, kami sebagai pelaksana sqrt()tidak bertanggung jawab atas konsekuensinya.

Ekspresi setelah @preadalah ekspresi Java Boolean.

Kondisi pasca

Kondisi akhir juga ditambahkan ke komentar header dari metode mereka. Di iContract, @postdirektif mendefinisikan 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 membutuhkan sedikit penjelasan.