計(jì)算機(jī)文化基礎(chǔ)系列常識(shí)-圖靈獎(jiǎng)獲獎(jiǎng)?wù)呓榻B連載(十二)

計(jì)算機(jī)文化基礎(chǔ)系列常識(shí)-圖靈獎(jiǎng)獲獎(jiǎng)?wù)呓榻B連載（十二）米凱爾，拉賓(MichaelO．Rabin)米凱爾，拉賓(MichaelO．Rabin)達(dá)納·斯科特(DanaStewardScott)——非確定性有限狀態(tài)自動(dòng)機(jī)理論的開(kāi)創(chuàng)者

1976年度的圖靈獎(jiǎng)由當(dāng)時(shí)在以色列希伯萊大學(xué)任教授的米凱爾，拉賓(MichaelO．Rabin)和在英國(guó)牛津大學(xué)任數(shù)理邏輯教授的達(dá)納·斯科特(DanaStewardScott)共同獲得。拉賓和斯科特是師兄弟，兩人在20世紀(jì)50年代中期先后師從著名的邏輯學(xué)家和計(jì)算機(jī)專家阿隆索·邱奇(AlonzoChurch，他因與Curry一起發(fā)明了λ-演算以及提出了“任何計(jì)算，如果存在一有效過(guò)程，它就能被圖靈機(jī)所實(shí)現(xiàn)”這一被稱為“邱奇論題”的命題而聞名于世)，并在有限自動(dòng)機(jī)及其判定問(wèn)題的研究中進(jìn)行合作，奠定了非確定性有限狀態(tài)自動(dòng)機(jī)的理論基礎(chǔ)。之后，他們的研究方向不盡相同，拉賓側(cè)重于計(jì)算理論，而斯科特側(cè)重于邏輯學(xué)在計(jì)算機(jī)科學(xué)中的應(yīng)用，在各自的領(lǐng)域中又分別獲得重大成果，作出了創(chuàng)造性貢獻(xiàn)。拉賓1931年9月1日生于德國(guó)的布雷斯勞(Breslau，第二次世界大戰(zhàn)以后成為波蘭的城市并改名為弗羅茨瓦夫)。他父親是一名猶太教教士，也是一位博士，在當(dāng)時(shí)很著名的布雷斯勞神學(xué)院教猶太歷史和哲學(xué)，還當(dāng)過(guò)院長(zhǎng)。拉賓的母親也是知識(shí)分子，有文學(xué)博士頭銜，年輕時(shí)即開(kāi)始從事兒童文學(xué)的創(chuàng)作。納粹希特勒上臺(tái)以后，拉賓的父親因?yàn)樵?jīng)在俄羅斯呆過(guò)，憑著政治敏感性，預(yù)感到會(huì)有動(dòng)蕩和麻煩，曾建議神學(xué)院遷往耶路撒冷，未獲同意，于是全家于1935年遷回了巴勒斯坦，躲過(guò)了一劫。1948年以色列建國(guó)以后，他們成為以色列公民。

