KAL
Menu

Invarian loop

Invarian loop agar loop dapat ditangani prover.

Daftar isi

Prover memeriksa program dengan menerjemahkannya menjadi rumus logika, dan loop menjadi kasus yang sulit karena jumlah iterasinya bergantung pada data masukan. Invarian loop (loop invariant) adalah asersi yang menyatakan sifat yang berlaku pada setiap iterasi loop, sehingga prover dapat meringkas seluruh perulangan menjadi satu rumus yang ukurannya tidak bergantung pada jumlah iterasi. Topik ini membahas alasan prover memerlukan invarian, cara menuliskannya dengan pragma Loop_Invariant, sifat invarian loop yang baik, serta pemeriksaan invarian saat run time.

Alasan prover memerlukan invarian#

Pembuktian formal menalar keadaan program pada titik-titik tertentu, sedangkan loop mengembalikan kendali ke titik yang sama berkali-kali dengan nilai yang berubah. Tanpa informasi tambahan, prover tidak dapat menentukan sifat yang berlaku pada iterasi ke-n, sehingga sifat yang ingin dibuktikan setelah loop tidak dapat disimpulkan. Invarian loop menyediakan informasi itu dengan menyatakan hubungan antarvariabel yang bertahan dari iterasi ke iterasi.

GNATprove memeriksa dua properti atas setiap invarian loop. Loop invariant initialization menuntut invarian benar pada iterasi pertama, sedangkan loop invariant preservation menuntut invarian benar pada iterasi berapa pun dengan asumsi invarian benar pada iterasi sebelumnya. Kedua properti ini diperiksa secara terpisah, sehingga kegagalan pada salah satunya dilaporkan dengan pesan yang spesifik.

Posisi pragma juga menentukan maknanya. Asersi pada Loop_Invariant dinilai pada titik penulisan pragmanya, sehingga invarian di akhir tubuh loop menyatakan keadaan setelah tubuh dieksekusi, sedangkan invarian di awal tubuh menyatakan keadaan sebelum tubuh dieksekusi pada setiap iterasi.

Program berikut menghitung jumlah bacaan sensor yang melampaui ambang, dan kontraknya menjamin hasil tidak melebihi panjang data. Invarian Hasil <= J menyatakan hubungan antara penghitung hasil dan indeks loop, dan hubungan itulah yang membuat kontrak setelah loop dapat dibuktikan.

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

