KAL
Menu

Subset SPARK

Subset SPARK dari Ada: bagian yang dibuang dan alasan pembuangannya.

Daftar isi

SPARK adalah subset bahasa Ada yang diperluas dengan kontrak untuk pembuktian formal (formal verification), yaitu pengujian kebenaran program dengan metode matematis sebelum program dijalankan. Sebagai subset, SPARK membuang sejumlah konstruksi Ada yang menghambat pembuktian, dan setiap pembuangan memiliki alasan teknis yang dapat dijelaskan. Topik ini membahas batas antara SPARK dan Ada, menguraikan konstruksi yang dibuang beserta alasannya, serta menunjukkan bahwa program yang mematuhi subset tetap merupakan program Ada biasa yang dapat dikompilasi dan dijalankan dengan GNAT.

Batas antara SPARK dan Ada#

Panduan resmi SPARK mendeskripsikan bahasa ini dengan dua langkah sekaligus, yaitu memangkas fitur yang menghambat pembuktian dan memperluas sistem kontrak serta aspek agar pembuktian formal dapat berjalan secara modular. Langkah pertama menjadikan SPARK subset dari Ada. Setiap program SPARK adalah program Ada yang sah, sehingga GNAT mengompilasinya tanpa pengaturan khusus, sedangkan arah sebaliknya tidak berlaku karena program Ada bebas menggunakan konstruksi yang tidak masuk subset.

SPARK menyediakan penanda keanggotaan subset berupa pragma SPARK_Mode dan aspek SPARK_Mode dengan nilai On atau Off. Pada unit yang ditandai On, seluruh kode wajib mematuhi subset, sedangkan unit yang ditandai Off bebas menggunakan fitur Ada apa pun. Cara ini memungkinkan satu program memuat kode SPARK dan kode Ada biasa secara berdampingan, misalnya bagian antarmuka perangkat keras ditulis dalam Ada penuh, sedangkan bagian yang lain dibuktikan secara formal.

Konstruksi yang dibuang dan alasannya#

Bab Language Restrictions pada Panduan Pengguna SPARK menetapkan daftar konstruksi yang dibuang, dan setiap butirnya disertai alasan yang berkaitan dengan pembuktian. Konstruksi yang utama adalah sebagai berikut.

  • Tipe akses (access type) dan alokator memori diberi kebijakan kepemilikan, yaitu aturan bahwa hanya satu objek akses yang boleh mengubah suatu memori teralokasi pada satu waktu. Aturan ini mencegah dua nama menulis pada memori yang sama, sehingga pembuktian atas memori dinamis dapat dilakukan secara presisi.
  • Semua ekspresi, termasuk pemanggilan fungsi, wajib bebas efek samping. Fungsi tanpa efek samping dapat diperlakukan sebagai fungsi matematis di dalam kontrak, dan sifat tersebut dibutuhkan oleh prover, yaitu mesin pembuktian otomatis yang bekerja atas rumus logika.
  • Aliasing tidak diizinkan. Apabila dua nama menunjuk objek yang sama, nilai yang diubah melalui satu nama ikut berubah melalui nama lain, sehingga prover tidak selalu dapat menyimpulkan perilaku kode tersebut secara tepat.
  • goto mundur (backward goto) tidak diizinkan karena lompatan mundur menciptakan loop yang tidak tampak sebagai pernyataan loop. Pembuktian loop memerlukan konstruksi loop yang eksplisit karena invarian loop hanya ditempatkan di dalam pernyataan loop.
  • Tipe controlled tidak diizinkan karena kompilator menyisipkan pemanggilan implisit yang tidak memiliki kode sumber, sehingga GNATprove tidak dapat melaporkan lokasi sumber atas pemanggilan tersebut.
  • Kode generik tidak dianalisis pada unit generiknya, melainkan pada setiap instansiasinya, sehingga kontrak yang diperiksa selalu konkret untuk tipe yang bersangkutan.

Konstruksi yang kerap diduga dibuang tetapi ternyata dipertahankan adalah exception. Raise statement dan raise expression tetap bagian SPARK, dan GNATprove menghasilkan kewajiban bukti atas kedua bentuk tersebut. Konkurensi pun tidak dibuang seluruhnya, tetapi dibatasi pada profil Ravenscar agar perilaku task dapat dianalisis secara deterministik. Fragmen berikut memperlihatkan goto mundur yang ditolak.

