軟件需求分析圖形表示與形式描述

軟件需求分析圖形表示與形式描述傳統(tǒng)圖形描述技術(shù)建模及語義中國諺語EINBILDZEIGTUEBERTAUSENDSAETZEAPICTURESHOWSMORETHAN1000SENTENCES1、三種主要傳統(tǒng)圖形描述技術(shù)（1）數(shù)據(jù)流圖技術(shù)DFD（DATAFLOWDIAGRAM）描述一個信息系統(tǒng)的數(shù)據(jù)（信息）流。（2）實體關(guān)系圖技術(shù)ERD（ENTITYRELATIONSHIPDIAGRAM）描述一個信息系統(tǒng)的邏輯數(shù)據(jù)結(jié)構(gòu)。（3）狀態(tài)轉(zhuǎn)換圖技術(shù)STD（STATETRANSITIONDIAGRAM）描述一個信息系統(tǒng)的狀態(tài)轉(zhuǎn)換過程。2、基于圖形描述技術(shù)的需求分析模型（1）需求分析模型的基本功能描述用戶需求建立創(chuàng)建軟件設(shè)計的基礎(chǔ)定義軟件開發(fā)后的驗證條件集合（2）需求分析模型結(jié)構(gòu)圖21給出了基于圖形描述技術(shù)的需求分析模型結(jié)構(gòu)。圖21需求分析模型結(jié)構(gòu)（摘自PRESSMAN，SOFTWAREENGINEERING，P300）其中（1）核心部分DATADICTIONARY（DD，數(shù)據(jù)字典）存儲所有軟件使用或產(chǎn)生的對象數(shù)據(jù)的描述。（2）中間層DATAFLOWDIAGRAM（DFD，數(shù)據(jù)流圖）描述數(shù)據(jù)在經(jīng)過系統(tǒng)時的轉(zhuǎn)換過程圖示數(shù)據(jù)流函數(shù)ENTITYRELATIONSHIPDIAGRAM（ERD，實體關(guān)系圖）圖示數(shù)據(jù)之間的關(guān)系STATETRANSITIONDIAGRAM（STD，狀態(tài)轉(zhuǎn)換圖）描述系統(tǒng)接收外部事件后的狀態(tài)變化（3）外部層PROCESSSPECIFICATION（PSPEC，過程規(guī)約）描述DFD中定義的每個函數(shù)DATAOBJECTDESCRIPTION（數(shù)據(jù)對象描述）描述ERD中每個數(shù)據(jù)對象的屬性CONTROLSPECIFICATION（CSPEC，控制規(guī)約）描述軟件控制外觀的附加信息231數(shù)據(jù)流圖DFD及語義1定義（DFD）數(shù)據(jù)流圖DFD技術(shù)描述流經(jīng)一個信息系統(tǒng)的數(shù)據(jù)（信息）流，主要包括（1）數(shù)據(jù)的輸入與輸出數(shù)據(jù)是如何進入系統(tǒng)或從系統(tǒng)離開；（2）數(shù)據(jù)處理站點在哪里數(shù)據(jù)是怎樣處理的；（3）存儲單元數(shù)據(jù)是在哪里存儲的。2定義（DFD符號）數(shù)據(jù)（信息）的源點/終點數(shù)據(jù)（信息）加工或邏輯處理數(shù)據(jù)（信息）存儲數(shù)據(jù)（信息）流3實例研究汽車租賃數(shù)據(jù)流圖（1）一個汽車租賃數(shù)據(jù)流圖EURENTDFD見圖22。圖22EURENTDFD（摘自HAGGENMUELLER,WIRSINGMETHODENDERSOFTWAREENTWICKLUNG,P29）圖中KUNDE用戶或汽車租賃者MAKEBOOKINGS租車登記OBTAINPAYMENT得到支付VEHICLEDEPARTURESFUNCTFPREDPSGENERATEDBYC定義公理AXIOMSEENDAXIOMS其中,S規(guī)約中包括的所有數(shù)據(jù)類型的集合F所有函數(shù)符號的集合P所有謂詞符號的集合CS的構(gòu)造操作符集合,且CFE公理集合,表示所有的特性（CHARACTERISTICPROPERTIES）上述規(guī)約可書寫成如下規(guī)約SP標記，公理EBOOLTHVALUE的規(guī)約設(shè)計（1）公理規(guī)約（AXIOMATICSPECIFICATION）BOOL0SIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLPREDICATESYMBOLSPREDNOTBOOLBOOLAXIOMSAXIOMS，XBOOLNOTTRUEFALSENOTNOT（X）XENDAXIOMS2PROLOG規(guī)約PROLOGSPECIFICATIONREMARKN個變量的函數(shù)將通過N1變量的關(guān)系定義，函數(shù)的值變量置于N1個關(guān)系的最后一位BOOL_PLSIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLPREDICATESYMBOLSPREDNOTBOOLBOOLAXIOMSAXIOMSX,YBOOLNOTTRUE,FALSENOTX,YNOTY,XENDAXIOMS3邏輯規(guī)約LOGICSPECIFICATIONREMARK一個自變量的布爾函數(shù)將通過一個變量的關(guān)系表達BOOL_LSIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLPREDICATESYMBOLSPREDNOTBOOLAXIOMSAXIOMSNOTFALSENOTTRUEENDAXIOMS4帶構(gòu)造操作符的公理規(guī)約SPECIFICATIONWITHCONSTRUCTORBOOLTSIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORTRUTHVALUEBOOLGENERATEDBYTRUE,FALSENONCONSTRUCTORSYMBOLFUNCTNOTBOOLBOOLAXIOMSAXIOMSXBOOLNOTTRUEFALSENOTNOTXXENDAXIOMS322標記SIGNATURE1定義（SIGNATURE）一個標記是一個三元組（S，F(xiàn)，P），其中S是一個類集（SETOFSORTS），F(xiàn)是一個定義在SS上的函數(shù)符號集，其中S為定義域，SS為函數(shù)F,S的值域，P是一個定義在S上的謂詞符號集。REMARK（1）標記描述規(guī)約的語法（SYNTAXOFSPECIFICATION）（2）FF,S可寫成FS1S2,SNS（3）PP可寫成PS1S2,SN（4）規(guī)約SP的標記可寫成SIG（SP）SP2案例研究例1上述邏輯規(guī)約LOGICSPECIFICATIONBOOL_L的標記SIG（BOOL_L）SBOOLF（F）BOOLNN0且FTRUE，F(xiàn)ALSE常量FOTHERWISE空集P（P）BOOLNN0且PNOT，其中為布爾運算POTHERWISE例2公理規(guī)約BOOL0及BOOLT的標記SIG（BOOL0）SIG（BOOLT）SBOOL；F（F）BOOLNN0且FTRUE，F(xiàn)ALSE常量FNOT函數(shù)FOTHERWISE；空集P（P）BOOLNN0且P其中為布爾運算POTHERWISE思考（1）找出程序中所有類型與運算符號有利于程序理解；（2）可用于程序測試、項目管理、程序度量等；（3）可用于研究程序體系結(jié)構(gòu)等（4）語法、語義匹配，語義查詢等；（5）基于語義的WEB服務應用等。3定義標記被稱為是代數(shù)的，只有當?shù)仁健啊笔瞧渲形ㄒ坏年P(guān)系運算符。例上述規(guī)約BOOL0和BOOLT的標記是代數(shù)的；規(guī)約BOOL_L不是代數(shù)的，因為存在關(guān)系運算符“NOT”。323項（TERM）每個標記（S，F(xiàn)，P）定義了一個表達式的集合，稱為項集，其中項元素是由自由變量X和中的函數(shù)符號構(gòu)成。XS所有程序中的表達式都是由和X構(gòu)成的。1定義（項的歸納定義）（1）設(shè)為標記，X（XS）SS為標識符（IDENTIFICATOR）的集合，則對每個SS，T（，X）S為最小項集并滿足下列特性A）對每個XXS滿足XT（，X）S，則X是一個項；B）若FF并滿足FT（，X）S，則F是一個常量，同時F也是一個項；C）若FF,S且TIT（，X）SI，I1,N，則FT1,TNT（，X）（2）不含變量的項稱為基項（GROUNDTERM），即當X時，所有的TT（，）S是基項；（3）標記被稱為是敏感的（SENSITIVE），如果每個類SS都存在一個基項TT（，）S，即SST（，）S成立；（4）項TT（，X）S的類型為S；（5）T（，X）DEF（T（，X）S）SS2舉例數(shù)學表達式中的項表達式A2ABB2項A2，AB，B2324結(jié)構(gòu)（STRUCTURE）一個結(jié)構(gòu)可看作對標記中符號的進一步定義和說明，其中（1）每個類對應一個值的集合；（2）每個函數(shù)符號定義一個函數(shù)；（3）每個謂詞運算符號定義一個關(guān)系。1定義（結(jié)構(gòu)）一個結(jié)構(gòu)（也稱代數(shù)）A包括（1）一個家族（FAMILY，或集合的集合）（AS）SS，其中AS為非空的值的集合；（2）一個函數(shù)集FAS1AS2ASNAS，其中FF,S；（3）一個謂詞集PS1S2,SN，其中PP。所有的具有標記為的結(jié)構(gòu)的類（CLASS）表示為STRUCT（）。2案例研究例設(shè)SIG（BOOLT），則結(jié)構(gòu)包括（1）真值的標準模塊BBBOOLT，F(xiàn)；TRUEBT；FALSEBF；NOTB（T）F；NOTB（F）T；XBYIFFXY；（2）在自然數(shù)上定義的結(jié)構(gòu)NBNBBOOLN；TRUENB1；FALSENB0；NOTNB（2I）2I1；NOTNB（2I1）2I；I0XNBYIFFXY；（3）非標準模塊NB1NB1BOOLN；TRUENB11；FALSENB10；NOTNB1（I1）0；NOTNB1（0）1；I0，1，2，XNB1YIFFXY0OR（X0Y0）；（4）定義在整數(shù)上的結(jié)構(gòu)ZBZBBOOLZ；TRUEZB1；FALSEZB0；NOTZB（1）0；NOTZB（0）1；NOTZB（I）I，F(xiàn)ORI0I1，IZ；XZBYIFFXY；（5）定義在整數(shù)上的結(jié)構(gòu)ZB1ZB1BOOLZ；TRUEZB11；FALSEZB10；NOTZB1（1）0；NOTZB1（0）1；NOTNB1（I）I1，F(xiàn)ORI0I1，IZ；XZB1YIFFXY；（6）最小的結(jié)構(gòu)UBUBBOOL1；TRUEUBFALSEUB1；NOTUB（1）1；（UBBOOL）DEF11；說明1軟件的實現(xiàn)是多樣化的；2軟件的正確性是相對的。325公理/代數(shù)規(guī)約REMARK簡單公理規(guī)約可以通過其標記和一個好形公式（WFF）集合E定義。1定義（公理規(guī)約）設(shè)（S，F(xiàn)，P）是一個標記，E是一個定義的好形公式集合，則SP，E是一個公理規(guī)約。NOTE（1）公理規(guī)約SP是代數(shù)的，如果等式“”是唯一的謂詞符號，即SPS，S（2）好形公式WFF（WELLFORMEDFORMULA）的定義見離散數(shù)學相關(guān)教材和參考資料。一階謂詞邏輯FIRSTORDERLOGIC；只包含函數(shù)符和等式“”；由原子公式、布爾運算符及量詞（全稱量詞和存在量詞）組成。2定義（規(guī)約語義）規(guī)約SP，E的語義可通過標記和模型類（CLASSOFMODELS）定義，即標記SIG（SP）SIG（，E），模型類MOD（SP）MOD（，E）ASTRUCT（）AGFORALLGE，其中，A為模型，STRUCT（）為結(jié)構(gòu)，AG為“A滿足于G”，GE表示G為公理集合E中的等式，MOD（SP）可表示成SP。3實例研究證明上述結(jié)構(gòu)B、NB、NB1、ZB、UB為規(guī)約BOOL0的模型；ZB1不是規(guī)約BOOL0的模型。證明（1）B是規(guī)約BOOL0的模型證明義務需證明B結(jié)構(gòu)定義使BOOL0中的每個公理成立。NOT（TRUEB）NOT（T）FFALSEB；DEFINITIONNOT（NOT（X）NOT（NOT（T）NOT（F）TTRUEBX，當XTRUEB；NOT（NOT（F）NOT（T）FFALSEBX，當XFALSEB。（2）NB是規(guī)約BOOL0的模型證明義務需證明NB結(jié)構(gòu)定義使BOOL0中的每個公理成立。NOT（TRUENB）NOT（1）0FALSENB；NOT（NOT（X）NOT（NOT（2I）NOT（2I1）2IX，當X2INB；NOT（2I）2I1X，當X2I1NB。（3）NB1是規(guī)約BOOL0的模型證明義務需證明NB1結(jié)構(gòu)定義使BOOL0中的每個公理成立。NOT（TRUENB1）NOT（1）0FALSENB1；NOT（NOT（X）NOT（NOT（0）NOT（1）0，當X0NB1；NOT（NOT（I1）NOT（0）1I1，當XI1NB。（4）UB是規(guī)約BOOL0的模型證明義務需證明UB結(jié)構(gòu)定義使BOOL0中的每個公理成立。NOT（TRUEUB）NOT（1）1FALSEUB；NOT（NOT（X）NOT（NOT（1）NOT（1）1X，當X1。（5）ZB是規(guī)約BOOL0的模型證明義務需證明ZB結(jié)構(gòu)定義使BOOL0中的每個公理成立。NOT（TRUEZB）NOT（1）0FALSEZB；NOT（NOT（X）NOT（NOT（0）NOT（1）0，當X0；NOT（NOT（1）NOT（0）1，當X1；NOT（NOT（X）NOT（X）X，當XI且X0，X1。（6）ZB1不是規(guī)約BOOL0的模型證明義務需證明ZB結(jié)構(gòu)定義不能使BOOL0中的每個公理成立。NOT（TRUEZB1）NOT（1）0FALSEZB1；NOT（NOT（X）NOT（NOT（0）NOT（1）0，當X0；NOT（NOT（1）NOT（0）1，當X1；NOT（NOT（I）NOT（I1）I2I，當XI且X0，X1。例設(shè)IZ32101234則NOTZB1II121010345顯然NOTZB1NOTZB1II,FORI0,I1326規(guī)約實例設(shè)計1、自然數(shù)（NATURALNUMBER）規(guī)約設(shè)計NATSIGNATURESORTSORTNATCONSTRUCTORSFUNCTZERONATSUCCNATNATCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORNATURALNUMBERNATGENERATEDBYZERO,SUCCAXIOMSAXIOMSX,YNATZEROSUCCXSUCCXSUCCYXYENDAXIOMS2、整數(shù)（INTEGER）規(guī)約設(shè)計INTSIGNATURESORTSORTINTCONSTRUCTORSFUNCTZEROINTSUCCINTINTPREDINTINTCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORINTEGERINTGENERATEDBYZERO,SUCC,PREDAXIOMSAXIOMSXINTSUCCPREDXXPREDSUCCXXENDAXIOMS3、真值（TRUTHVALUE）規(guī)約設(shè)計BOOLSIGNATURESORTSORTBOOLCONSTRUCTORSFUNCTTRUEBOOLFALSEBOOLCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORTRUTHVALUEBOOLGENERATEDBYTRUE,FALSENONCONSTRUCTORSFUNCTNOTBOOLANDBOOLBOOLBOOLORBOOLBOOLBOOLAXIOMSAXIOMSX，YBOOL；（TRUEFALSE）NOT（TRUE）FALSENOT（NOT（X）XAND（TRUE，X）XAND（FALSE，X）FALSEOR（X，Y）NOT（AND（NOT（X），NOT（Y）ENDAXIOMS4、結(jié)合率（ASSOCIATION）規(guī)約設(shè)計ASSOCSORTSORTDATAFUNCTIONSYMBOLFUNCTDATADATADATAAXIOMSAXIOMSX,Y,ZDATAXYZXYZENDAXIOMS5、堆棧（STACK）規(guī)約設(shè)計STACKSORTDATA,STACKFUNCTEMPTYSTACKPUSHDATASTACKSTACKTOPSTACKDATAPOPSTACKSTACKCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORSTACKSTACKGENERATEDBYEMPTY,PUSHAXIOMSAXIOMSDDATA,SSTACKTOPPUSHD,SDPOPPUSHD,SSPOPEMPTYEMPTYENDAXIOMS6、帶ERROR堆棧（STACKWITHERRORELEMENT）規(guī)約設(shè)計ESTACKSORTEDATA,ESTACKFUNCTERRORDEDATAEMPTY,ERRORSTESTACKPUSHEDATAESTACKESTACKTOPESTACKEDATAPOPESTACKESTACKCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORSTACKWITHERRORELEMENTESTACKGENERATEDBYERRORST,EMPTY,PUSHAXIOMSAXIOMSDEDATA,SESTACKDERRORDSERRORSTTOPPUSHD,SDPOPPUSHD,SSTOPERRORSTERRORDPOPERRORSTERRORSTTOPEMPTYERRORDPOPEMPTYERRORSTPUSHD,ERRORSTERRORSTPUSHERRORD,SERRORSTENDAXIOMS7、帶結(jié)點標識符的二叉樹（BINARYTREEWITHNODEIDENTIFICATION）規(guī)約設(shè)計BTREESORTDATA,BTREEFUNCTEMPTYBTREENODEBTREEDATABTREEBTREELEFTBTREEBTREERIGHTBTREEBTREELABELBTREEDATACONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORBINARYTREEBTREEGENERATEDBYEMPTY,NODEAXIOMSAXIOMST1,T2BTREE,DDATALEFTNODET1,D,T2T1LABELNODET1,D,T2DRIGHTNODET1,D,T2T2LEFTEMPTYEMPTYRIGHTEMPTYEMPTYENDAXIOMS8、方位（ORIENTATION）規(guī)約設(shè)計ORIENTATIONSORTORIENTATIONFUNCTNORTH,EAST,SOUTH,WESTORIENTATIONTURNLEFT,TURNRIGHT,OPPOSITEORIENTATIONORIENTATIONCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORORIENTATIONORIENTATIONGENERATEDBYNORTH,EAST,SOUTH,WESTAXIOMSTURNLEFTNORTHWESTTURNLEFTWESTSOUTHTURNLEFTSOUTHEASTTURNLEFTEASTNORTHTURNRIGHTNORTHEASTTURNRIGHTEASTSOUTHTURNRIGHTSOUTHWESTTURNRIGHTWESTNORTHOPPOSITENORTHSOUTHOPPOSITEEASTWESTOPPOSITESOUTHNORTHOPPOSITEWESTEASTENDAXIOMS9、方位（ORIENTATION）規(guī)約設(shè)計ORIENTATION1SORTORIENTATIONFUNCTNORTH,EAST,SOUTH,WESTORIENTATIONTURNLEFT,TURNRIGHT,OPPOSITEORIENTATIONORIENTATIONCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORORIENTATIONORIENTATIONGENERATEDBYNORTH,EAST,SOUTH,WESTAXIOMSORORIENTATIONTURNLEFTNORTHWESTTURNLEFTWESTSOUTHTURNLEFTSOUTHEASTTURNLEFTEASTNORTHTURNRIGHTTURNLEFTOROROPPOSITEORTURNLEFTTURNLEFTORENDAXIOMS可以證明ORIENTATIONORIENTATION1即證明SIGORIENTATIONSIGORIENTATION1MODORIENTATIONMODORIENTATION1證明方法1證明SIGORIENTATIONSIGORIENTATION1根據(jù)以上給出的2個規(guī)約,顯然2證明MODORIENTATIONMODORIENTATION1需證明EAXIOMSORIENTATION1EAXIOMSORIENTATIONEAXIOMSORIENTATIONEAXIOMSORIENTATION133大型規(guī)約設(shè)計331規(guī)約操作符及語義1規(guī)約組合（COMBINATION）操作（1）定義（COMBINATION）SP1，SP2是兩個規(guī)約，其組合操作SP1SP2是一個規(guī)約且定義如下SIG（SP1SP2）DEFSIG（SP1）SIG（SP2）SP1SP2DEFAASIG（SPI）SPI，I1，2AASIG（SP1）SP1AASIG（SP2）SP2說明組合操作SP1SP2實際上是將規(guī)約SP1的標記和公理，分別與SP2的標記和公理進行“合并”（）操作。SP表示規(guī)約SP包含的模型集合