Kode ghost

Kontrak dan asersi tidak selalu cukup untuk menyatakan sifat yang ingin dibuktikan, dan pembuktian sering memerlukan perhitungan tambahan yang tidak boleh mengubah perilaku program. SPARK menyediakan kode ghost (ghost code), yaitu konstruksi yang ditandai dengan aspek Ghost, hanya dimaksudkan untuk spesifikasi dan pembuktian, dan dibuang pada build produksi. Topik ini membahas fungsi ghost dan variabel ghost, batasan rujukan antara kode ghost dan kode biasa, serta siklus hidup kode ghost pada build dan pembuktian.

Fungsi dan variabel ghost#

Program berikut menggunakan dua bentuk kode ghost sekaligus. Fungsi Suhu_Sah ditandai Ghost karena hanya dirujuk oleh kontrak, sedangkan variabel Sebelum pada badan prosedur ditandai Ghost karena hanya dirujuk oleh asersi pada prosedur yang sama. Keduanya membantu pembuktian tanpa menjadi bagian dari perilaku program.

with Ada.Text_IO; use Ada.Text_IO;

procedure Batas_Suhu with SPARK_Mode is

   Tertinggi : Integer := 0;

   -- Fungsi ghost: hanya dipakai untuk menyatakan kontrak.
   function Suhu_Sah (X : in Integer) return Boolean with Ghost is
   begin
      return X >= 0 and X <= 100;
   end Suhu_Sah;

   procedure Perbarui_Tertinggi (X : in Integer) with
     Pre  => Suhu_Sah (X),
     Post => Tertinggi >= X and Tertinggi >= Tertinggi'Old
   is
      Sebelum : Integer := Tertinggi with Ghost;
   begin
      if X > Tertinggi then
         Tertinggi := X;
      end if;
      pragma Assert (Tertinggi >= Sebelum);
   end Perbarui_Tertinggi;

