面向軟件系統(tǒng)XYZ的程序語(yǔ)言的邏輯動(dòng)態(tài)發(fā)展之探究

姚從軍，陳寶愛(ài)

（湘潭大學(xué)碧泉書(shū)院，湖南 湘潭 411105）

1 XYZ的程序語(yǔ)言及其孕育的邏輯動(dòng)態(tài)化發(fā)展思想

中國(guó)科學(xué)院的唐稚松院士是我國(guó)著名的邏輯學(xué)家和計(jì)算機(jī)科學(xué)家。①唐稚松院士科研團(tuán)隊(duì)從20世紀(jì)80年代初開(kāi)始，歷經(jīng)3個(gè)五年計(jì)劃的科研攻關(guān)，終于在1995年開(kāi)發(fā)了世界上獨(dú)創(chuàng)的大型軟件工程工具系統(tǒng)XYZ。XYZ系統(tǒng)被稱(chēng)為系列化語(yǔ)言組，其對(duì)應(yīng)的漢語(yǔ)拼音為Xiliehua Yuyan Zu，因此簡(jiǎn)稱(chēng)XYZ。這項(xiàng)創(chuàng)新性成果榮獲1989年國(guó)家自然科學(xué)獎(jiǎng)一等獎(jiǎng)和1996年何梁何利科學(xué)技術(shù)進(jìn)步獎(jiǎng)，它是我國(guó)軟件工程領(lǐng)域發(fā)展的一個(gè)里程碑，同時(shí)也是我國(guó)為世界軟件工程領(lǐng)域所做的重要貢獻(xiàn)之一。

唐院士提出了世界上第一個(gè)可執(zhí)行時(shí)序邏輯語(yǔ)言XYZ/E，該語(yǔ)言在邏輯系統(tǒng)中引入狀態(tài)轉(zhuǎn)換的控制機(jī)制，是時(shí)序邏輯形式化理論與最新軟件技術(shù)交叉研究的創(chuàng)新案例。XYZ系統(tǒng)由時(shí)序邏輯語(yǔ)言XYZ/E及一組基于該語(yǔ)言的CASE工具集組成?！癤YZ系統(tǒng)是將時(shí)序邏輯和軟件工程有機(jī)結(jié)合而成的整體，時(shí)序邏輯語(yǔ)言XYZ/E是XYZ系統(tǒng)的核心，它既是一個(gè)時(shí)序邏輯系統(tǒng)，又是一種程序語(yǔ)言?！盵1]42

在時(shí)序邏輯語(yǔ)言XYZ/E和C語(yǔ)言的賦值語(yǔ)句那里，出現(xiàn)“一表達(dá)式一范疇多語(yǔ)義”的情況，這里顯示出動(dòng)態(tài)邏輯的思想；另一方面，計(jì)算機(jī)程序C語(yǔ)言的賦值語(yǔ)句直接就是量化動(dòng)態(tài)邏輯的研究對(duì)象，可以對(duì)此進(jìn)行更加精細(xì)的刻畫(huà)；XYZ/E之后出現(xiàn)的動(dòng)態(tài)邏輯主要關(guān)注程序語(yǔ)言的動(dòng)態(tài)特征，然而XYZ/E的基本構(gòu)件，即單元的表述既有動(dòng)態(tài)的特征也兼具靜態(tài)的性質(zhì)，可以設(shè)想擴(kuò)大標(biāo)準(zhǔn)動(dòng)態(tài)邏輯的表達(dá)能力，全面刻畫(huà)XYZ/E的兼容功能；XYZ/E的子語(yǔ)言XYZ/BE所描述的并發(fā)通訊進(jìn)程語(yǔ)義的組合性問(wèn)題是：踏步語(yǔ)句的靜態(tài)組合和非踏步語(yǔ)句的動(dòng)態(tài)組合，靜態(tài)組合原則已有一般性的概括表述，尚需要給出動(dòng)態(tài)組合原則的一般邏輯表述；XYZ/E是建立在時(shí)序邏輯基礎(chǔ)上的程序語(yǔ)言，時(shí)序邏輯的語(yǔ)義是靜態(tài)的，但XYZ/E卻可表現(xiàn)可執(zhí)行命令式編程語(yǔ)言的動(dòng)態(tài)特征——狀態(tài)轉(zhuǎn)換的控制機(jī)制，況且XYZ/E依據(jù)的一階時(shí)序邏輯還是一種擴(kuò)展的多體的時(shí)序邏輯，可以設(shè)想更精準(zhǔn)的方案，來(lái)確立XYZ/E的邏輯基礎(chǔ)。

