第3章程序標(biāo)準(zhǔn)及其正確性證明概述內(nèi)容－Whereweare？程序標(biāo)準(zhǔn)、標(biāo)準(zhǔn)的描述斷言與標(biāo)準(zhǔn)及{P}S{Q}程序正確性的概念程序正確性證明的過(guò)程3.1程序標(biāo)準(zhǔn)與程序1.程序標(biāo)準(zhǔn)：程序設(shè)計(jì)之前，第一步必須明確“做什么〞。所謂“做什么〞是指對(duì)欲求解的問(wèn)題的描述。程序標(biāo)準(zhǔn)〔PS-ProgramSpecification〕:關(guān)于“做什么〞的描述。這里的PS僅指功能的描述，不包括諸如處理速度、執(zhí)行時(shí)間、響應(yīng)周期等與時(shí)間有關(guān)性能指標(biāo)。PS是軟件工程的需求分析的結(jié)果。PS的含義是映射，是輸入到輸出的映射，它反映了程序?qū)?shù)據(jù)的作用。3.1程序標(biāo)準(zhǔn)與程序(續(xù))2.程序程序也是映射，是輸入到計(jì)算的映射，即每一輸入都對(duì)應(yīng)一串計(jì)算步。3.程序標(biāo)準(zhǔn)與程序的關(guān)系給出標(biāo)準(zhǔn)后，程序開發(fā)就是建立一個(gè)程序，使得計(jì)算剛好能實(shí)現(xiàn)標(biāo)準(zhǔn)的映射；程序驗(yàn)證是證明程序正確地實(shí)現(xiàn)了標(biāo)準(zhǔn)，即證明標(biāo)準(zhǔn)和已有程序之間的一致性規(guī)范程序輸入輸出映射輸入計(jì)算映射3.1程序標(biāo)準(zhǔn)與程序(續(xù))4.程序標(biāo)準(zhǔn)的描述-----標(biāo)準(zhǔn)語(yǔ)言標(biāo)準(zhǔn)必須用語(yǔ)言描述，該語(yǔ)言稱為標(biāo)準(zhǔn)語(yǔ)言。描述一個(gè)復(fù)雜問(wèn)題的輸入和輸出之間的關(guān)系是困難的，目前對(duì)標(biāo)準(zhǔn)語(yǔ)言的模式尚無(wú)定論。有三種模式：自然語(yǔ)言：不夠準(zhǔn)確，存在二義性，必須輔以數(shù)學(xué)語(yǔ)言。一階謂詞：可以精確地描述問(wèn)題的輸入和輸出的關(guān)系，但是標(biāo)準(zhǔn)文本比較長(zhǎng)。如Hoare系統(tǒng)。數(shù)學(xué)語(yǔ)言：用數(shù)學(xué)語(yǔ)言可以把輸入和輸出的映射描述為函數(shù)。這些函數(shù)的精確的泛函定義就構(gòu)成了問(wèn)題的標(biāo)準(zhǔn)。但存在過(guò)于標(biāo)準(zhǔn)的問(wèn)題。3.1程序標(biāo)準(zhǔn)與程序(續(xù))5.一個(gè)適宜的程序標(biāo)準(zhǔn)語(yǔ)言應(yīng)滿足的根本條件:應(yīng)當(dāng)為描述者和使用者所直接理解；應(yīng)當(dāng)有嚴(yán)格的數(shù)學(xué)語(yǔ)義應(yīng)當(dāng)與形式方法的構(gòu)造理論和程序設(shè)計(jì)語(yǔ)言協(xié)調(diào)應(yīng)當(dāng)有較強(qiáng)的表達(dá)能力和通用性3.1程序標(biāo)準(zhǔn)與程序(續(xù))Z語(yǔ)言VDMB方法三者的比較6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介3.1程序標(biāo)準(zhǔn)與程序(續(xù))Z語(yǔ)言是一種基于集合論和一階謂詞邏輯的形式化語(yǔ)言；Z語(yǔ)言支持軟件的形式化標(biāo)準(zhǔn)描述，標(biāo)準(zhǔn)的推理和求精；是迄今為止應(yīng)用最廣泛的形式語(yǔ)言之一；Z是在JeanRaymondAbrial等的開創(chuàng)性工作下，由英國(guó)牛津大學(xué)的程序設(shè)計(jì)研究小組〔PRG，ProgrammingResearchGroup〕，于20世紀(jì)80年代初開發(fā)；PRG與IBM的Hursley實(shí)驗(yàn)室合作，將Z語(yǔ)言用于IBM的客戶信息控制系統(tǒng)的開發(fā)，使得最終的產(chǎn)品質(zhì)量得到了全面的的提高，所測(cè)出的錯(cuò)誤數(shù)量大大減少，并且整體開發(fā)費(fèi)用降低了9％；在ISO指導(dǎo)下的國(guó)際標(biāo)準(zhǔn)化Z工作于2002年完成6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－Z語(yǔ)言簡(jiǎn)介13.1程序標(biāo)準(zhǔn)與程序(續(xù))提供了一種稱為模式〔Schema〕的結(jié)構(gòu)，它是Z的根本描述單位，以此來(lái)描述一個(gè)標(biāo)準(zhǔn)說(shuō)明的狀態(tài)空間〔靜態(tài)性質(zhì)〕和操作〔動(dòng)態(tài)行為〕。Ｚ語(yǔ)言的模式和模式演算：狀態(tài)模式對(duì)目標(biāo)軟件系統(tǒng)的結(jié)構(gòu)特征進(jìn)行抽象描述；操作模式對(duì)目標(biāo)軟件系統(tǒng)的行為特征進(jìn)行抽象描述；通過(guò)模式演算，無(wú)論多么大型系統(tǒng)的規(guī)格說(shuō)明都可以通過(guò)一個(gè)個(gè)小的局部來(lái)構(gòu)成；6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－Z語(yǔ)言簡(jiǎn)介23.1程序標(biāo)準(zhǔn)與程序(續(xù))Ｚ模式說(shuō)明可以組合成新的Ｚ模式，新的Ｚ模式繼承其成分模式的一切屬性和約束。軟件系統(tǒng)的Ｚ模式規(guī)格說(shuō)明可以按一定的層次結(jié)構(gòu)給出。Ｚ規(guī)格說(shuō)明由一系列模式組成，每個(gè)模式定義一個(gè)抽象對(duì)象或操作，并用謂詞判定描述給出新的對(duì)象或操作的語(yǔ)義約束。模式例:6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－Z語(yǔ)言簡(jiǎn)介33.1程序標(biāo)準(zhǔn)與程序(續(xù))模式例1:[Student]//引入根本類型studentStudentSys//模式名Enrolled,tested:PStudent//聲明局部,學(xué)生的密集類型#enrolled≤size//斷言局部，合取關(guān)系testedenrolled等價(jià)于：//水平方式StudentSys=[enrolled,tested:PStudent|

