Rabu, 04 Juli 2012

Metode Formal

Mengapa seorang software engineers PERLU memiliki kemampuan matematika yang mumpuni? Pertanyaan ini seringkali ditanyakan oleh mahasiswa jurusan informatika dan masyarakat umum. Sepertinya telah terjadi salah-pemahaman mengenai keilmuan Informatika itu sendiri. Masyarakat awam "memiliki" pemahaman bahwa informatika terkait dengan Facebook, Twitter dan Internet Marketing, sedangkan mahasiswa informatika sering memahami keilmuan informatikan itu sebagai Gaming dengan berbagai bentuknya. Semua itu merupakan pandangan yang keliru.

Beberapa waktu lalu saya telah menulis tentang kemampuan matematika dasar yang harus dimiliki oleh seorang software engineer. Tulisan itu dapat dibaca pada link ini:

Pada bagian ini, saya akan menulis tentang Formal Methods atau Metode Formal. Sebagai pengantar, maka perlulah dikemukakan apa itu formal methods tersebut ...
Formal methods is the term applied to the analysis of software (and computer hardware) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include denotational semantics, axiomatic semantics, operational semantics, and abstract interpretation.

Jika diterjemahkan maka akan seperti ini:
Metode formal adalah istilah yang diterapkan pada analisis perangkat lunak (dan perangkat keras komputer) yang hasilnya diperoleh murni melalui penggunaan metode matematika ketat. Teknik-teknik matematika yang digunakan meliputi semantik denotational, semantik aksiomatik, semantik operasional, dan interpretasi abstrak.


Formal Methods merupakan bagian pembahasan pengembangan perangkat lunak yang makin berkembang sekarang ini. Mahasiswa jurusan informatika harus memahami konsep dan implementasi Formal Methods dalam pengembangan perangkat lunak, dan untuk itu dibutuhkan kemampuan matematika dasar dan lanjut yang menyeluruh.

Misalnya kita dapat melihat apa yang dimaksud dengan interpretasi abstrak:
Abstract interpretation models the effect that every statement has on the state of an abstract machine (i.e., it 'executes' the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviours of the system: the abstract system is thus made simpler to analyze, at the expense of incompleteness (not every property true of the original system is true of the abstract system).
Use of assertions in program code as first suggested by Hoare logic. There is tool support for some programming languages (e.g., the SPARK programming language (a subset of Ada) and the Java Modeling Language — JML — using ESC/Java and ESC/Java2, Frama-c WP (weakest precondition) plugin for the C language extended with ACSL (ANSI/ISO C Specification Language).

atau dalam terjemahannya ...
Interpretasi abstrak memodelkan efek dari setiap pernyataan pada keadaan mesin abstrak (yaitu, 'mengeksekusi' perangkat lunak berdasarkan sifat matematis dari setiap pernyataan dan deklarasi). Mesin abstrak memperkirakan perilaku sistem: sehingga dapat digunakan untuk menganalisis, dengan model sistem yang tidak lengkap (yakni tidak setiap properti dari sistem yang asli dimodelkan pada sistem abstrak). 
Penggunaan pernyataan dalam kode program sebagai pertama kali diusulkan oleh logika Hoare. Ada alat dukungan untuk beberapa bahasa pemrograman (misalnya, pemrograman SPARK bahasa (subset dari Ada) dan Modeling Language Jawa - JML - menggunakan ESC / Jawa dan ESC/Java2, Frama-c WP (prasyarat paling lemah) plugin untuk C bahasa diperpanjang dengan ACSL (ANSI / ISO C Language Specification)).

Matematika Diskrit adalah salah satu mata kuliah yang mendasari konsep-konsep metode formal. Sedangkan Kalkulus, Aljabar Linier, Probabilitas dan Statistik serta Metode Numerik memberikan latar belakang keteknikan untuk formulasi permasalahan, pemodelan masalah dan penyusunan algoritma penyelesaian masalah, untuk selanjutnya disalin dalam bahasa coding.

Berikut ini adalah slide kuliah tentang Formal Method:
Diposting oleh di
Label:

2 komentar:

Langganan: Posting Komentar (Atom)