2 從XYZ的程序語(yǔ)言看邏輯動(dòng)態(tài)化發(fā)展的可能性、必要性及路徑

2.1 應(yīng)用CCG分析方式于時(shí)序邏輯語(yǔ)言XYZ/E，構(gòu)建動(dòng)態(tài)CCG

XYZ的基礎(chǔ)和核心是基于時(shí)序邏輯的程序語(yǔ)言XYZ/E。計(jì)算機(jī)程序語(yǔ)言的任務(wù)是刻畫(huà)機(jī)器狀態(tài)轉(zhuǎn)換的控制機(jī)制，而狀態(tài)轉(zhuǎn)換機(jī)制則通過(guò)賦值語(yǔ)句體現(xiàn)出來(lái)，XYZ/E用時(shí)序邏輯的語(yǔ)義刻畫(huà)賦值語(yǔ)句的動(dòng)態(tài)特征。

XYZ/E的賦值語(yǔ)句表述，如：求階乘0!,1!,…,k!的和，即s=SUM(i=0,…,k)(i!)。[1]53XYZ/E的表述是：

古希臘辯證法思想家赫拉克利特的名言：

一個(gè)人不能兩次踏進(jìn)同一條河流

XYZ/E的賦值語(yǔ)句：

時(shí)序邏輯算子$O的作用使得左邊的j和右邊的j不能賦予同一個(gè)數(shù)值(否則將導(dǎo)致矛盾)，但其類(lèi)型（范疇）卻是一樣的，其類(lèi)型都是e。被賦予的兩個(gè)不同的數(shù)值就是兩個(gè)j的不同語(yǔ)義所指（見(jiàn)下圖紅色符號(hào)串）。具體分析推演如下：

上例可見(jiàn)，可以創(chuàng)立受限的描述個(gè)例的CCG函項(xiàng)應(yīng)用規(guī)則：

對(duì)XYZ/E中類(lèi)似的賦值語(yǔ)句進(jìn)行研究，可以看出動(dòng)態(tài)視角的CCG研究的必要性。組合范疇語(yǔ)法CCG的自然語(yǔ)言研究，采納結(jié)合語(yǔ)用語(yǔ)境的經(jīng)驗(yàn)主義方法，遵循“一詞多范疇多語(yǔ)義”和“多詞一范疇多語(yǔ)義”的原則構(gòu)建CCG處理自然語(yǔ)言的詞庫(kù)。CCG的研究角度也適合于計(jì)算機(jī)程序語(yǔ)言的研究。在時(shí)序邏輯語(yǔ)言XYZ/E和C語(yǔ)言的賦值語(yǔ)句那里，出現(xiàn)“一表達(dá)式一范疇多語(yǔ)義”的情況，這里顯示出動(dòng)態(tài)邏輯的思想。因此，可以把CCG分析方式應(yīng)用于時(shí)序邏輯語(yǔ)言XYZ/E，嘗試構(gòu)建具有動(dòng)態(tài)邏輯思想的CCG研究模式，提出基于個(gè)案?jìng)€(gè)例的CCG函項(xiàng)組合的新規(guī)則，這是一種新的CCG研究方式，即動(dòng)態(tài)CCG。

2.2 計(jì)算機(jī)程序C語(yǔ)言的賦值語(yǔ)句本身是量化動(dòng)態(tài)邏輯的研究對(duì)象

上例看到C語(yǔ)言的賦值語(yǔ)句：

