\chapter{Formal Specification}

Seperti telah dijelaskan secara sepintas pada bab Pendahuluan,
proses desain dimulai dari sebuah spesifikasi.
Spesifikasi ini dibuat oleh pemberi pekerjaan yang kemudian
akan diimplementasikan oleh seorang (atau satu tim) implementor.

Spesifikasi dari sebuah sistem yang akan didesain dapat dituliskan
dalam bahasa Inggris (atau {\em natural language} lainnya) dan
kadang-kadang dilengkapi dengan diagram atau sketsa.
Namun spesifikasi dalam bahasa natural ini memiliki kelemahan:
\begin{itemize}
\item {\em ambiguous} atau memiliki banyak makna
\item sukar diproses secara otomatis ({\em mechanized})
\end{itemize}

Contoh suatu pernyataan atau spesifikasi yang {\em ambiguous} adalah
sebagai berikut. Jika kita pergi ke sebuah restoran,
ada sebuah pilihan:
\begin{quote}
{\em Sup atau sayur sudah termasuk dalam menu.}
\end{quote}
Apakah yang dimaksud adalah salah satu saja (sup saja,
atau sayur saja)? Ataukah keduanya?
Kata ``atau'' di sini sangat rancu. Dia mungkin tidak
tepat sama seperti {\em OR} dalam boolean logic
dimana keduanya boleh ada, akan tetapi
lebih tepat seperti {\em exclusive OR} atau {\em XOR}
dimana hanya salah satu yang dipilih tapi tidak
boleh dua-duanya.

Spesifikasi yang dituliskan dalam bahasa natural tadi,
karena kerancuannya, sulit untuk diproses secara otomatis
oleh sebuah komputer misalnya.
Jika kita dapat menggunakan notasi yang standar dalam penulisan
spesifikasi, mungkin proses selanjutnya bisa diotomatisasi
dengan lebih mudah.
Sebagai contoh, Kimia mempunyai standar baku untuk menuliskan
rumus-rumus Kimia.

{\em TODO: contoh-contoh notasi kimia}

