Jalur ini mengajarkan pemrograman Ada 2022 dari nol sampai mampu membangun, menguji, dan membuktikan program yang nyata. Ciri utamanya adalah menjadikan kompilator sebagai peninjau kode pertama: tipe yang membawa makna domain, kontrak pada setiap subprogram, tasking yang dibangun ke dalam bahasa, serta subset SPARK yang mengubah pengujian menjadi pembuktian. Seluruh contoh dijalankan dengan GNAT dan dikelola melalui Alire, sehingga cukup terminal dan GNAT 14 atau lebih baru untuk mengikuti jalur ini dari awal sampai akhir.
Ada
Jalur lengkap pemrograman Ada 2022: pengetikan kuat, kontrak subprogram, tasking, dan pembuktian SPARK dengan toolchain GNAT dan Alire.
0/0 selesai
Modul pembuka: latar munculnya Ada, penyiapan toolchain Alire dan GNAT, serta lanskap kompilatornya.
- Apa itu Ada?Lahirnya Ada di lingkungan Departemen Pertahanan Amerika Serikat serta karakter bahasanya yang menempatkan kebenaran program sebagai tujuan.
- PenyiapanMemasang toolchain Ada melalui pengelola package Alire dan memverifikasi kompilator GNAT yang tersedia.
- Lanskap compilerPeta pilihan kompilator Ada: GNAT di dalam GCC dari distribusi dan rilis tahunan dari AdaCore melalui Alire.
Fondasi bahasa: deklarasi, tipe integer, subtipe, enumerasi, dan ekspresi dengan aturan pengetikan kuat.
- DeklarasiKonstanta bernama, deklarasi variabel, dan kewajiban inisialisasi yang menegakkan pengetikan kuat sejak awal.
- Tipe integerRentang nilai yang melekat pada tipe integer beserta luapan yang tertangkap sejak rancangan.
- Subtipe dan tipe turunanPerbedaan subtipe sebagai tampilan terkendala dan tipe turunan sebagai tipe baru yang sesungguhnya.
- EnumerasiTipe enumerasi dengan nilai buatan pengguna serta atribut Pos dan Val untuk konversi.
- EkspresiOperator pada ekspresi Ada, bentuk evaluasi short-circuit, dan perbedaan rem dengan mod.
Fungsi dan prosedur dengan mode parameter, kontrak Pre dan Post, predikat, serta exception.
- Fungsi dan prosedurPembedaan fungsi dan prosedur beserta mode parameter in, out, dan in out.
- Aspek Pre dan PostAspek Pre dan Post sebagai kontrak subprogram yang diperiksa saat run time.
- PredikatPredikat subtipe yang menjaga setiap nilai tetap valid pada batas yang ditetapkan.
- ExceptionMekanisme exception, penanganan Constraint_Error, dan pemulihan yang disengaja.
Struktur program berbasis package: spesifikasi, badan, tipe privat, unit anak, dan disiplin nama.
- Spesifikasi dan badanPemisahan spesifikasi dan badan package serta ketergantungan klien pada spesifikasi.
- Tipe privatTipe privat dengan representasi tersembunyi dan operasi yang diekspor.
- Unit anakUnit anak untuk membangun struktur hierarkis pada program besar.
- Nama dan klausa useNama terkualifikasi sebagai pilihan utama dan disiplin penggunaan klausa use.
Record, record berdiskriminan, array, tipe akses, dan klausul representasi.
- RecordRecord dengan bidang bernama, nilai bawaan, dan penulisan agregat record.
- Record berdiskriminanRecord berdiskriminan sebagai record varian dengan kendala yang diperiksa secara statis.
- ArrayArray dengan batas yang menjadi bagian tipenya serta pemotongan slice.
- Tipe aksesTipe akses pool-specific dan general beserta aturan scope pada manajemen memori.
- Klausul representasiKlausul representasi untuk tata letak bit-eksak menuju perangkat keras dan protokol.
Parameterisasi tipe melalui subprogram dan package generik hingga container standar.
- Subprogram generikSubprogram generik yang diparameterisasi atas tipe.
- Package generikPackage generik sebagai abstraksi pakai ulang yang diinstansiasi per tipe.
- Parameter formalParameter formal berupa tipe berkendala, subprogram, dan package.
- Container standarContainer standar Ada.Containers: vector, hash map, dan list.
Konkurensi bawaan bahasa: task, rendezvous, objek terlindungi, delay dan select, serta profil Ravenscar.
- Task dan rendezvousTask sebagai aktivitas konkuren bawaan bahasa yang bertemu melalui entry.
- Objek terlindungiObjek terlindungi untuk data bersama terkapsulasi dengan barrier entry.
- Delay dan selectPenundaan waktu dengan delay dan penerimaan entry selektif melalui select.
- Profil RavenscarProfil Ravenscar sebagai tasking deterministik untuk deployment kritis.
Subset SPARK, alur kerja GNATprove, invarian loop, dan kode ghost.
- Subset SPARKSubset SPARK dari Ada: bagian yang dibuang dan alasan pembuangannya.
- Alur kerja GNATproveAlur kerja GNATprove untuk menjalankan prover dan membaca hasil verifikasi.
- Invarian loopInvarian loop agar loop dapat ditangani prover.
- Kode ghostKode ghost: konstruksi khusus pembuktian yang lenyap saat build.
Berkas proyek GPRbuild, pengujian unit AUnit, dan analisis statis.
- Berkas proyekBerkas proyek GPRbuild: susunan sumber, konfigurasi, dan switch.
- Pengujian unitPengujian unit dengan AUnit dan kasus uji berbasis kontrak.
- Analisis statisAnalisis statis dengan aturan GNATcheck dan standar pengodean.
Antarmuka C, akses perangkat keras, operasi unchecked, dan penjadwalan waktu nyata.
- Antarmuka CAntarmuka ke C dengan pragma Import dan Export serta Interfaces.C.
- Akses perangkat kerasAkses perangkat keras melalui klausul address, variabel volatile, dan interrupt.
- Operasi uncheckedOperasi unchecked untuk konversi dan dealokasi yang dipakai secara sengaja.
- Penjadwalan waktu nyataPenjadwalan waktu nyata: prioritas, ceiling locking, dan kebijakan dispatching.
Proyek akhir terpandu: pemilihan proyek dan perancangan arsitektur lebih dahulu.
- Pemilihan proyekPemilihan proyek akhir: pengendali lift atau sistem interlocking lampu lalu lintas.
- Arsitektur lebih duluPerancangan arsitektur lebih dahulu: task, state terlindungi, dan kontrak digambar di muka.