begin
   Perbarui_Tertinggi (24);
   Perbarui_Tertinggi (31);
   Perbarui_Tertinggi (27);
   Put_Line ("Tertinggi tercatat =" & Integer'Image (Tertinggi));
end Batas_Suhu;

# kompilasi dengan -gnata agar kontrak dan asersi dinilai saat run time
gnatmake -q -gnata batas_suhu.adb
# jalankan program hasil kompilasi
./batas_suhu

Tertinggi tercatat = 31

Fungsi ghost pada contoh digunakan oleh kontrak, sedangkan variabel ghost lokal menyimpan nilai awal untuk dihubungkan oleh asersi, dan pola ini persis seperti contoh resmi pada Panduan Pengguna SPARK. Kontrak pada entitas yang bukan ghost tetap bukan kode ghost, tetapi kontrak tersebut boleh merujuk entitas ghost, dan inilah cara fungsi serta variabel ghost berperan dalam pembuktian. Selain fungsi dan variabel, SPARK juga menyediakan prosedur ghost untuk merangkum penanganan variabel ghost, serta tipe ghost, package ghost, dan model ghost sebagai abstraksi atas bagian program yang rumit.

Variabel ghost global melayani kebutuhan lain, yaitu mencatat keadaan dari pemanggilan sebelumnya. Variabel semacam itu menyimpan nilai dari pemanggilan terakhir, misalnya nilai argumen sebelumnya, dan nilai tersebut dirujuk oleh kontrak subprogram pada pemanggilan berikutnya. Pola ini memungkinkan kontrak menyatakan sifat urutan pemanggilan, seperti syarat bahwa nilai argumen tidak pernah menurun antarpemanggilan, tanpa menambah satu pun variabel nyata pada program.

Batasan rujukan kode ghost#

Kode ghost wajib bebas pengaruh terhadap perilaku program, dan aturan utamanya adalah kode biasa tidak boleh merujuk entitas ghost. Alasannya, kode ghost dapat dibuang, sehingga pembacaan entitas ghost oleh kode biasa mengubah perilaku program apabila pembuangan terjadi. GNAT menegakkan sebagian aturan ini sejak kompilasi, dan program berikut memuat kode biasa yang membaca variabel ghost untuk memperlihatkan akibatnya.

with Ada.Text_IO; use Ada.Text_IO;

procedure Langgar_Ghost with SPARK_Mode is

   Cadangan : Integer := 0 with Ghost;

begin
   Put_Line ("Cadangan =" & Integer'Image (Cadangan));
end Langgar_Ghost;

# kompilasi gagal, pesan error memang diharapkan muncul
gnatmake -q -gnata langgar_ghost.adb

langgar_ghost.adb:8:44: error: ghost entity cannot appear in this context
gnatmake: "langgar_ghost.adb" compilation error

Pesan error menunjuk tepat pada Cadangan di dalam Put_Line, dan kompilasi berhenti sebelum program dihasilkan. GNATprove menegakkan aturan yang lebih lengkap lagi, yaitu memastikan tidak ada kode ghost yang berpengaruh pada perilaku program maupun pada entitas ghost lain yang sedang aktif, sehingga hasil pembuktian tetap sah untuk setiap konfigurasi kebijakan asersi.

Siklus hidup pada build dan pembuktian#

Siklus kode ghost bergantung pada kebijakan asersi yang dipilih. Pada kompilasi dengan flag -gnata, kebijakan asersi Ghost => Check berlaku sebagaimana tercantum pada manual GNAT, sehingga entitas ghost diterjemahkan seperti entitas biasa dan kontrak yang merujuknya ikut dinilai saat run time. Program Batas_Suhu di atas memperlihatkan perilaku ini, karena Pre yang memanggil fungsi ghost benar-benar dinilai pada setiap pemanggilan Perbarui_Tertinggi.

Pada build produksi, kode ghost dibuang sehingga tidak menambah biaya waktu eksekusi maupun ukuran program. Panduan resmi menyatakan kode ghost dibuat agar dapat dibuang pada kompilasi (discarded during compilation), dan dalam penggunaan yang lazim kode ghost tidak dibawa ke executable akhir. Pembuangan ini menjadi alasan fungsi ghost boleh menggunakan perhitungan yang mahal, misalnya menyalin seluruh isi container, karena perhitungan tersebut hanya dijalankan oleh alat pembuktian.

Kesalahan umum#

• Membaca entitas ghost dari kode biasa. Kompilasi ditolak dengan pesan ghost entity cannot appear in this context, karena pembacaan itu membuat perilaku program bergantung pada kode yang dapat dibuang. Perbaikannya, pindahkan nilai yang diperlukan ke variabel biasa, atau nyatakan sifatnya melalui kontrak dan asersi.
• Memberi efek samping pada kode ghost. Prosedur ghost tidak boleh menghasilkan keluaran non-ghost, baik melalui parameter maupun variabel global, karena efek semacam itu membuat kode non-ghost bergantung pada kode ghost. Perbaikannya, batasi kode ghost pada pembacaan keadaan dan pemeriksaan atas variabel ghost.
• Menganggap semua asersi termasuk kode ghost. Kontrak pada entitas non-ghost bukan kode ghost dan tetap dinilai pada build dengan -gnata, sedangkan penandaan Ghost hanya berlaku pada entitas yang memang ditandai. Perbaikannya, bedakan tujuan asersi biasa dari tujuan kode ghost sebelum menuliskannya.

Ringkasan#

• Kode ghost adalah konstruksi bertanda aspek Ghost yang hanya melayani spesifikasi dan pembuktian, dan dibuang pada build akhir.
• Fungsi ghost digunakan untuk menyatakan properti di dalam kontrak, sedangkan variabel ghost menyimpan catatan keadaan yang dirujuk asersi.
• Kode biasa dilarang merujuk entitas ghost, dan GNAT menolak pelanggarannya saat kompilasi dengan pesan ghost entity cannot appear in this context.

Referensi#

• SPARK User’s Guide: Specification Features, Ghost Code — AdaCore — Definisi kode ghost beserta fungsi, variabel, prosedur, dan model ghost serta aturan pembuangannya.
• GNAT Reference Manual: Implementation Defined Pragmas — AdaCore — Dokumentasi pragma Ghost pada GNAT beserta rujukan semantiknya.
• SPARK User’s Guide: How to View GNATprove Output — AdaCore — Kebijakan asersi bawaan GNAT pada tabel assertion pragma yang dikutip untuk kebijakan Ghost.