CCG對(duì)自然語(yǔ)言的分析，參照語(yǔ)用語(yǔ)境的情況是：一詞多范疇。按照CCG的方式對(duì)C語(yǔ)言的賦值語(yǔ)句進(jìn)行分析，(在沒(méi)有時(shí)序算子$O的條件下)參照不同語(yǔ)境，左邊的i和右邊的i不能賦予同一個(gè)數(shù)值，但其類(lèi)型（范疇）卻是一樣的，其類(lèi)型都是e。被賦予的兩個(gè)不同的數(shù)值就是兩個(gè)i的不同語(yǔ)義所指。

對(duì)程序語(yǔ)言賦值語(yǔ)句的分析結(jié)果是：一變項(xiàng)一類(lèi)型（范疇），但一類(lèi)型多語(yǔ)義，最終是：一變項(xiàng)多語(yǔ)義。變項(xiàng)的語(yǔ)義隨語(yǔ)境而改變，這也體現(xiàn)出動(dòng)態(tài)的邏輯思想，如量化動(dòng)態(tài)邏輯QDL關(guān)于賦值等式的語(yǔ)義定義針對(duì)的就是這種情況：

這里“x”是被賦值變項(xiàng)，“t”是賦值詞項(xiàng)，它可以是包含變項(xiàng)而經(jīng)過(guò)函子運(yùn)算而產(chǎn)生的項(xiàng)，例如“x+1”。這里賦值語(yǔ)句的動(dòng)態(tài)特征通過(guò)賦值函項(xiàng)a到b的擴(kuò)展體現(xiàn)出來(lái)，b對(duì)“x”的賦值可能不同于a。就上例而言，如a把個(gè)體2賦給“x+1”中的“x”，b給“x”賦的值就是個(gè)體3。

動(dòng)態(tài)邏輯是上個(gè)世紀(jì)90年代才出現(xiàn)的邏輯新品種，直接受計(jì)算機(jī)程序語(yǔ)言動(dòng)態(tài)特征的影響，結(jié)合當(dāng)今上千種程序語(yǔ)言的多樣特征，動(dòng)態(tài)邏輯可以進(jìn)一步拓展。

2.3 XYZ/E的單元兼顧動(dòng)靜，呼喚具有兼容功能的動(dòng)態(tài)邏輯

在唐院士構(gòu)造的XYZ/E中：基本構(gòu)件(單元)的一般表述兼顧動(dòng)靜，既體現(xiàn)了程序的動(dòng)態(tài)語(yǔ)義，還顯示了程序的靜態(tài)語(yǔ)義。XYZ/E的基本構(gòu)件，即單元的一般表述為：

XYZ/E的動(dòng)態(tài)描述：從Ai到Ai+1機(jī)器的狀態(tài)轉(zhuǎn)換 變項(xiàng)的賦值更新

XYZ/E的靜態(tài)描述: 從Bi到Bi+1靜態(tài)的邏輯合取 沒(méi)有變項(xiàng)的賦值更新

當(dāng)單元中的nF2，m=0時(shí)，單元中時(shí)序算子＊限制的諸條件元之間體現(xiàn)的是動(dòng)態(tài)的程序語(yǔ)義。例證：求階乘0!,1!,…,k!的和，即s=SUM(i=0,…,k)(i!)。用純粹可執(zhí)行語(yǔ)言的風(fēng)格表述，即是：

就變項(xiàng)i而言，從A1到A2、A3和A6，被賦予的值不斷更新變化；就變項(xiàng)j而言，從A1到A3、A4和A5，被賦予的值也不斷更新變化?？傊珹1---A6的合取表現(xiàn)的是動(dòng)態(tài)的程序語(yǔ)義。

當(dāng)n=1，mF1時(shí)，單元中的WHERE部分各合取支之間體現(xiàn)的是一種靜態(tài)的邏輯語(yǔ)義。

沿用上述，其表述為：

WHERE后是單元的約束部分，由三個(gè)條件句的合取構(gòu)成，合取支之間沒(méi)有變項(xiàng)的賦值更新，因而是一種靜態(tài)的合取。最后一個(gè)條件句是“階乘和”的數(shù)學(xué)歸納定義，根據(jù)定義，可依次獲得：1!=0!×1，2!=1!×2，3!=2! × 3，……。

