csp[通信順序進程]

Communication Sequential Process （簡稱CSP）是著名計算機科學家C.A.R.Hoare為解決並發現象而提出的代數理論，是一個專為描述並發系統中通過訊息交換進行互動通信實體行為而設計的一種抽象語言。

簡介

可用FDR（Failure Divergence Refinement）驗證設計是否正確。

在該語言中，一個並發系統由若干並行運行的順序進程組成，每個進程不能對其他進程的變數賦值。進程之間只能通過 一對通信原語實現協作：Q->x表示從進程Q輸入一個值到變數x中；P<-e表示把表達式e的值傳送給進程P。當P進程執行Q->x， 同時Q進程執行P<-e時，發生通信，e的值從Q進程傳送給P進程的變數x。後來出現的實用程式語言OCCAM即以CSP為基礎發展而成。

1984年S．Brooks，C．A．R．Hoare和W．Roscoe提出CSP理論(TCSP)。這是一個代數演算系統，其基本成分是事件(或動 作)。進程由事件和一組運算元構造而成。

典型的運算元有：→(前綴)，|(外部非確定性選擇)，\e(事件隱蔽)，以及遞歸等。

例子

例：(自動售貨機) VM=coin→(choc→VM|coffee→VM)， CUST：coin→(choc→CUST coffee→CUST) 這裡定義了兩個進程：VM(售貨機)和CUST (顧客)。售貨機在接受了硬幣coin後，可按顧客的要求支付choc或coffee。顧客在付了硬幣後，或者想要choc，或者想要coffee，其選 擇不受外界影響。