Alur kerja GNATprove

GNATprove adalah alat verifikasi resmi SPARK yang menggabungkan analisis aliran data (flow analysis) dan pembuktian formal dalam satu pemanggilan. Topik ini membahas alur kerjanya, mulai dari berkas proyek yang menjadi titik masuk, pilihan mode dan tingkat bukti, sampai pembacaan kategori pesan yang dilaporkan. Program contoh dikompilasi dan dijalankan secara nyata dengan gprbuild dan GNAT, sedangkan keluaran gnatprove dikutip dari Panduan Pengguna SPARK karena alat tersebut belum terpasang pada lingkungan latihan.

Berkas proyek sebagai titik masuk#

GNATprove didistribusikan sebagai executable bernama gnatprove dan, seperti alat lain pada keluarga GNAT, berpijak pada struktur proyek GNAT yang didefinisikan dalam berkas .gpr. Berkas proyek yang sama digunakan oleh dua alat sekaligus, yaitu gprbuild yang membangun program dan gnatprove yang memeriksanya, sehingga daftar sumber proyek dinyatakan satu kali saja. Bentuk paling sederhana dari berkas proyek hanya menyatakan direktori sumber dan berkas utama.

Program berikut memuat kontrak yang akan menjadi objek pemeriksaan, dan berkas proyeknya mengikuti contoh pada panduan resmi.

with Ada.Text_IO; use Ada.Text_IO;

procedure Pemeriksa with SPARK_Mode is

   function Sisa (X, Y : in Natural) return Natural with
     Pre  => Y > 0,
     Post => Sisa'Result < Y
   is
   begin
      return X mod Y;
   end Sisa;