ada goto mundur yang dibuang dari SPARK 
<<Ulangi>>
   Posisi := Posisi - 1;
   if Posisi > 0 then
      goto Ulangi;   -- loop terselubung bagi prover, ditolak sebagai error
   end if;

Kode subset tetap dikompilasi dan dijalankan#

Program berikut menghitung rata-rata bacaan sensor suhu dan mematuhi subset secara penuh. Tipe data yang digunakan adalah array tetap tanpa tipe akses, fungsi Rata_Rata bebas efek samping karena hanya membaca parameternya, dan tidak ada dua nama yang menunjuk objek yang sama. Kontrak Pre dan Post dituliskan pada fungsi agar sifat hasil menjadi kewajiban bukti, sedangkan aspek SPARK_Mode menandai prosedur utama sebagai kode SPARK.

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

procedure Rata_Sensor with SPARK_Mode is

   type Data_Suhu is array (1 .. 6) of Integer;

   function Rata_Rata (Data : Data_Suhu) return Integer with
     Pre  => (for all J in Data'Range => Data (J) in 0 .. 1000),
     Post => Rata_Rata'Result in 0 .. 1000
   is
      Total : Integer := 0;
   begin
      for J in Data'Range loop
         Total := Total + Data (J);
      end loop;
      return Total / Data'Length;
   end Rata_Rata;

   Suhu : constant Data_Suhu := (21, 24, 23, 25, 22, 27);

begin
   Put_Line ("Rata-rata bacaan =" & Integer'Image (Rata_Rata (Suhu)));
end Rata_Sensor;
bash 
# kompilasi program SPARK dengan GNAT biasa
gnatmake -q -gnata rata_sensor.adb
# jalankan program hasil kompilasi
./rata_sensor
text Keluaran 
Rata-rata bacaan = 23

Tidak ada flag khusus SPARK pada pemanggilan gnatmake karena GNAT memperlakukan berkas ini sebagai Ada biasa. Kontrak Pre mensyaratkan bacaan berada pada rentang 0 sampai 1000, sedangkan Post menjamin hasil pada rentang yang sama. Apabila kode ini dianalisis dengan GNATprove, kontrak tersebut beserta pemeriksaan run time seperti luapan penjumlahan menjadi kewajiban bukti yang harus dibuktikan secara matematis.

Kesalahan umum#

  • Menganggap SPARK sebagai bahasa dengan pustaka terpisah. Pustaka standar Ada tetap digunakan, dan yang diperiksa adalah konstruksi yang digunakan kode SPARK, bukan asal pustakanya. Perbaikannya, gunakan pustaka seperti biasa dan biarkan GNATprove menandai bagian yang menimbulkan pelanggaran.
  • Menganggap semua fitur dinamis terlarang. Tipe akses tetap dapat digunakan dengan kebijakan kepemilikannya, sehingga alokasi memori tidak otomatis menyingkirkan kode dari SPARK. Perbaikannya, baca ulang batasan tipe akses pada bab Language Restrictions sebelum menyimpulkan.
  • Beranggapan bahwa GNAT menolak konstruksi terlarang pada unit SPARK_Mode => On. Kompilasi tetap berhasil, dan pelanggaran baru terlihat ketika GNATprove dijalankan. Perbaikannya, jadikan pemanggilan GNATprove bagian tetap dari alur kerja, bukan langkah opsional.

Ringkasan#

  • SPARK adalah subset Ada yang diperluas dengan kontrak, sehingga setiap program SPARK dapat dikompilasi dan dijalankan dengan GNAT biasa, sedangkan kebalikannya tidak berlaku.
  • Konstruksi utama yang dibuang mencakup aliasing, efek samping pada fungsi, goto mundur, tipe controlled, dan generik yang dianalisis pada instansiasinya, sedangkan exception dipertahankan dengan kewajiban bukti.
  • Unit yang ditandai SPARK_Mode => On wajib mematuhi subset, dan pemeriksaan pelanggarannya dilakukan oleh GNATprove, bukan oleh kompilator.

Referensi#