拉賓在瀕臨地中海的港口城市海法度過(guò)了他的童年和少年時(shí)代。由于閱讀了著名微生物學(xué)家保羅·德克呂夫(PaulDeKmif)所著的《微型獵人》一書(shū)，激起了拉賓的想象，幻想自己成為微生物學(xué)家。一次他和比他高好幾班的學(xué)生比試解歐幾里德幾何題，他贏了他們，這又使他對(duì)數(shù)學(xué)產(chǎn)生了興趣，因此，從萊利學(xué)院(RealiCollege)畢業(yè)以后，他進(jìn)入希伯萊大學(xué)學(xué)習(xí)數(shù)學(xué)，在那里，他通過(guò)數(shù)學(xué)家克林(S．C．Kleene，因提出不動(dòng)點(diǎn)定理——theoremonfixpoint及正則集定理一theoremonregularset而聞名于世)所著的《元數(shù)學(xué)》一書(shū)首次接觸到圖靈關(guān)于可計(jì)算性的概念和圖靈機(jī)這一理論計(jì)算模型，立即被深深吸引。但為了打好自己的數(shù)學(xué)墓礎(chǔ)，他的碩土論文沒(méi)有以此為課題，而選擇了當(dāng)時(shí)由德國(guó)女?dāng)?shù)學(xué)家埃米·諾特(EmmyNoether，1882—1932)創(chuàng)立不久的抽象代數(shù)中關(guān)于可交換環(huán)理論中的一個(gè)問(wèn)題。獲得數(shù)學(xué)碩士學(xué)位以后，拉賓去了美國(guó)，因?yàn)?0世紀(jì)50年代初，以色列建國(guó)伊始，經(jīng)濟(jì)與科技都還不夠發(fā)達(dá)，很少有人研究計(jì)算這類問(wèn)題，甚至連計(jì)算機(jī)都沒(méi)有。拉賓到美國(guó)后，先在賓夕法尼亞大學(xué)，后來(lái)轉(zhuǎn)到普林斯頓大學(xué)攻讀博士學(xué)位。拉賓的博士論文課題將他所熟悉的抽象代數(shù)和他感興趣的可計(jì)算性問(wèn)題聯(lián)系在一起：群(GROUP)的可計(jì)算性問(wèn)題。拉賓在論文中證明了與群有關(guān)的許多問(wèn)題，如群是否符合交換律等，都是不能由計(jì)算機(jī)解答的。但是使拉賓成名的并非其博士論文而是源于IBM研究中心于1957年向他和他的師弟斯科特提供的一份暑期工作。公司允許他們作他們感興趣的任何工作，于是拉賓和斯科特就聯(lián)手研究圖靈提出的計(jì)算模型，也就是圖靈機(jī)。圖靈機(jī)是一種禁止往磁帶上寫(xiě)的計(jì)算機(jī)，叫有限狀態(tài)自動(dòng)機(jī)(finitestateautomata，縮寫(xiě)FSA)。圖靈在研究這種機(jī)器時(shí)的基本信條是：機(jī)器在輸入相同時(shí)，其“心智狀態(tài)”也相同，即對(duì)于具有給定指令集的機(jī)器而言，一定輸入的機(jī)器總是按同一方式運(yùn)行的。拉賓和斯科特認(rèn)為，這種具有“確定性”行為的機(jī)器帶來(lái)了局限性。因此，他們定義了一種新的、“非確定性”的有限狀態(tài)自動(dòng)機(jī)(nondeterministicfinitestateautomata，縮寫(xiě)為NDFSA)，這種機(jī)器在讀取到一定的輸入后，有一個(gè)可以進(jìn)入的可能的新的狀態(tài)的“菜單”可供選擇，這樣對(duì)給定的輸入計(jì)算便不單一了，每個(gè)選擇代表一種可能的計(jì)算。拉賓和斯科特將圖靈的有限狀態(tài)自動(dòng)機(jī)從確定性一種形態(tài)擴(kuò)展到非確定性的另一種形態(tài)，極大地推動(dòng)了有限狀態(tài)自動(dòng)機(jī)理論的發(fā)展。雖然非確定性有限狀態(tài)自動(dòng)機(jī)的能力并不比確定性的有任何增加(拉賓和斯科特自己已經(jīng)證明任何可以用非確定性機(jī)器解決的問(wèn)題都可以在確定性機(jī)器上解決，而且提出了將非確定性機(jī)器轉(zhuǎn)換為確定性機(jī)器的方法問(wèn)題)，但是它可以簡(jiǎn)化機(jī)器描述和加快解題速度。后來(lái)的實(shí)踐證明，非確定性有限狀態(tài)自動(dòng)機(jī)在機(jī)器翻譯、文獻(xiàn)檢索和字處理程序等應(yīng)用中都起了重要的作用。拉賓和斯科特的研究成果過(guò)了兩年才在IBM公司的研究和開(kāi)發(fā)雜志上發(fā)表，這就是論文“有限自動(dòng)機(jī)及其判定問(wèn)題”(Finiteantomataandtheirdecisionproblems，IBMJournalofResearchandDevelopment，3(1959)，114—125頁(yè))。

