Proses Verifikasi Piranti Lunak Basis Data dengan Lingu dan Theorem Prover Hol

Secara spesifik ruang lingkup buku ini adalah:

1. Menjelaskan Lingu – suatu bahasa spesifikasi baru untuk aplikasi basis data. Penulisan dalam bahasa ini dapat diverifikasi dengan bantuan theorem prover HOL.

2. Mengulas contoh bagaimana suatu aplikasi basis data dapat dituliskan dalam Lingu dan memverifikasinya. Tujuan dari verifikasi program adalah memberikan jaminan bahwa program yang dibuat telah sesuai dengan spesifikasi yang diberikan. Dengan adanya jaminan tersebut, pengembang dapat melanjutkan proses pembuatan piranti lunak hingga tahap terakhir. Saat ini, Lingu hanya memfokuskan diri pada aplikasi basis data.

3. Memberikan wawasan baru dalam membangun piranti lunak dan memverifikasi program dengan menggunakan Lingu. Studi kasus menggunakan Test Penerimaan Mahasiswa Baru – Student Entrance Test (SET).

4. Melakukan analisis perbandingan Lingu dengan bahasa lain seperti SQL dan Metode B.

Buku ini dapat dipakai sebagai salah satu acuan perkuliahan Rekayasa Perangkat Lunak yang membutuhkan dukungan verifikasi kebenaran suatu spesifikasi. Karena mensyaratkan pengetahuan logika yang sangat kuat, maka buku ini akan tepat menjadi acuan mahasiswa S1 bila sudah di tingkat akhir atau bagi mahasiswa pascasarjana tingkat awal.