begin
   Put_Line ("Sisa (17, 5)  =" & Integer'Image (Sisa (17, 5)));
   Put_Line ("Sisa (1024, 8)=" & Integer'Image (Sisa (1024, 8)));
end Pemeriksa;

project Verifikasi is

   for Source_Dirs use (".");
   for Main use ("pemeriksa.adb");

end Verifikasi;

# bangun proyek dengan gprbuild menggunakan berkas proyek yang sama
gprbuild -q -P verifikasi.gpr
# jalankan program utama proyek
./pemeriksa

Sisa (17, 5)  = 2
Sisa (1024, 8)= 0

Pembangunan dengan gprbuild memastikan berkas proyek benar bentuknya sebelum digunakan oleh gnatprove. Kedua panggilan pada fungsi Sisa memenuhi kontraknya, yaitu penyebut positif dan hasil sisa yang lebih kecil dari penyebut. Akibatnya, program berjalan tanpa exception, dan pemeriksaan oleh GNATprove nantinya tidak menimbulkan satu pun pesan.

Mode pemeriksaan dan tingkat bukti#

Switch --mode memilih analisis yang dijalankan oleh GNATprove, dan pilihannya bertingkat dari pemeriksaan aturan saja sampai pembuktian penuh. Mode bawaannya adalah all, sedangkan seluruh pilihan mode menurut panduan resmi adalah sebagai berikut.

Switch --level memilih pengaturan bawaan untuk pembuktian, dari level 0 yang paling cepat sampai level 4 yang paling kuat. Nilai level menentukan prover otomatis yang dipanggil, misalnya cvc5 dan z3, beserta batas waktunya. Level 2 merupakan pilihan yang lazim untuk pekerjaan sehari-hari.

# tidak-dijalankan
# perintah berikut dijalankan pada lingkungan yang memasang gnatprove
gnatprove -P verifikasi.gpr --mode=all --level=2

Pada proyek contoh ini, pemanggilan tersebut tidak menghasilkan satu pun pesan check maupun warning, karena seluruh pemeriksaan run time dan kontrak fungsi Sisa terbukti. Diagram berikut merangkum alur kerja dari kontrak menuju pesan perbaikan.

Membaca pesan hasil verifikasi#

GNATprove mengelompokkan keluarannya menjadi empat kategori. Error dilaporkan untuk pelanggaran aturan SPARK atau aturan legalitas Ada dan wajib diperbaiki sebelum analisis berlanjut. Warning berawalan warning: dan menandai kejadian yang mencurigakan, misalnya nilai yang tidak pernah digunakan. Check message diberi tingkat keparahan low:, medium:, atau high: dan menandai kemungkinan masalah yang memengaruhi kebenaran program. Information message berawalan info: dan memberi keterangan tambahan, misalnya pemberitahuan bahwa suatu check terbukti.

Bentuk pesan tersebut paling mudah dipahami dari contoh resmi. Panduan Pengguna SPARK menggunakan prosedur Diff yang mengandung bug, dan mode flow melaporkan hal berikut.

procedure Diff (X, Y : in Natural; Z : out Natural) with
  SPARK_Mode,
  Depends => (Z => (X, Y))
is
begin
   Z := X - X;   -- Y tidak pernah digunakan
end Diff;

 warning: unused variable "Y"
--> diff.adb:1:20
    1 |    procedure Diff (X, Y : in Natural; Z : out Natural) with
      |                       ^

 medium: missing dependency "null => Y"
--> diff.adb:3:03
    3 |      Depends => (Z => (X, Y))
      |      ^~~~~~~~~~~~~~~~~~~~~~

 medium: incorrect dependency "Z => Y"
--> diff.adb:3:24
    3 |      Depends => (Z => (X, Y))
      |                           ^

Setelah kode diperbaiki menjadi Z := X - Y, mode proof masih menemukan peluang error run time pada tipe Natural yang tidak memuat nilai negatif. Pesan berikut, yang juga dikutip dari panduan yang sama, memperlihatkan cara GNATprove menunjuk baris dan memberi contoh nilai pemicu.

 high: range check might fail, cannot prove lower bound for X - Y
--> diff.adb:6:11
    6 |       Z := X - Y;
      |            ~~^~~
      + e.g. when X = 0
      and Y = 1
      + reason for check: result of subtraction must fit in the target type of the assignment
      + possible fix: add precondition (X >= Natural'First + Y) to subprogram at line 1
    1 |    procedure Diff (X, Y : in Natural; Z : out Natural) with
      |              ^

Baris + e.g. when adalah contoh tandingan (counterexample), yaitu satu kombinasi nilai masukan yang membuat check gagal, sehingga perbaikan dapat diarahkan langsung pada penyebabnya. Baris + possible fix bahkan menyarankan kontrak yang dapat ditambahkan. Selain keluaran pada layar, gnatprove menulis ringkasan seluruh hasil analisis proyek pada berkas gnatprove.out.

Kesalahan umum#

• Menganggap pesan medium: boleh diabaikan karena bukan high:. Tingkat keparahan hanya menyatakan keyakinan alat bahwa kegagalan itu mungkin terjadi, sedangkan seluruh check wajib terbukti atau dijustifikasi secara eksplisit. Perbaikannya, tuntaskan setiap pesan sampai hilang sebelum kode dianggap selesai.
• Menambah asersi hanya untuk membuat pesan hilang. Asersi yang selalu benar memang menghilangkan pesan, tetapi bukti yang dihasilkan tidak lagi menyatakan perilaku yang diinginkan. Perbaikannya, perkuat kontrak, misalnya dengan Pre yang menyempitkan rentang masukan seperti saran pada pesan di atas.
• Mengubah mode pemeriksaan demi kecepatan tanpa memahami akibatnya. Mode check tidak menjalankan flow analysis maupun proof, sehingga hasilnya bukan bukti kebenaran program. Perbaikannya, gunakan mode check hanya sebagai penyaring awal, lalu jalankan mode all pada titik pemeriksaan yang sesungguhnya.

Ringkasan#

• GNATprove berpijak pada berkas proyek .gpr yang sama dengan gprbuild, sehingga build dan verifikasi menggunakan satu daftar sumber.
• Mode pemeriksaan bertingkat dari check, check_all, flow, prove, sampai all, sedangkan --level mengatur kekuatan prover dari 0 sampai 4.
• Keluarannya terbagi atas error, warning, check message dengan tingkat low sampai high, dan information message, lengkap dengan contoh tandingan dan saran perbaikan.

Referensi#

• SPARK User’s Guide: Getting Started with SPARK — AdaCore — Contoh resmi pemanggilan GNATprove beserta keluaran flow analysis dan proof yang dikutip pada topik ini.
• SPARK User’s Guide: How to Run GNATprove — AdaCore — Penjelasan berkas proyek, mode pemeriksaan, dan switch level beserta provernya.
• SPARK User’s Guide: How to View GNATprove Output — AdaCore — Kategori pesan, bentuk check message, dan berkas ringkasan gnatprove.out.