#enrolled≤sizetestedenrolled]6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－Z語(yǔ)言簡(jiǎn)介43.1程序標(biāo)準(zhǔn)與程序(續(xù))模式例2:EnrollStudentStudentSys//=StudentsysStudentSys’的簡(jiǎn)寫

name?:Student//在輸入變量后加？name?enrolled//在輸出變量后加！enrolled<size//帶有后綴‘的變量表示操作后的變量enrolled’=enrolled∪{name?}tested’=tested

6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－Z語(yǔ)言簡(jiǎn)介53.1程序標(biāo)準(zhǔn)與程序(續(xù))缺點(diǎn):⑴Ｚ語(yǔ)言對(duì)大型系統(tǒng)的模塊化能力缺乏。⑵難以識(shí)別影響某一狀態(tài)模式的所有操作模式。⑶不能支持規(guī)格說(shuō)明的重用。⑷Ｚ語(yǔ)言難以由計(jì)算機(jī)直接處理。缺少商品化的工具支持等到諸多原因6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－Z語(yǔ)言簡(jiǎn)介63.1程序標(biāo)準(zhǔn)與程序(續(xù))VDM〔ViennaDevelopmentMethod〕是在1969年為開發(fā)PL/1語(yǔ)言時(shí)，由IBM公司維也納實(shí)驗(yàn)室的研究小組提出的。初衷是為了描述PL/1語(yǔ)言的語(yǔ)義。VDM是一種功能構(gòu)造性規(guī)格說(shuō)明技術(shù)，它通過(guò)一階謂詞邏輯和已建立的抽象數(shù)據(jù)類型來(lái)描述每個(gè)運(yùn)算或函數(shù)的功能。這種方法在90年代初在歐美許多研究機(jī)構(gòu)或大學(xué)得到了廣泛的應(yīng)用。如曼徹斯特大學(xué)將其作為CS的必修課。1996年ISO制訂了VDM的國(guó)際標(biāo)準(zhǔn)化版本VDM-SL6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－VDM簡(jiǎn)介13.1程序標(biāo)準(zhǔn)與程序(續(xù))VDM技術(shù)的根本思想：運(yùn)用抽象數(shù)據(jù)類型、數(shù)學(xué)概念和符號(hào)來(lái)規(guī)定運(yùn)算或函數(shù)的功能；可使軟件系統(tǒng)的功能描述在抽象級(jí)上進(jìn)行，完全擺脫了實(shí)現(xiàn)細(xì)節(jié)，這樣為軟件實(shí)現(xiàn)者提供了很大的靈活性；這種形式化規(guī)格說(shuō)明還為程序正確性證明提供了依據(jù)。6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－VDM簡(jiǎn)介23.1程序標(biāo)準(zhǔn)與程序(續(xù))VDM支持兩種抽象：數(shù)據(jù)抽象和操作抽象。一個(gè)VDM標(biāo)準(zhǔn)有以下不同的塊組成：types<typedefinitions>values<valuedefinitions>functions<functiondefinitions>operations<operationdefinitions>state<statename>of<statedefinition>end6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－VDM簡(jiǎn)介33.1程序標(biāo)準(zhǔn)與程序(續(xù))缺點(diǎn)：⑴由于VDM對(duì)抽象數(shù)據(jù)類型預(yù)先定義了運(yùn)算，而某些用戶定義的類型在規(guī)格說(shuō)明描述中無(wú)需這么多運(yùn)算，因而產(chǎn)生了運(yùn)算冗余。⑵VDM目前還未能建立一整套描述機(jī)制，將一個(gè)大型系統(tǒng)分解為許多運(yùn)算而描述出這些運(yùn)算之間的關(guān)系⑶VDM形式規(guī)格說(shuō)明過(guò)于形式化不容易理解6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－VDM簡(jiǎn)介43.1程序標(biāo)準(zhǔn)與程序(續(xù))B方法是20世紀(jì)80年代初中期由以及BP研究中心的MATRA和GEAlsthom研究小組開發(fā)的。Ｂ語(yǔ)言是計(jì)算機(jī)輔助軟件工程中Ｂ技術(shù)、方法和工具集的簡(jiǎn)稱;Ｂ語(yǔ)言是一種健全的面向?qū)嶋H軟件過(guò)程的基于數(shù)學(xué)理論的技術(shù);Ｂ方法所用的符號(hào)和方法支持大局部的軟件過(guò)程：需求分析、規(guī)格說(shuō)明、軟件設(shè)計(jì)、實(shí)現(xiàn)和維護(hù);Ｂ方法的指導(dǎo)性原那么：分層軟件的逐步構(gòu)造伴隨著逐步的驗(yàn)證和校驗(yàn)；6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－B語(yǔ)言簡(jiǎn)介13.1程序標(biāo)準(zhǔn)與程序(續(xù))Ｂ工具盒包括有大量的工具，所有的工具集成在一個(gè)基于窗口的軟件開發(fā)環(huán)境中，因而支持運(yùn)用Ｂ方法開發(fā)軟件的整個(gè)軟件過(guò)程；Ｂ工具支持軟件的逐步構(gòu)造，其中的驗(yàn)證過(guò)程可用靜態(tài)分析，動(dòng)態(tài)分析采用模擬技術(shù)，正確性證明那么使用集成的定理證明器。Ｂ方法用一種簡(jiǎn)單的偽程序語(yǔ)言來(lái)描述需求模型、說(shuō)明接口，并進(jìn)行中間設(shè)計(jì)和實(shí)現(xiàn)；B語(yǔ)言就是AMN〔抽象機(jī)器符號(hào)〕，AMN支持規(guī)格說(shuō)明的類型檢測(cè)、動(dòng)態(tài)驗(yàn)證、數(shù)學(xué)證明等來(lái)確保設(shè)計(jì)過(guò)程的正確。6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－B語(yǔ)言簡(jiǎn)介23.1程序標(biāo)準(zhǔn)與程序(續(xù))B方法的特點(diǎn)簡(jiǎn)單熟悉的符號(hào)表示法：這種符號(hào)表示法用來(lái)表達(dá)狀態(tài)轉(zhuǎn)換，從規(guī)格說(shuō)明到編碼，這種統(tǒng)一的形式減少了學(xué)習(xí)的難度和轉(zhuǎn)換中的語(yǔ)法錯(cuò)誤。模塊化構(gòu)造：從規(guī)格說(shuō)明到實(shí)現(xiàn)的模塊化構(gòu)造允許將規(guī)格說(shuō)明和驗(yàn)證過(guò)程分解為多個(gè)子任務(wù)來(lái)進(jìn)行。大量實(shí)用的工具支持：現(xiàn)有大量的實(shí)用工具支持了B方法軟件開發(fā)周期的所有階段，包括動(dòng)畫和文檔生成。成功的工業(yè)應(yīng)用：B語(yǔ)言和方法已在很多的工業(yè)領(lǐng)域得到成功應(yīng)用，包括實(shí)時(shí)、仿真、信息處理和工程等。6.形式化程序標(biāo)準(zhǔn)描述語(yǔ)言簡(jiǎn)介－B語(yǔ)言簡(jiǎn)介33.1程序標(biāo)準(zhǔn)與程序(續(xù))6.Z語(yǔ)言、VDM、B形式化方法的比較屬性ZVDMB基礎(chǔ)謂詞演算,集合論,模式偏函數(shù),集合論最弱前置條件,集合論開發(fā)階段規(guī)范說(shuō)明規(guī)范說(shuō)明,設(shè)計(jì)規(guī)范說(shuō)明,設(shè)計(jì),實(shí)現(xiàn)形式模式的符號(hào)表示,關(guān)系前/后置條件,函數(shù)嚴(yán)格的編程語(yǔ)言工具支持在規(guī)格說(shuō)明級(jí)在規(guī)格說(shuō)明級(jí)B-Toolkit,AtchierB,所有開發(fā)階段培訓(xùn)支持圖書、課程圖書,課程實(shí)例研究、課程內(nèi)容－Whereweare？程序標(biāo)準(zhǔn)、標(biāo)準(zhǔn)的描述斷言與標(biāo)準(zhǔn)及{P}S{Q}程序正確性的概念程序正確性證明的過(guò)程3.2斷言與標(biāo)準(zhǔn)1.斷言斷言就是關(guān)于事物性質(zhì)的陳述。這個(gè)陳述可真可假。如“三是個(gè)質(zhì)數(shù)〞用斷言作為程序的注解或作為正確性命題的一局部時(shí)，常用大括號(hào)括起來(lái)。例1：寫一個(gè)計(jì)算商和余數(shù)的程序程序標(biāo)準(zhǔn)：“設(shè)被除數(shù)x1是個(gè)非負(fù)整數(shù)，除數(shù)x2是個(gè)正整數(shù)，計(jì)算x1除以x2的商y1和余數(shù)y2〞又描述為：“初始條件：{x1>=0ANDx2>0},計(jì)算滿足{x1=x2*y1+y2and0<=y2<x2}的整數(shù)y1和y2〞3.2斷言與標(biāo)準(zhǔn)(續(xù))一般地，一個(gè)程序標(biāo)準(zhǔn)可表示為由兩個(gè)謂詞構(gòu)成的二元組〔P，Q〕。其中，P描述了所欲求解的問(wèn)題必須滿足的初始條件，它限定了輸入?yún)?shù)的性質(zhì)，稱為初始斷言或前置斷言；Q描述了問(wèn)題的最終解必須滿足的性質(zhì)，稱為結(jié)果斷言或后置斷言。3.2斷言與標(biāo)準(zhǔn)(續(xù))程序斷言是對(duì)程序的性質(zhì)的陳述。最重要的一個(gè)程序斷言為：{P}S{Q}。其中，〔P，Q〕是程序S的程序標(biāo)準(zhǔn)，S是一個(gè)程序〔或語(yǔ)句〕斷言{P}S{Q}稱為S關(guān)于〔P，Q〕的正確性斷言。它的意義：“假設(shè)S開始執(zhí)行時(shí)P為真，那么S的執(zhí)行必終止且終止時(shí)Q為真〞3.2斷言與標(biāo)準(zhǔn)(續(xù))例：求商余程序{x1>=0andx2>0}Y2:=x1;y1:=0;{0<=y2and0<x2andx1=x2*y1+y2}Whiley2>=x2dobegin{0<=y2and0<x2<＝y(tǒng)2andx1=x2*y1+y2}