1958年夏天，拉賓又一次來(lái)到IBM。當(dāng)時(shí)，“人工智能之父”麥卡錫(J．McCarthy，1971年圖靈獎(jiǎng)獲得者)正在那兒研究往巴克斯(J．Backus，1977年圖靈獎(jiǎng)獲得者)發(fā)明不久的Fortran語(yǔ)言中加入表處理功能。他給拉賓出了一道難題：設(shè)計(jì)一種口令，即使口令被敵方竊去，也無(wú)法進(jìn)入系統(tǒng)。拉賓經(jīng)過(guò)艱苦探索，終于利用由馮·諾伊曼開(kāi)發(fā)的一個(gè)單向函數(shù)解決了這個(gè)問(wèn)題。所謂單向函數(shù)簡(jiǎn)單說(shuō)來(lái)就是正向極易于計(jì)算而反向極難計(jì)算的函數(shù)，例如“平方取中”：y=[x2中間一半的位所組成的數(shù)].這樣，當(dāng)x為100位的數(shù)時(shí)，x2為200位的數(shù)，y則為這200位的中間100位所組成的數(shù)。由z算y是容易的，而由y求出x則非常困難，因?yàn)榭赡艿膞非常之多。正是這個(gè)問(wèn)題促使拉賓進(jìn)一步研究計(jì)算任務(wù)的最小計(jì)算量這一一般性問(wèn)題，也就是計(jì)算的固有難度問(wèn)題，從而成為最早研究計(jì)算復(fù)雜性問(wèn)題的先驅(qū)之一。1959年和1960年，拉賓在耶路撒冷先后發(fā)表了有關(guān)此問(wèn)題的兩篇論文，即“計(jì)算速度和遞歸集合的分類”(Speedofcomputationandclassificationofrecursivesets，3rdConventionofSci．Sco，Israel，1959)及“函數(shù)的計(jì)算難度和遞歸集合的偏序“(DegreeOfdifficultyOfcomputingafunctionandapartialorderingofrecursivesets，Tech．Rep．No．1，O．N．R·，Jerusalem，1960)。論文雖然沒(méi)有用“計(jì)算復(fù)雜性”這個(gè)名詞而用了“計(jì)算速度”和“計(jì)算難度’’這類名詞，但學(xué)術(shù)界公認(rèn)這兩篇論文是研究計(jì)算復(fù)雜性的最早、最權(quán)威的論文中的兩篇，對(duì)1964年正式提出“計(jì)算復(fù)雜性”這一術(shù)語(yǔ)的哈特馬尼斯(J．Hartmanis)和斯特恩斯(R．E．Sterns，這兩人是1993年圖靈獎(jiǎng)獲得者)以及計(jì)算復(fù)雜性理論的另一奠基人布盧姆(M．Blum，1995年圖靈獎(jiǎng)獲得者)都曾產(chǎn)生過(guò)深刻影響。其中布盧姆正是聽(tīng)了拉賓的有關(guān)演說(shuō)才開(kāi)始研究計(jì)算復(fù)雜性并完成其博士論文的。

拉賓的研究成果在一定程度上改變了人們的研究方向。例如，波蘭數(shù)學(xué)家普里斯伯克(M．Presburger)在1930年于華沙舉行的一次國(guó)際數(shù)學(xué)家會(huì)議上所發(fā)表的論文中提出了這樣一個(gè)命題：只包括自然數(shù)相加運(yùn)算的數(shù)學(xué)系統(tǒng)是完備的，也就是說(shuō)這樣的系統(tǒng)在圖靈機(jī)上都是可計(jì)算的。因此這被稱為普里斯伯格算術(shù)系統(tǒng)，不少計(jì)算機(jī)科學(xué)家試圖編寫(xiě)出能證明這個(gè)系統(tǒng)中的定理的計(jì)算機(jī)程序。但拉賓指出，這是極其困難而無(wú)法實(shí)現(xiàn)的。對(duì)于只有100個(gè)符號(hào)的這樣的系統(tǒng)，即使是1萬(wàn)億臺(tái)每秒運(yùn)行1萬(wàn)億次的計(jì)算機(jī)，也要運(yùn)行1萬(wàn)億年才能得出結(jié)果。1974年在斯德哥爾摩的IFIP大會(huì)上他作了一次學(xué)術(shù)演講，公布了他和耶魯大學(xué)的費(fèi)歇爾(M．Fisher)的這項(xiàng)研究成果，宣稱“這就是通向人工智能的理論障礙”。拉賓演說(shuō)那天，正好是美國(guó)總統(tǒng)尼克松因水門事件被迫宣布辭職這一天，拉賓原以為代表們都去看尼克松演說(shuō)的電視轉(zhuǎn)播而不會(huì)有多少人來(lái)聽(tīng)講，卻不料演說(shuō)一開(kāi)始人們就潮水一樣涌了進(jìn)來(lái)，對(duì)演說(shuō)的反應(yīng)十分強(qiáng)烈，拉賓講完以后人們?cè)邴溈孙L(fēng)前排成長(zhǎng)隊(duì)向他提問(wèn)。對(duì)于從事普里斯伯格系統(tǒng)研究的許多人來(lái)說(shuō)，他們聽(tīng)了拉賓演說(shuō)以后的感覺(jué)是非常難受，似乎“世界末日”到了似的。但拉賓本人則并不悲觀，他認(rèn)為應(yīng)該放棄的只是以完全確定的方式去獲得結(jié)果的企圖，但完全可以利用隨機(jī)性以某種方式很快獲得結(jié)果，這種結(jié)果可能出錯(cuò)，然而出錯(cuò)的可能性微乎其微，也就是說(shuō)可以把概率算法(probabilisticalgorithm，或叫隨機(jī)算法，randomizealgorithm)用到這類問(wèn)題中來(lái)，這是拉賓的又一個(gè)貢獻(xiàn)。

