KAL
Menu

Aspek Pre dan Post

Aspek Pre dan Post sebagai kontrak subprogram yang diperiksa saat run time.

Daftar isi

Topik ini membahas aspek Pre dan Post, yaitu kontrak yang ditempelkan pada deklarasi subprogram dan diperiksa saat run time. Aspek Pre menyatakan syarat yang wajib benar sebelum badan subprogram dieksekusi, sedangkan aspek Post menyatakan janji yang wajib benar setelah badan selesai. Setelah topik ini dibaca, kontrak pada sebuah subprogram dapat dituliskan, diperiksa, dan dilanggar secara sengaja untuk mengamati pesan pemeriksaannya.

Kontrak pada deklarasi subprogram#

Aspek dinyatakan setelah tanda tangan subprogram dengan kata with, dan isinya berupa ekspresi boolean yang dinilai oleh pemeriksaan run time. Di dalam aspek Post pada sebuah fungsi, atribut Result yang ditulis Bagi'Result merujuk nilai yang akan dikembalikan. Kontrak yang baik menyatakan tujuan, bukan langkah, sehingga pembaca deklarasi dapat memahami syarat dan janjinya tanpa membaca badan subprogram.

ada Kontrak pada deklarasi fungsi Bagi 
function Bagi (Pembilang, Penyebut : in Integer) return Integer with
  Pre  => Penyebut /= 0,
  Post => Bagi'Result * Penyebut + Pembilang rem Penyebut = Pembilang;

Klausa Pre pada contoh menuntut penyebut bukan nol sebelum pembagian dilakukan, sedangkan klausa Post menjanjikan sifat pembagian bilangan bulat, yaitu hasil kali penyebut ditambah sisa pembagian selalu mengembalikan pembilang. Janji seperti itu dapat dinilai tanpa mengungkap isi badan, dan inilah alasan kontrak ditempatkan pada deklarasi, bukan pada badan. Pada proyek nyata, deklarasi subprogram berada pada spesifikasi package, sehingga kontrak terbaca oleh setiap pemanggilnya.

Selain Result, ekspresi Post juga dapat merujuk nilai parameter pada saat pemanggilan melalui atribut Old. Penulisan X'Old pada klausa Post merekam nilai X sebelum badan dieksekusi, sehingga janji dapat membandingkan keadaan awal dengan keadaan akhir, misalnya Hasil'Result = X'Old + 1 untuk menjanjikan penambahan tepat satu. Atribut ini menjadikan Post jauh lebih bermanfaat pada prosedur dengan mode out dan in out, karena janjinya dapat menyatakan hubungan antara nilai masuk dan nilai keluar, bukan sekadar kendala pada hasilnya.

Pemeriksaan saat run time#

Program berikut memanggil fungsi Bagi dua kali dengan penyebut yang sah, dan keduanya lolos kedua aspek. Kompilasi menggunakan -gnata agar pemeriksaan kontrak benar-benar berjalan.

ada kontrak_bagi.adb 
with Ada.Text_IO; use Ada.Text_IO;

procedure Kontrak_Bagi is

   -- Kontrak: penyebut tidak boleh nol, dan hasil kali penyebut ditambah
   -- sisa harus mengembalikan pembilang.
   function Bagi (Pembilang, Penyebut : in Integer) return Integer with
     Pre  => Penyebut /= 0,
     Post => Bagi'Result * Penyebut + Pembilang rem Penyebut = Pembilang
   is
   begin
      return Pembilang / Penyebut;
   end Bagi;