當(dāng)nF2，mF1時(shí)，單元中既有＊限制部分中諸條件元之間體現(xiàn)的動(dòng)態(tài)思想，也有WHERE部分各合取支之間體現(xiàn)的靜態(tài)思想，即整個(gè)單元是動(dòng)態(tài)和靜態(tài)的融合。其價(jià)值有：

用混合的形式來(lái)表示中間程度的抽象性。表述為：

其動(dòng)態(tài)合取和靜態(tài)合取的說(shuō)明同上。

動(dòng)態(tài)謂詞邏輯DPL對(duì)邏輯連接詞尤其是對(duì)合取連接詞的定義如下：[3]

由上可知，否定、析取和蘊(yùn)涵連接詞的定義都是靜態(tài)的，a=a，不存在從賦值a到賦值a的更新。而合取連接詞的定義卻是動(dòng)態(tài)的，a并非等同c，從賦值a由于賦值b的關(guān)聯(lián)更新到賦值c，因?yàn)楹先≈Е罩械淖冺?xiàng)賦值可能不同于合取支ψ中的變項(xiàng)賦值，猶如XYZ/E單元中從Ai到Ai+1的賦值更新。量化動(dòng)態(tài)邏輯QDL中對(duì)合取連接詞也有類(lèi)似的動(dòng)態(tài)處理。

XYZ/E之后出現(xiàn)的動(dòng)態(tài)邏輯主要關(guān)注程序語(yǔ)言的動(dòng)態(tài)特征，比如DPL和QDL等動(dòng)態(tài)邏輯刻畫(huà)的是計(jì)算機(jī)程序語(yǔ)言的動(dòng)態(tài)機(jī)制，其合取連接詞的語(yǔ)義定義是動(dòng)態(tài)的，但XYZ/E的單元表述中既有動(dòng)態(tài)的合取，在其受限部分那里還有靜態(tài)的合取。DPL和QDL等動(dòng)態(tài)邏輯對(duì)蘊(yùn)涵連接詞的定義是靜態(tài)的，但XYZ/E中的條件元后件中可能出現(xiàn)時(shí)序算子，就是說(shuō)這樣的條件元的語(yǔ)義可能是動(dòng)態(tài)的。因此，可以考慮擴(kuò)大標(biāo)準(zhǔn)動(dòng)態(tài)邏輯的表達(dá)能力或構(gòu)建新的動(dòng)態(tài)邏輯來(lái)表述XYZ/E的單元中關(guān)于合取和蘊(yùn)涵的動(dòng)靜混合的語(yǔ)義，從而全面刻畫(huà)XYZ/E的兼容功能。

2.4 子語(yǔ)言XYZ/BE描述并發(fā)通訊進(jìn)程語(yǔ)義需要最一般地表述動(dòng)態(tài)組合原則

XYZ/BE中處理并發(fā)通訊進(jìn)程時(shí)：當(dāng)可同步的進(jìn)程P1和P2中的同步語(yǔ)句α1和α2有一個(gè)是踏步語(yǔ)句時(shí)，P1，P2的并發(fā)[P1||P2]中的是靜態(tài)組合的產(chǎn)物；當(dāng)可同步的進(jìn)程P1和P2中的同步語(yǔ)句α1和α2都不是踏步語(yǔ)句時(shí)，P1，P2的并發(fā)[P1||P2]中的是動(dòng)態(tài)組合的產(chǎn)物。[1]229-230踏步語(yǔ)句是一種等待指令，就是等待某個(gè)條件成立，它才會(huì)繼續(xù)，不然就在原地等待。關(guān)于踏步語(yǔ)句和同步語(yǔ)句的定義參見(jiàn)唐稚松2002。[1]227-228

例證：用XYZ/BE表示出兩進(jìn)程：

P1中的紅色條件元和P2中的紅色條件元?jiǎng)討B(tài)組合成[P1||P2]中藍(lán)色條件元，P1中的藍(lán)色條件元和P2中的藍(lán)色條件元?jiǎng)討B(tài)組合成[P1||P2]中藍(lán)色條件元。P1中的其他條件元和P2中的其他條件元保持不變直接延續(xù)到[P1||P2]中去，這些組合是通常的靜態(tài)組合。