所謂概率算法，就是帶有隨機(jī)操作的一類算法。這種算法在計(jì)算的某一步或某些步產(chǎn)生符合規(guī)定要求的隨機(jī)數(shù)，然后根據(jù)產(chǎn)生出韻隨機(jī)數(shù)決定下一步的計(jì)算。例如，在計(jì)算的某一步有兩種選擇：執(zhí)行A或執(zhí)行B。此時(shí)隨機(jī)產(chǎn)生一個(gè)0或1。若產(chǎn)生的是0則執(zhí)行A，若產(chǎn)生的是1則執(zhí)行B。這相當(dāng)于根據(jù)擲一枚硬幣的結(jié)果(正面或反面)決定下一步的計(jì)算。

將概率的思想用到算法中始于數(shù)值計(jì)算，在計(jì)算方法中通常稱作蒙特卡羅法，是在20世紀(jì)40年代中葉提出的。它的基本思想是建立概率模型，通過(guò)統(tǒng)計(jì)模擬或抽樣得到問(wèn)題的近似解。通常要求計(jì)算結(jié)果的期望值等于問(wèn)題的精確解，并且計(jì)算誤差的期望值隨可供使用的時(shí)間增加減小。近20年來(lái)概率算法在非數(shù)值計(jì)算中得到很好的應(yīng)用。例如，已經(jīng)設(shè)計(jì)出關(guān)于排序和搜索、素?cái)?shù)判定、有限域上的多項(xiàng)式分解和求根、字符串的模式匹配等方面的有效概率算法。概率算法同樣也應(yīng)用到并行計(jì)算中，得到概率并行算法。

利用這種概率算法的思想拉賓在1974年斯德哥爾摩演說(shuō)時(shí)就已有了萌芽，但還不夠成熟。第二年休假時(shí)他去了麻省理工學(xué)院，得知了加里·米勒(GaryMiller)的研究工作。米勒證明，利用著名的黎曼假設(shè)(G．P．B．Riemann，1826—1866，德國(guó)的數(shù)學(xué)家兼物理學(xué)家)，可以用一般的確定性算法判斷很大的數(shù)是否是素?cái)?shù)。拉賓利用米勒的研究結(jié)果和數(shù)論中關(guān)于素?cái)?shù)密度的理論，終于在1976年提出了一個(gè)判定素?cái)?shù)的概率算法，取得了極大成功。這個(gè)算法的理論根據(jù)是：當(dāng)n是合數(shù)時(shí)，在1到n—1的整數(shù)中有一半以上是n為合數(shù)的“見(jiàn)證人”。算法的基本做法是：隨機(jī)地產(chǎn)生一個(gè)1與n—1之間的整數(shù)b，檢查6是否是n為合數(shù)的“見(jiàn)證人”。若6是“見(jiàn)證人”，則計(jì)算結(jié)束并得出n為合數(shù)的結(jié)論；否則重復(fù)這個(gè)過(guò)程。至多進(jìn)行K次，若產(chǎn)生的K個(gè)隨機(jī)數(shù)^都不是n為合數(shù)的“見(jiàn)證人”，則得出n為素?cái)?shù)的結(jié)論。算法所需要的時(shí)間為O(1OG3n)。當(dāng)計(jì)算的結(jié)果是n為合數(shù)時(shí)，結(jié)果肯定是正確的。但是，“n為素?cái)?shù)”的結(jié)果有可能是錯(cuò)誤的。此時(shí)n為合數(shù)的概率，即得出錯(cuò)誤結(jié)果的概率不超過(guò)1／2k。當(dāng)k足夠大時(shí)，這是一個(gè)很小的數(shù)。譬如，取K=10，錯(cuò)誤的概率小于0.001。這已經(jīng)是在實(shí)驗(yàn)中不大可能發(fā)生的事件了。實(shí)驗(yàn)表明，算法在實(shí)際使用中幾乎不會(huì)給出錯(cuò)誤的結(jié)論。