y2:=y2-x2;y1:=y1+1;

{0<=y2and0<x2andx1=x2*y1+y2}end;{x1=x2*y1+y2and0<=y2<x2}3.2斷言與標(biāo)準(zhǔn)(續(xù))問(wèn)題：如何構(gòu)造斷言使他們能準(zhǔn)確地反映不同位置上程序的性質(zhì)？有了斷言，如何證明他們的正確性？能否有準(zhǔn)那么，可以從標(biāo)準(zhǔn)〔P，Q〕構(gòu)造出程序S，使{P}S{Q}為真。3.2斷言與標(biāo)準(zhǔn)(續(xù))2.程序斷言的進(jìn)一步說(shuō)明說(shuō)明：在給出標(biāo)準(zhǔn)描述〔P，Q〕時(shí)，必須指明哪些量是可變的，哪些是不可變的。如果是可變的，必要時(shí)對(duì)前者還需指明其變化方式。輸入?yún)?shù)：在程序執(zhí)行前從外部獲得值，但在程序執(zhí)行中，其值始終保持不變的變量。一般用以x開頭的標(biāo)識(shí)符表示。輸出變量：其值隨程序的執(zhí)行而不斷變化的變量。一般以y開頭的變量，或不以x和u開頭的變量標(biāo)識(shí)。輔助變量：為了描述程序變量取值變化方式而因入的變量。這些變量不得在程序中出現(xiàn)，用以u(píng)開頭的變量表示。3.2斷言與標(biāo)準(zhǔn)(續(xù))例1.編寫一個(gè)程序Swap〔y1，y2〕，功能是把y1，y2兩變量的值互換。其標(biāo)準(zhǔn):({y1=u1∧y2=u2}，{y1=u2∧y2=u1})3.2斷言與標(biāo)準(zhǔn)(續(xù))例2：對(duì)數(shù)組b[m：n]進(jìn)行排序的程序。功能是把數(shù)組b[m：n]各元素的值從小到大排列起來(lái)，使得最后的數(shù)組滿足b[i]≤b[i+1]，i=m，…,n-1。標(biāo)準(zhǔn)：P：{m≤n∧b[m:n]=u[m:n]}Q：{m≤n∧perm(b[m:n],u[m:n])∧(i:m≤i<n:b[i]≤b[i+1])}其中，u[m:n]代表b的任意可能初值；perm(b[m:n],u[m:n])是一個(gè)常謂詞，表示b是u的一個(gè)置換。3.2斷言與標(biāo)準(zhǔn)(續(xù))程序標(biāo)準(zhǔn)總結(jié)：在做程序標(biāo)準(zhǔn)時(shí)，必須區(qū)分三種變量：輸入變量、輸出變量、輔助變量。作為某一個(gè)標(biāo)準(zhǔn)〔P，Q〕的實(shí)現(xiàn)程序S，S不得包含輔助變量，S也不得對(duì)輸入?yún)?shù)進(jìn)行任何形式的賦值，這些就是對(duì)標(biāo)準(zhǔn)〔P，Q〕和斷言{P}S{Q}的語(yǔ)法規(guī)定。程序正確性斷言{P}S{Q}的意義：“假設(shè)S的執(zhí)行開始于一個(gè)滿足P的狀態(tài)，那么這個(gè)執(zhí)行必將在有限的時(shí)間內(nèi)終止于一個(gè)滿足Q的狀態(tài)〞。所謂一個(gè)狀態(tài)是滿足P〔或Q〕的，假設(shè)在此狀態(tài)下P〔或Q〕為真。內(nèi)容－Whereweare？程序標(biāo)準(zhǔn)、標(biāo)準(zhǔn)的表示方法斷言與標(biāo)準(zhǔn)及{P}S{Q}程序正確性的概念程序正確性證明的過(guò)程3.3程序正確性概念定義1.如果對(duì)于每一個(gè)使得P(ā)為真的輸入ā，程序S計(jì)算都終止，稱程序S對(duì)P是終止的。定義2：對(duì)于滿足P(ā)為真，且能夠使程序S計(jì)算終止的每個(gè)ā，如果Q(ā,P(ā))為真，那么稱程序S對(duì)于P和Q是局部正確的。記為[P]S[Q]。?[P]S[Q]iff(ā)((?p(ā)and(?Sterminates))?Q(ā,P(ā))3.3程序正確性概念(續(xù))定義3：對(duì)于滿足P(ā)為真的每個(gè)ā，如果程序S能夠計(jì)算終止，且Q(ā,P(ā))為真，那么稱程序S對(duì)于P和Q是完全正確的。記為{P}S{Q}?{P}S{Q}iff(ā)(?p(ā)((?Sterminates)

and?Q(ā,P(ā)))?[P]S[Q]iff(ā)((?p(ā)and(?Sterminates))?

Q(ā,P(ā))〔1〕關(guān)于局部正確性證明的方法Floyd的不變式斷言法Manna的子目標(biāo)斷言法Hoare的公理化方法〔2〕關(guān)于終止性證明的方法Floyd的良序集方法Knuth的計(jì)數(shù)器方法Manna等人的不動(dòng)點(diǎn)方法〔3〕關(guān)于完全正確性的證明方法Hoare的公理化方法〔Manna、Pnueli〕Bustall的間發(fā)斷言法Dijkstra的弱謂詞轉(zhuǎn)換方法以及強(qiáng)驗(yàn)證方法。3.3程序正確性概念(續(xù))主要的程序正確性證明方法內(nèi)容－Whereweare？程序標(biāo)準(zhǔn)、標(biāo)準(zhǔn)的表示方法斷言與標(biāo)準(zhǔn)及{P}S{Q}程序正確性的概念程序正確性證明的過(guò)程3.4程序的非形式化正確性證明簡(jiǎn)介設(shè)〔P，Q〕是一個(gè)標(biāo)準(zhǔn)，S是依照這個(gè)標(biāo)準(zhǔn)要求設(shè)計(jì)的程序，且是由語(yǔ)句s1，s2，…，sn組成的一個(gè)枚舉型程序〔即其執(zhí)行等于組成它的各個(gè)語(yǔ)句的逐一順序的執(zhí)行，其中的每個(gè)語(yǔ)句都只有一個(gè)入口和一個(gè)出口，且沒(méi)有GOTO語(yǔ)句〕。令P1,Q1,P2,Q2,…,Pn,Qn是2n個(gè)謂詞，且P=P1，Q=Qn。如果所有斷言{Pi}Si{Qi}，i=1，2，…,n,為真，并且每個(gè)蘊(yùn)涵：QiPi+1，i=1，2，…,n成立，就稱〔P1，Q1〕，〔P2，Q2〕，…,〔Pn，Qn〕是{P}S{Q}的一個(gè)證明。例1：3.4程序的非形式化正確性證明簡(jiǎn)介(續(xù))例1：令〔P，Q〕為：P：{i≥0∧s=b[0]+…+b[i]}Q：{i>0∧s