靜態(tài)組合的定義：設(shè)有復(fù)合表達(dá)式的句法運(yùn)算F(α1,…, αn)，復(fù)合表達(dá)式的語(yǔ)義G(α1′,…, αn′)意味由α1′,…, αn′定義的組合語(yǔ)義。

例證：MG（蒙太格語(yǔ)法）中的量化復(fù)合表達(dá)式F(α)=every α，這里對(duì)應(yīng)的語(yǔ)義運(yùn)算G(α′)=λP?x[α′(x)→P(x)]

組合前的表達(dá)式α′仍然出現(xiàn)在組合后的表達(dá)式中，保持不變。

動(dòng)態(tài)組合就不一樣了。P1藍(lán)色條件元和P2藍(lán)色條件元中的動(dòng)作部分的動(dòng)態(tài)組合：

這里獲得了[P1||P2]藍(lán)色條件元的動(dòng)作部分中的$O j=k，組合前的$Oc?(j)和c!(k)已不在組合后的表達(dá)式中出現(xiàn)，組合改變了原有表達(dá)式，這就是動(dòng)態(tài)的組合。我們需要對(duì)這類(lèi)個(gè)案?jìng)€(gè)例的程序并發(fā)組合進(jìn)行搜集，期望獲得規(guī)律性的動(dòng)態(tài)組合表述。

總之，XYZ/E的子語(yǔ)言XYZ/BE所描述的并發(fā)通訊進(jìn)程語(yǔ)義的組合性問(wèn)題是：踏步語(yǔ)句的靜態(tài)組合和非踏步語(yǔ)句的動(dòng)態(tài)組合，靜態(tài)組合原則已有一般性的概括表述，怎樣概括動(dòng)態(tài)組合原則的一般表述？值得研究。

2.5 XYZ/E具有的動(dòng)態(tài)精神預(yù)示了時(shí)序邏輯的動(dòng)態(tài)化發(fā)展方向

XYZ/E是建立在時(shí)序邏輯基礎(chǔ)上的程序語(yǔ)言，時(shí)序邏輯的語(yǔ)義是靜態(tài)的，而XYZ/E所關(guān)注的是計(jì)算機(jī)程序中狀態(tài)轉(zhuǎn)換的控制機(jī)制，它可表現(xiàn)可執(zhí)行命令式編程語(yǔ)言的動(dòng)態(tài)特征——狀態(tài)轉(zhuǎn)換的控制機(jī)制，這顯示出動(dòng)態(tài)的精神，可以設(shè)想更精準(zhǔn)的方案，來(lái)確立XYZ/E的邏輯基礎(chǔ)。

XYZ/E定義了10個(gè)時(shí)序算子，比通常時(shí)間邏輯定義的算子要多，多出來(lái)的算子必要性在哪里？可以嘗試對(duì)XYZ/E依據(jù)的時(shí)序邏輯進(jìn)行改造，使其語(yǔ)義直接顯示動(dòng)態(tài)的觀念，據(jù)此構(gòu)建的動(dòng)態(tài)時(shí)序邏輯顯得更加精致。況且XYZ/E依據(jù)的一階時(shí)序邏輯還是一種擴(kuò)展的多體的時(shí)序邏輯，從邏輯系統(tǒng)的精準(zhǔn)性角度調(diào)整XYZ/E的時(shí)序邏輯，是有進(jìn)一步的研究空間。

3 XYZ的程序語(yǔ)言視域下動(dòng)態(tài)邏輯的構(gòu)建方法

3.1 理論聯(lián)系實(shí)際的方法