拉賓的一個(gè)同事普拉特(V．R．Pratt)用拉賓的算法編寫(xiě)了一個(gè)程序，在1975年冬找到了當(dāng)時(shí)最大的素?cái)?shù)2400—593以及最大的孿生素?cái)?shù)AX338+821和KX338+823(A是小于300的所有素?cái)?shù)的乘積)，創(chuàng)造了世界記錄。拉賓的算法目前仍然是尋找素?cái)?shù)的最快算法之一。

概率算法在分布式計(jì)算、通信、信息檢索、計(jì)算幾何、密碼學(xué)等方面都有廣泛的應(yīng)用。目前，在連接高度并行的計(jì)算機(jī)的專用網(wǎng)絡(luò)上發(fā)送信息的算法就是拉賓的另一個(gè)同事瓦里安特(L．Valiant)所設(shè)計(jì)的一種隨機(jī)算法，這種算法不將信息直接發(fā)往目的地，而是先發(fā)送到任意一個(gè)節(jié)點(diǎn)，然后再由該節(jié)點(diǎn)發(fā)往目的地。瓦里安特證明這種看上去似乎瘋了的方法能有效地減少網(wǎng)絡(luò)中的競(jìng)爭(zhēng)，避免阻塞。這正是隨機(jī)化的威力和魅力所在。在密碼技術(shù)中目前廣泛采用的公開(kāi)密鑰體制(publickey)和RSA算法(Rivest—Shsmjr—Adlemanalgorithm)也使用了拉賓的隨機(jī)化和概率技術(shù)。當(dāng)然，好的技術(shù)也可以用來(lái)干壞事：1988年11月在Internet上廣泛傳播的病毒正是拉賓在哈佛大學(xué)時(shí)的一個(gè)大學(xué)生羅伯特·莫里斯(RobertTappanMorris)利用學(xué)到的隨機(jī)化技術(shù)設(shè)計(jì)出來(lái)并加以傳播的。

斯科特比拉賓小一歲，1932年10月11日生于加利福尼亞州，在加州大學(xué)伯克利分校獲得學(xué)士學(xué)位以后，進(jìn)入普林斯頓大學(xué)研究生院深造，與拉賓一起師從阿隆索·邱奇。邱奇對(duì)學(xué)生要求很嚴(yán)，布置的問(wèn)題也很難，斯科特開(kāi)始時(shí)難以適應(yīng)，精神很緊張，經(jīng)常夜里做惡夢(mèng)。但經(jīng)過(guò)努力，終于可以從容應(yīng)付。1957年暑假他與師兄拉賓一起完成了對(duì)圖靈機(jī)的研究，提出非確定性有限狀態(tài)自動(dòng)機(jī)的理論以后，在1958年取得博士學(xué)位。之后他先后在芝加哥大學(xué)、加州大學(xué)伯克利分校、斯坦福大學(xué)、荷蘭的阿姆斯特丹大學(xué)、普林斯頓大學(xué)和英國(guó)牛津大學(xué)等國(guó)際知名的高等學(xué)府任教。1981年被卡內(nèi)基—梅隆大學(xué)聘為計(jì)算機(jī)科學(xué)、數(shù)理邏輯和哲學(xué)教授。