Contoh lain yang dapat menunjukkan kemudahan notasi formal adalah
penulisan rumus matematik.
Sebagai contoh, {\em Fermat's Last Theorem} dapat dijabarkan dalam
kata-kata sebagai berikut:
\begin{quote}
{\em
Tidak ada empat bilangan bulat yang memenuhi persamaan
sebagai berikut. Bilangan pertama dipangkatkan bilangan keempat,
ditambah bilangan kedua dipangkatkan bilangan keempat, sama dengan
bilangan ketiga dipangkatkan bilangan keempat, dimana bilangan
keempat lebih besar dari dua.}
\end{quote}
Teorema di atas lebih mudah dituliskan sebagai berikut
\begin{quote}
Tidak ada bilangan bulat $x$, $y$, $z$ yang memenuhi persamaan\\
$x^n + y^n = z^n$, dimana $n > 2$.
\end{quote}


Untuk mengatasi masalah spesifikasi yang tidak jelas
maka dibuatlah pendekatan yang disebut {\em formal specification}.
Hal ini dilakukan dengan menggunakan notasi formal.


\section{Notasi formal}
Formal specification menggunakan notasi formal yang memiliki basis
matematik serta memiliki {\em syntax} dan {\em sematics} yang jelas.
Seringkali notasi formal ini memiliki format yang dapat diproses
oleh komputer ({\em machine readable format}).
Tujuannya adalah membuat proses verifikasi menjadi otomatis,
yaitu melakukan perbandingan antara spesifikasi dengan implementasi
secara otomatis oleh komputer.

Pada bagian ini akan dibahas beberapa contoh notasi formal.
Pemilihan notasi bergantung kepada beberapa hal:
\begin{itemize}
\item expresiveness
\item kemudahan penggunaan (easy to use)
\end{itemize}
Kemampuan ekspresi yang tinggi memudahkan untuk menulis spesifikasi
sistem yang kompleks. Namun seringkali hal ini diimbangi dengan
ketidak-mudahan untuk menuliskan spesifikasi tersebut.
Sebagai contoh, higher-order logic memiliki kemampuan ekspresi
yang sangat fleksibel. Namun untuk menggunakan higher-order logic
ini membutuhkan pengetahuan dan pengalaman yang tinggi
({\em steep learning curve}).
Kesulitan ini memudahkan orang membuat kesalahan dalam menuliskan
spesifikasi, atau spesifikasi itu susah dibaca dan dimengerti.

\section{CSP}
\index{CSP}
{\em Communicating Sequential Processes (CSP)} merupakan sebuah
{\em formalism} yang dikembangkan oleh 
C.A.R. Hoare~\cite{hoare78,hoare95}.\index{Hoare}
CSP ini memiliki kemampuan ekspresi yang sangat baik.
Namun sayangnya belum ada tools CSP yang mudah digunakan dan tersedia
secara gratis. (Lihat bagian PROMELA.)

Pada bahasa pemrograman tingkat tinggi, {\em assignment} merupakan sebuah
hal yang sudah dimengerti dengan baik. Akan tetapi operasi {\em input}
dan {\em output} belum dimengerti dengan baik.
{\em Assignment} berhubungan dengan {\em state} di dalam (internal) sebuah
sistem, sementara {\em input} dan {\em output} berhubungan dengan state
di luar (external). CSP mencoba memberikan sebuah notasi untuk input dan
output ini.

Program konvensional ditargetkan untuk dijalankan pada satu prosesor.
Saat ini mulai banyak sistem yang menggunakan prosesor lebih dari satu
(multiprocessor), dimana prosesor ini saling berkomunikasi satu dengan
lainnya.
Komunikasi antar prosesor ini harus dapat dijabarkan dengan mudah dan
tidak {\em ambiguous}. Itulah sebabnya perlu ada notasi input dan output.

{\em Communicating Sequential Processes} (CSP) mencoba memecahkan masalah 
notasi untuk menjabarkan (menspesifikasi) sistem yang terdiri dari beberapa 
proses, dimana pada setiap proses ini ada program yang sifatnya berurut (sequential).
Proses-proses ini saling berkomunikasisatu dengan lainnya melalui input dan output.
Contoh penggunaan notasi ini akan dijelaskan lebih lanjut.

CSP mengusulkan sebuah solusi, yaitu:
\begin{itemize}
\item {\em Dijkstra's guarded command};
\item Perintah parallel, yang juga berdasarkan kepada {\em Dijkstra's} parbegin;
\item Perintah input dan output dengan format yang sederhana;
\item dan gabungan hal di atas.
\end{itemize}

Notasi dari CSP bisa dituliskan dengan menggunakan notasi BNF\index{BNF}.

\subsection{Input dan Output}
Perintah atau operator input dan output digunakan untuk menspesifikasikan
komunikasi antara dua proses yang berjalan bersamaan ({\em concurrent}).
Jika kita memiliki dua proses, P1 dan P2, yang berjalan bersamaan dan
saling berkomunikasi maka komunikasinya dapat dilakukan dengan:
\begin{itemize}
\item Perintah input di proses P1 yang menspesifikasikan proses P2
   sebagai sumbernya ({\em source}). Perintah input dituliskan dengan
   operator tanda tanya ({\bf ?}).
\item Perintah output di proses P2 yang menspesifikasikan proses P1
   sebagai tujuannya ({\em destination}). Perintah output dituliskan
   dengan operator tanda seru ({\bf !}).
\item Variabel target cocok dengan nilai ({\em value}) yang dituliskan
   pada ekspresi perintah output.
\item Perintah input berhenti (gagal, {\em fail}) apabila sumber data
   dihentikan ({\em terminated}).
\item Perintah output akan gagal bila proses target berhenti (terminated).
\end{itemize}

Beberapa contoh penggunaan notasi dari CSP antara lain:
\begin{itemize}
\item {\bf cardreader?cardimage}\\
   baca data dari proses ``cardreader'' dan masukkan ke variabel ``cardimage''
\item {\bf lineprinter!lineimage}\\
   kirimkan data dari variabel ``lineimage'' ke proses ``lineprinter''
\item {\bf [cardreader?cardimage] $\parallel$ [lineprinter!lineimage]}\\
   Notasi di atas menunjukkan dua perintah secara paralel dan berhenti
   apabila kedua operasi di atas telah selesai.
\item {\bf X?(x,y)}\\
   Baca dari proses X dua data yang akan dimasukkan ke variabel $x$ dan $y$.
   Data yang dikirimkan harus sama jenisnya (tipenya) dengan kedua variabel
   tersebut. Jika tipenya berbeda, maka proses input tersebut tidak bisa
   dieksekusi.
\item {\bf DIV!(3*a+b,13)}\\
   Kirim ke proses DIV dua buah data, dimana data yang pertama adalah
   nilai hasil evaluasi $3*a + b$ sementara nilai kedua adalah 13.
\item Kedua perintah di atas dapat digabungkan menjadi satu sehingga berarti
   $(x,y)=(3*a+b,13)$, yaitu masukkan hasil evaluasi $3*a+b$ ke variabel $x$
   dan angka 13 ke variabel $y$.
\item {\bf console(i)?c}\\
   Baca data dari {\em console} nomor $i$, dimana angka $i$ merupakan integer.
\item {\bf console(j-1) ! ``A''}
\item {\bf X(i)?V()}\\
   Baca dari proses $X(i)$ sebuah sinyal $V()$. Sinyal ditandai dengan tanda kurung. 
   Jika sinyal tersebut tidak bisa dibaca, misalnya proses $X(i)$ mengirimkan 
   sinyal lain, maka ekspresi tersebut tidak dapat dieksekusi.
\item {\bf sem!P()}
\end{itemize}

(Pada versi berikutnya akan saya tambahkan informasi mengenai notasi CSP di sini.)
Penjelasan mengenai notasi CSP dibahas dengan lebih lengkap pada paper Hoare~\cite{hoare78}.


\section{PROMELA dan SPIN}
\index{PROMELA}
PROMELA merupakan sebuah bahasa yang dikembangkan oleh Gerrard 
Holzmann~\cite{holzmann91} untuk memodelkan sistem, 
khususnya protokol komputer.
PROMELA, yang merupakan kependekan dari PROcess MEta LAnguage,
menggunakan basis CSP, bahasa C, dan SDL
({\em Specification Description Language}, yang akan dibahas tersendiri
pada bagian terpisah).

Selain mengembangkan bahasanya, Holzmann juga mengembangkan sebuah
tools yang diberi nama SPIN untuk melakukan
validasi -- tepatnya {\em model checking} --
terhadap spesifikasi yang ditulis dalam bahasa PROMELA.
Bahkan, sebetulnya buku dan makalah dari Holzmann lebih banyak
difokuskan kepada algoritma-algoritma yang dituangkan dalam
bentuk tools SPIN tersebut.

\subsection{Bahasa PROMELA}
Pada bagian berikut akan dijelaskan secara sepintas mengenai bahasa
PROMELA\footnote{
Informasi mengenai PROMELA dan SPIN dapat diperoleh dari
situs http://spinroot.com}.
Informasi yang lebih lengkap dapat dilihat pada buku referensi.

Secara singkat, di dalam bahasa PROMELA ada tiga buah {\em objects};
\begin{itemize}
\item {\em process}
\item {\em message channels}
\item variabel (global atau lokal)
\end{itemize}
Dalam implementasinya, obyek ini ditranslasikan menjadi
{\em Finite State Machine} (FSM).

Deskripsi dalam bahasa PROMELA ditulis dalam  bentuk {\em statement}.
Dalam PROMELA tidak ada perbedaan antara {\em conditions}
dan {\em statements}.
Eksekusi dari {\em statement} ini bergantung kepada sifat
{\em executability}-nya.
Statement ini bisa dijalankan ({\em executable}) atau terhalang
({\em blocked}) bergantung kepada nilai dari variable atau isi
dari message channel.
Jika kondisinya benar ({\em holds}) maka statement akan dieksekusi.
Jika tidak, maka statement akan terhenti ({\em blocked}) sampai kondisi
menjadi benar.
Jika keterangan di atas agak membingungkan, jangan khawatir.
Pada bagian berikut kita akan melihat contoh-contoh.

Ada enam (6) jenis data yang sudah terdefinisi di PROMELA;
\begin{itemize}
\item {\em bit} (ukuran implementasi 1 bit)
\item {\em bool} (1 bit)
\item {\em byte} (8 bit)
\item {\em short} (16 bit)
\item {\em chan} (bergantung kepada data).
   Jenis data {\em chan} ini digunakan untuk mengimplementasikan
   message channel, yaitu sebuah obyek yang dapat menyimpan beberapa
   nilai yang dijadikan satu.
\end{itemize}

Contoh penggunaan jenis data di atas:
\begin{verbatim}
bool flag;
int  state;
byte pesan;
\end{verbatim}

Variabel data dinyatakan dalam {\em array} seperti contoh di bawah ini:
\begin{verbatim}
byte status[N];
status[0] = status[2] + 7 * status[3*n]
\end{verbatim}

Perlu dicatat bahwa {\em declaration} dan {\em assignment} selalu
dapat dieksekusi, jadi selalu {\em executable}.
Tanda titik koma (; atau {\em semi-colon}) merupakan tanda
pemisah statement atau {\em statement separator}.
Dia bukan {\em statement terminator} sehingga pada statement yang
terakhir tidak perlu diakhiri dengan tanda titik koma ini.
Ada dua {\em statement separator} dalam PROMELA, yaitu titik koma
dan tanda panah $->$.

Proses di dalam PROMELA didefinisikan dengan menggunakan keyword
{\em proctype}, seperti contoh di bawah ini.
\begin{verbatim}
proctype A() { byte state; state = 3}
\end{verbatim}
Contoh di atas menunjukkan definisi dari proses A,
dimana di dalamnya ada sebuah variabel lokal yang bernama {\em state}.
Kemudian variabel ini kita masukkan nilai ``3''.

Contoh lain lagi:
\begin{verbatim}
byte state = 2;
proctype A() { (state == 1) -> state = 3}
proctype B() { state = state  1}
\end{verbatim}
Pada contoh ini kita melihat adanya sebuah variabel global yang
bernama {\em state} dan pendefinisian dua buah proses, yaitu
prosess ``A'' dan ``B''.
Perhatikan bahwa pada proses A terdapat sebuah {\em guarded command}
dimana eksekusi dari statement tersebut bergantung kepada nilai
dari variabel {\em state}.

Contoh di atas hanya menunjukkan deskripsi dari proses tetapi
belum menunjukkan interaksi antar proses tersebut selain melalui
global variabel.
Proses diinisialisasi dengan menggunakan perintah {\em run}
seperti contoh di bawah ini:
\begin{verbatim}
init { run A(); run B() }
\end{verbatim}
Perintah {\em init} ini sama seperti perintah {\em main()}
pada bahasa C.

Message channel digunakan untuk mengkomunikasikan data antar proses.
Di bawah ini ada beberapa contoh penggunaan message channel.
\begin{verbatim}
chan a, b; chan c[3];
chan qname = [16] of { byte, int, chan, byte};
qname!expr;
qname?msg
\end{verbatim}

Mirip dengan CSP, nilai dari sebuah variabel dapat dikirimkan melalui
channel dengan menggunakan tanda seru. Dalam contoh di atas, nilai
dari ekspresi {\em expr} akan dikirimkan melalui channel ``qname''.
Sementara itu baris terakhir menunjukkan bahwa sebuah pesan dari
kepala ``qname'' dibaca dan disipan dalam variabel ``msg''.
Channel bersifat FIFO (First In, First Out).

PROMELA memiliki tiga {\em control flow};
{\em case selection}, {\em repetition}, dan {\em unconditional jump}.

Pemilihan atau {\em case selection} dilakukan dengan menggunakan
kata kunci {\em if if} dan tanda titik dua (:) dua kali.
\begin{verbatim}
if
:: (a != b) -> option1
:: (a == b) -> option2
fi
\end{verbatim}
Dalam contoh di atas, statement pertama berfungsi sebagai guard,
yang ikut menentukan sifat {\em executable} dari statement tersebut.
Dalam satu saat dipilih salah satu dari pilihan tersebut dengan
syarat bahwa statement tersebut executable.
Dalam contoh di atas, hanya salah satu statement akan dipilih bergantung
kepada guard yang ada, yaitu bergantung kepada nilai variabel
``a'' dan ``b''.
Namun dalam contoh lain bisa terjadi bahwa 
ada lebih dari satu pilihan yang bisa dipilih.
Untuk kasus ini akan dipilih salah satu secara random.
\begin{verbatim}
if
:: (x > y) -> maks = x
:: (y > x) -> maks = y
:: (x == y) -> maks = x
:: (x != y) -> flag = 1
fi
\end{verbatim}
Dalam contoh di atas jika $x = 5$ dan $y = 7$ maka ada dua pilihan
yang dapat dipilih, yaitu pilihan kedua -- dengan guard $(y > x)$ --
atau pilihan keempat -- dengan guard $(x != y)$.
Pilihan akan dipilih secara random.

Jika semua pilihan tidak ada yang {\em executable}, maka proses
akan terhambat (blocked) sampai ada salah satu yang bisa dieksekusi.

Pengulangan ({\em repetition}) dilakukan dengan keyword {\em do od}.
\begin{verbatim}
byte count;
proctype counter()
{
do
:: count = count +1
:: count = count -1
:: (count == 0) -> break
od
}
\end{verbatim}

Di dalam PROMELA diperkenankan untuk melakukan {\em unconditional jump}
dengan kata kunci {\em goto}. 
Flow akan diteruskan kepada bagian (label) yang dituju oleh goto.
Dalam contoh di bawah ini apa bila nilai $x$ sama dengan $y$ maka
flow akan diteruskan ke label ``done'' yang kemudian dilanjutkan
dengan perintah {\em skip} yang tidak melakukan apa-apa.
\begin{verbatim}
proctype Euclid(in x, y)
{
do
:: (x > y) -> x = x  y
:: (x < y) -> y = y  x
:: (x == y) -> goto done
od
done:
     skip
}
\end{verbatim}


\subsection{Tool SPIN}
SPIN merupakan sebuah tool yang dapat digunakan untuk melakukan
{\em model checking} terhadap sistem yang ditulis dalam bahasa PROMELA.
SPIN ditulis dalam bahasa C dan tersedia {\em source code}-nya untuk
sistem UNIX dan Windows.


\section{Higher Order Logic}
\section{Petri nets}
Informasi mengenai petri nets dapat diperoleh dari berbagai sumber
seperti:


Ada tools untuk mensimulasi dan menganalisa Petri nets. Salah
satu tools yang cukup baik adalah Design/CPN.
Sementara itu perbandingan antara Petri net tools dapat dilihat di

http://home.arcor-online.de/wolf.garbe/petrisoft.html

Tutorial mengenai Petri nets dapat dilihat di

http://www.iai.inf.tu-dresden.de/ms/lvbeschr/vwahl\_petri.html

\section{Synchronized Transition}
\section{Lain-lain: CCS, Estelle, Lotos, VDM, Z}
Selain formalism yang dijelaskan pada bagian sebelumnya,
ada beberapa notasi lain yang juga memiliki banyak pengikut.
Notasi tersebut antara lain:
\begin{itemize}
\item Calculus of Communicating System (CCS) yang dikembangkan
   oleh R. Milner~\cite{milner}
\end{itemize}