從邏輯理論出發(fā)，譬如采用組合范疇語(yǔ)法CCG的范疇邏輯分析方式，去剖析計(jì)算機(jī)程序語(yǔ)言的特性，分析XYZ/E表現(xiàn)出的狀態(tài)轉(zhuǎn)換的控制機(jī)制。具體而言，依據(jù)范疇邏輯原理上建立的CCG，把對(duì)自然語(yǔ)言的句法構(gòu)造和語(yǔ)義組合進(jìn)行處理的套路，搬到計(jì)算機(jī)程序語(yǔ)言的領(lǐng)域：確定原子表達(dá)式和初始算子符號(hào)的范疇類(lèi)型，確定對(duì)應(yīng)的語(yǔ)義所指；再依據(jù)通常范疇類(lèi)型運(yùn)算的規(guī)則對(duì)計(jì)算機(jī)程序語(yǔ)言的復(fù)合表達(dá)式乃至語(yǔ)句進(jìn)行推演，在推演過(guò)程中結(jié)合計(jì)算機(jī)程序語(yǔ)言的實(shí)際特征，尤其要捕捉到XYZ/E非常獨(dú)特的表述方式，透過(guò)時(shí)序算子的作用感受到動(dòng)態(tài)的思想，這樣反過(guò)來(lái)對(duì)CCG已有的推演規(guī)則進(jìn)行修正或調(diào)整。進(jìn)而探討新的CCG理論。

3.2 從實(shí)際出發(fā)的經(jīng)驗(yàn)主義方法和理論概括方法

對(duì)計(jì)算機(jī)程序語(yǔ)言XYZ/E進(jìn)行詳細(xì)和持續(xù)的觀察和學(xué)習(xí)，進(jìn)而上升到動(dòng)態(tài)邏輯的理論高度。XYZ/E是上個(gè)世紀(jì)末由中國(guó)科學(xué)家唐稚松院士獨(dú)創(chuàng)的計(jì)算機(jī)程序語(yǔ)言，唐院士非常關(guān)注該語(yǔ)言中的動(dòng)態(tài)語(yǔ)義和靜態(tài)語(yǔ)義，為了增強(qiáng)XYZ/E的表達(dá)力，接近可執(zhí)行命令式程序語(yǔ)言的表述風(fēng)格，并被廣大計(jì)算機(jī)編程人員所接受，唐院士提出了XYZ/E的基本構(gòu)件——單元的表述方式，單元能夠兼容動(dòng)態(tài)的程序語(yǔ)義和靜態(tài)的程序語(yǔ)義。通常邏輯的研究范式往往分而治之，根據(jù)XYZ/E的實(shí)際情況，在邏輯領(lǐng)域?qū)?dòng)態(tài)語(yǔ)義和靜態(tài)語(yǔ)義進(jìn)行融合表述，構(gòu)建新的解釋力更強(qiáng)大的動(dòng)態(tài)靜態(tài)交融的邏輯工具，這是基于XYZ/E這樣的程序語(yǔ)言的實(shí)際情況實(shí)際特征進(jìn)行的研究。

3.3 個(gè)案?jìng)€(gè)例的實(shí)證方法和中等程度的抽象方法

“大數(shù)據(jù)”的精神要求我們?cè)谔幚韱?wèn)題時(shí)盡最大可能搜集相關(guān)數(shù)據(jù)例證。可以采用對(duì)有限范圍的個(gè)案?jìng)€(gè)例進(jìn)行考證的方法，如通訊進(jìn)程的并發(fā)程序具有很多復(fù)雜多樣的例證，涉及的語(yǔ)義組合問(wèn)題是計(jì)算機(jī)軟件領(lǐng)域的著名難題，涉及許許多多計(jì)算機(jī)程序的技術(shù)細(xì)節(jié)。企圖從理論層面系統(tǒng)解決這樣的問(wèn)題談何容易！因此可以降低目標(biāo)，從有限的個(gè)例出發(fā)，逐步推進(jìn)求精，實(shí)現(xiàn)中等程度的抽象，對(duì)于眾多難題解決一點(diǎn)是一點(diǎn)。

注釋?zhuān)?/p>

①著名學(xué)者唐稚松大學(xué)與研究生就讀于清華大學(xué)哲學(xué)系，師從我國(guó)著名邏輯學(xué)家金岳霖先生學(xué)習(xí)邏輯學(xué)，先后進(jìn)入中國(guó)科學(xué)院計(jì)算技術(shù)研究所和軟件所工作，從事邏輯學(xué)與計(jì)算機(jī)科學(xué)的交叉研究，1991年當(dāng)選中國(guó)科學(xué)院院士。