procedure Hitung_Bacaan with SPARK_Mode is

   type Bacaan is array (1 .. 8) of Integer;

   Suhu : constant Bacaan := (24, 31, 27, 35, 29, 33, 22, 30);

   function Hitung_Lewat (Data : Bacaan; Ambang : Integer) return Natural with
     Pre  => (for all J in Data'Range => Data (J) >= 0),
     Post => Hitung_Lewat'Result <= Data'Length
   is
      Hasil : Natural := 0;
   begin
      for J in Data'Range loop
         if Data (J) > Ambang then
            Hasil := Hasil + 1;
         end if;
         pragma Loop_Invariant (Hasil <= J);
      end loop;
      return Hasil;
   end Hitung_Lewat;

begin
   Put_Line ("Bacaan di atas 28 =" & Integer'Image (Hitung_Lewat (Suhu, 28)));
end Hitung_Bacaan;
bash 
# kompilasi dengan -gnata agar invarian loop ikut dinilai saat run time
gnatmake -q -gnata hitung_bacaan.adb
# jalankan program hasil kompilasi
./hitung_bacaan
text Keluaran 
Bacaan di atas 28 = 5

Invarian pada contoh memenuhi empat sifat invarian loop yang baik menurut panduan resmi. Sifat pertama, yaitu invarian benar pada iterasi pertama, terpenuhi karena Hasil paling banyak bertambah satu dan tidak mungkin melebihi J yang bernilai satu. Sifat kedua dan ketiga, yaitu invarian cukup kuat untuk membuktikan pemeriksaan di dalam loop maupun kontrak setelah loop, terpenuhi karena Hasil <= J pada akhir loop berarti Hasil <= Data'Length. Sifat keempat, yaitu invarian dipertahankan pada iterasi berikutnya, terpenuhi karena setiap iterasi menaikkan J satu kali dan menaikkan Hasil paling banyak satu kali.

Menuliskan invarian memerlukan ketelitian, tetapi bahasa menyediakan bantuan berupa atribut Loop_Entry yang merujuk nilai sebuah ekspresi pada saat loop dimasuki. Atribut ini hanya sah di dalam ekspresi pragma Loop_Invariant. Dengan atribut tersebut, perbandingan antara keadaan saat ini dan keadaan awal loop dapat dinyatakan tanpa menambah variabel bantu, misalnya X = X'Loop_Entry + J.

Invarian yang keliru terdeteksi#

Invarian yang keliru dapat terdeteksi tanpa gnatprove. Kompilasi dengan flag -gnata membuat pragma Loop_Invariant dinilai seperti pragma Assert pada setiap iterasi, sehingga invarian yang tidak benar memunculkan exception saat program dijalankan. Program berikut mengganti invarian dengan persamaan Hasil = J.

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

procedure Salah_Invarian with SPARK_Mode is

   type Bacaan is array (1 .. 8) of Integer;

   Suhu : constant Bacaan := (24, 31, 27, 35, 29, 33, 22, 30);

   function Hitung_Lewat (Data : Bacaan; Ambang : Integer) return Natural with
     Pre  => (for all J in Data'Range => Data (J) >= 0),
     Post => Hitung_Lewat'Result <= Data'Length
   is
      Hasil : Natural := 0;
   begin
      for J in Data'Range loop
         if Data (J) > Ambang then
            Hasil := Hasil + 1;
         end if;
         pragma Loop_Invariant (Hasil = J);   -- invarian yang salah
      end loop;
      return Hasil;
   end Hitung_Lewat;

begin
   Put_Line ("Bacaan di atas 28 =" & Integer'Image (Hitung_Lewat (Suhu, 28)));
end Salah_Invarian;
bash 
# kompilasi lalu jalankan, exception memang diharapkan muncul
gnatmake -q -gnata salah_invarian.adb
./salah_invarian
text Keluaran 
raised ADA.ASSERTIONS.ASSERTION_ERROR : Loop_Invariant failed at salah_invarian.adb:19

Pesan run time menyebut Loop_Invariant failed beserta berkas dan baris pragmanya, dan kegagalan terjadi pada iterasi pertama karena Hasil masih bernilai 0 sedangkan J bernilai 1. GNATprove melaporkan kekeliruan yang sama secara statis dengan pesan khusus. Pesan berikut dikutip dari Panduan Pengguna SPARK untuk contoh invarian yang gagal pada iterasi pertama.

text Keluaran yang diharapkan 
 high: loop invariant might fail in first iteration
--> simple_loops.adb:8:30
    8 |          pragma Loop_Invariant (Prop);
      |                                 ^~~~
      + e.g. when Prop = False

Untuk invarian yang benar pada iterasi pertama tetapi gagal pada iterasi berikutnya, panduan melaporkan pesan medium: loop invariant might not be preserved by an arbitrary iteration, sehingga letak kekeliruannya dapat dibedakan dari tingkat dan isi pesan.

Kesalahan umum#

  • Menulis invarian yang terlalu lemah. Invarian True selalu terbukti, tetapi tidak memberi informasi apa pun kepada prover, sehingga kontrak setelah loop tetap tidak dapat dibuktikan. Perbaikannya, nyatakan hubungan antarvariabel yang benar-benar dibangun oleh loop, seperti hubungan penghitung dengan indeks pada contoh di atas.
  • Menulis invarian yang kuat tetapi tidak induktif. Invarian yang benar pada setiap eksekusi nyata tetap ditolak apabila prover tidak dapat membuktikan pemeliharaannya hanya dengan asumsi invarian pada iterasi sebelumnya. Perbaikannya, lengkapi invarian dengan informasi yang menjelaskan mengapa sifatnya bertahan.
  • Mengabaikan komponen yang tidak diubah. Apabila loop memodifikasi sebagian array atau record, prover harus diberi tahu bahwa bagian lainnya tidak berubah, yaitu syarat bingkai (frame condition). Perbaikannya, tambahkan pernyataan kesetaraan atas bagian yang tidak diubah oleh loop, atau andalkan frame condition yang dihasilkan otomatis pada kasus sederhana.

Ringkasan#

  • Invarian loop menyatakan sifat yang berlaku pada setiap iterasi dan memungkinkan prover meringkas loop yang tidak dapat diuraikan otomatis.
  • GNATprove memeriksa inisialisasi pada iterasi pertama dan pemeliharaan pada iterasi berikutnya sebagai dua properti yang terpisah.
  • Dengan flag -gnata, pragma Loop_Invariant dinilai seperti asersi pada setiap iterasi, sehingga invarian yang keliru memunculkan ADA.ASSERTIONS.ASSERTION_ERROR saat run time.

Referensi#