Buku ini menjelaskan hasil Riset Unggulan Terpadu Internasional (RUTI) 2003 — 2005 di Fasilkom UI yang disponsori oleh Kementerian Riset dan Teknologi RI tentang pengembangan teknologi untuk membangun aplikasi basis data kritis. Teknologi yang dikembangkan adalah dengan memasukkan unsur pembuktian logik sehingga spesifikasi suatu piranti lunak lebih terjamin kebenarannya secara matematis.
Secara spesifik buku ini
• menjelaskan Lingu — suatu bahasa spesifikasi baru untuk aplikasi basis data. Penuilsan dalam bahasa ini dapat diverifikasi dengan bantuan theorem prover HOL.
• 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.
• membenikan wawasan baru dalam membangun piranti lunak dan memverifikasi program dengan menggunakan Lingu, dengan studi kasus menggunakan Student Entrance Test (SET).
• Melakukan analisis perbandingan Lingu dengan bahasa lain seperti SQL dan Metode B.