斯科特的主要興趣和研究方向是邏輯學(xué)。他對(duì)邏輯學(xué)的研究涉及面很廣，包括集合論、模型論、自動(dòng)機(jī)理論、非經(jīng)典邏輯中的模態(tài)邏輯(modallogic，表達(dá)“必然”與“可能”這樣一些概念的邏輯)和直覺(jué)主義邏輯(intuitionismlogic)。直覺(jué)主義邏輯是為克服數(shù)學(xué)研究中出現(xiàn)的悖論而提出的，由荷蘭數(shù)學(xué)家布勞維(L．E．J．Brawer，1881—1966)所創(chuàng)立。直覺(jué)主義邏輯認(rèn)為數(shù)學(xué)是第一位的，邏輯是第二位的，邏輯只是數(shù)學(xué)思維的抽象，是正確的數(shù)學(xué)實(shí)踐的反映。而數(shù)學(xué)的唯一來(lái)臣源是數(shù)學(xué)思維中固有的一種帶構(gòu)造性的直覺(jué)。這些觀點(diǎn)和現(xiàn)今計(jì)算機(jī)科學(xué)與人工智能的研究相吻合，因而受到計(jì)算機(jī)科學(xué)家和人工智能專家的極大重視。斯科特在這些領(lǐng)域中都有不同程度的貢獻(xiàn)。

但斯科特的最大貢獻(xiàn)則是他與斯特雷奇(C．Strachey，1916—1975)合作，在20世紀(jì)60年代提出了程序設(shè)計(jì)語(yǔ)言的“標(biāo)志語(yǔ)義模型”(denotationalsemanticmodel)，為標(biāo)志語(yǔ)義學(xué)(denotationalsemantics)又稱數(shù)學(xué)語(yǔ)義學(xué)(mathematicalsemantics)奠定了堅(jiān)實(shí)的基礎(chǔ)。在標(biāo)言語(yǔ)義學(xué)出現(xiàn)之前，英國(guó)學(xué)者霍爾(，C．A．R．Hoare，1980年圖靈獎(jiǎng)獲得者)已經(jīng)在對(duì)一階謂詞演算擴(kuò)充了一組公理和一組推導(dǎo)規(guī)則的情況下建立起了公理語(yǔ)義學(xué)(axiomaticsemantics)作為程序設(shè)計(jì)語(yǔ)言語(yǔ)義形式化的一種方法，并曾被成功地用來(lái)描述Pascal等語(yǔ)言。但公理語(yǔ)義學(xué)是不完備的。標(biāo)志語(yǔ)義學(xué)把語(yǔ)言中的每一成分與一個(gè)數(shù)學(xué)對(duì)象相對(duì)應(yīng)，稱為從前者到后者的映射，后者即稱為前者的“標(biāo)志”(標(biāo)志語(yǔ)義學(xué)的名稱即由此而來(lái))。這個(gè)數(shù)學(xué)對(duì)象是某個(gè)區(qū)域的元素，該區(qū)域從數(shù)學(xué)上來(lái)說(shuō)是一個(gè)“格”(1attice)，格中的偏序以“定義范圍小于等于”來(lái)確定。標(biāo)志語(yǔ)義學(xué)還規(guī)定，這種映射是層次結(jié)構(gòu)的，映射函數(shù)則往往是遞歸的。這樣，語(yǔ)言中的每一元素既可解釋為一個(gè)函數(shù)，又可解釋為一個(gè)數(shù)據(jù)元素，這正好與程序的以下特性相吻合：既可把程序當(dāng)作函數(shù)予以執(zhí)行，又可把程序當(dāng)作二進(jìn)制位串加以處理。標(biāo)志語(yǔ)義學(xué)一經(jīng)誕生，就獲得了學(xué)術(shù)界廣泛的歡迎，不但被成功地用來(lái)定義Ada等大型程序設(shè)計(jì)語(yǔ)言，還被成功地用來(lái)定義大型數(shù)據(jù)庫(kù)和大型操作系統(tǒng)等，充分顯示了它的生命力。IBM公司的維也納實(shí)驗(yàn)室后來(lái)還開(kāi)發(fā)出元語(yǔ)言METAⅣ，成為用標(biāo)志語(yǔ)義描述大型軟件的強(qiáng)有力工具。后來(lái)它進(jìn)一步發(fā)展為維也納開(kāi)發(fā)方法VDM(ViennaDevelopmentMethod)，成為支持程序開(kāi)發(fā)的一般的形式化方式。國(guó)際標(biāo)準(zhǔn)化組織ISO正在制定有關(guān)VDM的規(guī)約語(yǔ)言VDM—SL(VDM—SpecificationLanguage)。

在建立標(biāo)志語(yǔ)義學(xué)的過(guò)程中，為了奠定其