begin
   Put_Line ("Bagi (7, 2)   =" & Integer'Image (Bagi (7, 2)));
   Put_Line ("Bagi (100, 5) =" & Integer'Image (Bagi (100, 5)));
end Kontrak_Bagi;
bash 
# kompilasi dengan flag -gnata agar kontrak diperiksa
gnatmake -q -gnata kontrak_bagi.adb
# jalankan program hasil kompilasi
./kontrak_bagi
text Keluaran 
Bagi (7, 2)   = 3
Bagi (100, 5) = 20

Pada setiap pemanggilan, Pre dinilai lebih dahulu, badan dieksekusi, dan Post dinilai setelah nilai kembali dihasilkan. Membagi 7 dengan 2 menghasilkan 3 sisa 1, dan persamaan 3 kali 2 ditambah 1 sama dengan 7 terpenuhi, sehingga janji Post benar. Urutan pemeriksaan ini sama pada semua pemanggilan, sehingga pemanggil yang melanggar Pre tidak pernah sampai ke badan, sedangkan pelanggaran Post berarti badan tidak menepati janjinya.

Pelanggaran kontrak yang tertangkap#

Dua program berikut membiarkan kontrak dilanggar agar pesan pemeriksaannya terlihat. Program pertama memanggil Bagi dengan penyebut nol, dan program kedua memuat fungsi Absolut yang badannya mengembalikan nilai negatif tanpa menjadikannya mutlak.

ada langgar_pre.adb 
with Ada.Text_IO; use Ada.Text_IO;

procedure Langgar_Pre is

   function Bagi (Pembilang, Penyebut : in Integer) return Integer with
     Pre  => Penyebut /= 0,
     Post => Bagi'Result * Penyebut + Pembilang rem Penyebut = Pembilang
   is
   begin
      return Pembilang / Penyebut;
   end Bagi;

   Penyebut : Integer := 0;

begin
   Put_Line ("Bagi (7, Penyebut) =" & Integer'Image (Bagi (7, Penyebut)));
end Langgar_Pre;
bash 
# kompilasi lalu jalankan, exception memang diharapkan muncul
gnatmake -q -gnata langgar_pre.adb
./langgar_pre
text Keluaran 
raised ADA.ASSERTIONS.ASSERTION_ERROR : failed precondition from langgar_pre.adb:6
ada langgar_post.adb 
with Ada.Text_IO; use Ada.Text_IO;

procedure Langgar_Post is

   -- Kontrak: hasil fungsi tidak boleh negatif.
   function Absolut (X : in Integer) return Integer with
     Post => Absolut'Result >= 0
   is
   begin
      return X;   -- bug: nilai negatif belum dibuat mutlak
   end Absolut;

begin
   Put_Line ("Absolut (5)  =" & Integer'Image (Absolut (5)));
   Put_Line ("Absolut (-8) =" & Integer'Image (Absolut (-8)));
end Langgar_Post;
bash 
# kompilasi lalu jalankan, exception memang diharapkan muncul
gnatmake -q -gnata langgar_post.adb
./langgar_post
text Keluaran 
Absolut (5)  = 5

raised ADA.ASSERTIONS.ASSERTION_ERROR : failed postcondition from langgar_post.adb:7

Pesan pemeriksaan menyebut ADA.ASSERTIONS.ASSERTION_ERROR, yaitu exception bawaan yang dipicu oleh pemeriksaan assertion, diikuti keterangan failed precondition atau failed postcondition beserta berkas dan baris aspeknya. Pada program pertama, baris yang disebut menunjuk klausa Pre, dan badan Bagi tidak pernah dieksekusi. Pada program kedua, pemanggilan pertama lolos dan hasilnya tercetak, sedangkan pemanggilan dengan nilai negatif tertangkap oleh Post sebelum keluarannya dicetak. Penunjuk berkas dan baris merujuk berkas sumber yang dikompilasi, sehingga pesan langsung membawa pembaca ke aspek yang terlanggar.

Pembagian tanggung jawab mengikuti pihak yang melanggar. Pelanggaran Pre berarti pemanggil tidak menepati syarat pemanggilan, sehingga perbaikannya berada di sisi pemanggil, misalnya memperbaiki nilai yang dikirim atau memperluas kontrak apabila syaratnya memang terlalu ketat. Pelanggaran Post berarti badan tidak menepati janjinya, sehingga perbaikannya berada di sisi penulis badan, misalnya memperbaiki algoritma atau menurunkan janji agar sesuai kenyataan. Kebiasaan ini menjaga kontrak tetap sesuai kenyataan dan membuat laporan kegagalan langsung menunjuk pihak yang wajib bertindak.

Kesalahan umum#

  • Menganggap kontrak selalu aktif. Tanpa flag -gnata, pemeriksaan Pre dan Post dilewati, sehingga pelanggaran tidak terdeteksi sama sekali. Perbaikannya, aktifkan -gnata pada konfigurasi build yang digunakan sehari-hari, dan tetap perlakukan kontrak sebagai dokumentasi yang penting, bukan sekadar pemeriksaan otomatis.
  • Menjanjikan lebih daripada yang dipenuhi badan. Kontrak Post pada program kedua benar sebagai tujuan, tetapi badannya tidak menepati janji itu, dan kegagalan itu baru terlihat ketika data negatif muncul. Perbaikannya, uji kontrak dengan data tepat pada batas, misalnya nilai negatif dan nol, atau buktikan kontrak secara statis dengan GNATprove.
  • Menuliskan kontrak yang meniru langkah badan. Klausa yang menyatakan urutan perhitungan internal hanya membebani pembaca dan mudah kedaluwarsa apabila badan berubah. Perbaikannya, nyatakan tujuan dan sifat hasilnya, seperti persamaan pembagian pada contoh di atas.

Ringkasan#

  • Aspek Pre diperiksa sebelum badan dieksekusi, sedangkan aspek Post diperiksa setelah badan selesai, dan keduanya ditulis pada deklarasi dengan kata with.
  • Pelanggaran kontrak memunculkan ADA.ASSERTIONS.ASSERTION_ERROR dengan keterangan berkas dan baris aspek yang terlanggar.
  • Pemeriksaan run time aktif dengan flag -gnata, dan kontrak yang sama dapat dibuktikan secara statis oleh GNATprove.

Referensi#