软件需求分析图形表示与形式描述

软件需求分析图形表示与形式描述传统图形描述技术建模及语义中国谚语EINBILDZEIGTUEBERTAUSENDSAETZEAPICTURESHOWSMORETHAN1000SENTENCES1、三种主要传统图形描述技术（1）数据流图技术DFD（DATAFLOWDIAGRAM）描述一个信息系统的数据（信息）流。（2）实体关系图技术ERD（ENTITYRELATIONSHIPDIAGRAM）描述一个信息系统的逻辑数据结构。（3）状态转换图技术STD（STATETRANSITIONDIAGRAM）描述一个信息系统的状态转换过程。2、基于图形描述技术的需求分析模型（1）需求分析模型的基本功能描述用户需求建立创建软件设计的基础定义软件开发后的验证条件集合（2）需求分析模型结构图21给出了基于图形描述技术的需求分析模型结构。图21需求分析模型结构（摘自PRESSMAN，SOFTWAREENGINEERING，P300）其中（1）核心部分DATADICTIONARY（DD，数据字典）存储所有软件使用或产生的对象数据的描述。（2）中间层DATAFLOWDIAGRAM（DFD，数据流图）描述数据在经过系统时的转换过程图示数据流函数ENTITYRELATIONSHIPDIAGRAM（ERD，实体关系图）图示数据之间的关系STATETRANSITIONDIAGRAM（STD，状态转换图）描述系统接收外部事件后的状态变化（3）外部层PROCESSSPECIFICATION（PSPEC，过程规约）描述DFD中定义的每个函数DATAOBJECTDESCRIPTION（数据对象描述）描述ERD中每个数据对象的属性CONTROLSPECIFICATION（CSPEC，控制规约）描述软件控制外观的附加信息231数据流图DFD及语义1定义（DFD）数据流图DFD技术描述流经一个信息系统的数据（信息）流，主要包括（1）数据的输入与输出数据是如何进入系统或从系统离开；（2）数据处理站点在哪里数据是怎样处理的；（3）存储单元数据是在哪里存储的。2定义（DFD符号）数据（信息）的源点/终点数据（信息）加工或逻辑处理数据（信息）存储数据（信息）流3实例研究汽车租赁数据流图（1）一个汽车租赁数据流图EURENTDFD见图22。图22EURENTDFD（摘自HAGGENMUELLER,WIRSINGMETHODENDERSOFTWAREENTWICKLUNG,P29）图中KUNDE用户或汽车租赁者MAKEBOOKINGS租车登记OBTAINPAYMENT得到支付VEHICLEDEPARTURESFUNCTFPREDPSGENERATEDBYC定义公理AXIOMSEENDAXIOMS其中,S规约中包括的所有数据类型的集合F所有函数符号的集合P所有谓词符号的集合CS的构造操作符集合,且CFE公理集合,表示所有的特性（CHARACTERISTICPROPERTIES）上述规约可书写成如下规约SP标记，公理EBOOLTHVALUE的规约设计（1）公理规约（AXIOMATICSPECIFICATION）BOOL0SIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLPREDICATESYMBOLSPREDNOTBOOLBOOLAXIOMSAXIOMS，XBOOLNOTTRUEFALSENOTNOT（X）XENDAXIOMS2PROLOG规约PROLOGSPECIFICATIONREMARKN个变量的函数将通过N1变量的关系定义，函数的值变量置于N1个关系的最后一位BOOL_PLSIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLPREDICATESYMBOLSPREDNOTBOOLBOOLAXIOMSAXIOMSX,YBOOLNOTTRUE,FALSENOTX,YNOTY,XENDAXIOMS3逻辑规约LOGICSPECIFICATIONREMARK一个自变量的布尔函数将通过一个变量的关系表达BOOL_LSIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLPREDICATESYMBOLSPREDNOTBOOLAXIOMSAXIOMSNOTFALSENOTTRUEENDAXIOMS4带构造操作符的公理规约SPECIFICATIONWITHCONSTRUCTORBOOLTSIGNATURESORTSORTBOOLFUNCTIONSSYMBOLFUNCTTRUEBOOLFALSEBOOLCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORTRUTHVALUEBOOLGENERATEDBYTRUE,FALSENONCONSTRUCTORSYMBOLFUNCTNOTBOOLBOOLAXIOMSAXIOMSXBOOLNOTTRUEFALSENOTNOTXXENDAXIOMS322标记SIGNATURE1定义（SIGNATURE）一个标记是一个三元组（S，F，P），其中S是一个类集（SETOFSORTS），F是一个定义在SS上的函数符号集，其中S为定义域，SS为函数F,S的值域，P是一个定义在S上的谓词符号集。REMARK（1）标记描述规约的语法（SYNTAXOFSPECIFICATION）（2）FF,S可写成FS1S2,SNS（3）PP可写成PS1S2,SN（4）规约SP的标记可写成SIG（SP）SP2案例研究例1上述逻辑规约LOGICSPECIFICATIONBOOL_L的标记SIG（BOOL_L）SBOOLF（F）BOOLNN0且FTRUE，FALSE常量FOTHERWISE空集P（P）BOOLNN0且PNOT，其中为布尔运算POTHERWISE例2公理规约BOOL0及BOOLT的标记SIG（BOOL0）SIG（BOOLT）SBOOL；F（F）BOOLNN0且FTRUE，FALSE常量FNOT函数FOTHERWISE；空集P（P）BOOLNN0且P其中为布尔运算POTHERWISE思考（1）找出程序中所有类型与运算符号有利于程序理解；（2）可用于程序测试、项目管理、程序度量等；（3）可用于研究程序体系结构等（4）语法、语义匹配，语义查询等；（5）基于语义的WEB服务应用等。3定义标记被称为是代数的，只有当等式“”是其中唯一的关系运算符。例上述规约BOOL0和BOOLT的标记是代数的；规约BOOL_L不是代数的，因为存在关系运算符“NOT”。323项（TERM）每个标记（S，F，P）定义了一个表达式的集合，称为项集，其中项元素是由自由变量X和中的函数符号构成。XS所有程序中的表达式都是由和X构成的。1定义（项的归纳定义）（1）设为标记，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举例数学表达式中的项表达式A2ABB2项A2，AB，B2324结构（STRUCTURE）一个结构可看作对标记中符号的进一步定义和说明，其中（1）每个类对应一个值的集合；（2）每个函数符号定义一个函数；（3）每个谓词运算符号定义一个关系。1定义（结构）一个结构（也称代数）A包括（1）一个家族（FAMILY，或集合的集合）（AS）SS，其中AS为非空的值的集合；（2）一个函数集FAS1AS2ASNAS，其中FF,S；（3）一个谓词集PS1S2,SN，其中PP。所有的具有标记为的结构的类（CLASS）表示为STRUCT（）。2案例研究例设SIG（BOOLT），则结构包括（1）真值的标准模块BBBOOLT，F；TRUEBT；FALSEBF；NOTB（T）F；NOTB（F）T；XBYIFFXY；（2）在自然数上定义的结构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）定义在整数上的结构ZBZBBOOLZ；TRUEZB1；FALSEZB0；NOTZB（1）0；NOTZB（0）1；NOTZB（I）I，FORI0I1，IZ；XZBYIFFXY；（5）定义在整数上的结构ZB1ZB1BOOLZ；TRUEZB11；FALSEZB10；NOTZB1（1）0；NOTZB1（0）1；NOTNB1（I）I1，FORI0I1，IZ；XZB1YIFFXY；（6）最小的结构UBUBBOOL1；TRUEUBFALSEUB1；NOTUB（1）1；（UBBOOL）DEF11；说明1软件的实现是多样化的；2软件的正确性是相对的。325公理/代数规约REMARK简单公理规约可以通过其标记和一个好形公式（WFF）集合E定义。1定义（公理规约）设（S，F，P）是一个标记，E是一个定义的好形公式集合，则SP，E是一个公理规约。NOTE（1）公理规约SP是代数的，如果等式“”是唯一的谓词符号，即SPS，S（2）好形公式WFF（WELLFORMEDFORMULA）的定义见离散数学相关教材和参考资料。一阶谓词逻辑FIRSTORDERLOGIC；只包含函数符和等式“”；由原子公式、布尔运算符及量词（全称量词和存在量词）组成。2定义（规约语义）规约SP，E的语义可通过标记和模型类（CLASSOFMODELS）定义，即标记SIG（SP）SIG（，E），模型类MOD（SP）MOD（，E）ASTRUCT（）AGFORALLGE，其中，A为模型，STRUCT（）为结构，AG为“A满足于G”，GE表示G为公理集合E中的等式，MOD（SP）可表示成SP。3实例研究证明上述结构B、NB、NB1、ZB、UB为规约BOOL0的模型；ZB1不是规约BOOL0的模型。证明（1）B是规约BOOL0的模型证明义务需证明B结构定义使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是规约BOOL0的模型证明义务需证明NB结构定义使BOOL0中的每个公理成立。NOT（TRUENB）NOT（1）0FALSENB；NOT（NOT（X）NOT（NOT（2I）NOT（2I1）2IX，当X2INB；NOT（2I）2I1X，当X2I1NB。（3）NB1是规约BOOL0的模型证明义务需证明NB1结构定义使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是规约BOOL0的模型证明义务需证明UB结构定义使BOOL0中的每个公理成立。NOT（TRUEUB）NOT（1）1FALSEUB；NOT（NOT（X）NOT（NOT（1）NOT（1）1X，当X1。（5）ZB是规约BOOL0的模型证明义务需证明ZB结构定义使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不是规约BOOL0的模型证明义务需证明ZB结构定义不能使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。例设IZ32101234则NOTZB1II121010345显然NOTZB1NOTZB1II,FORI0,I1326规约实例设计1、自然数（NATURALNUMBER）规约设计NATSIGNATURESORTSORTNATCONSTRUCTORSFUNCTZERONATSUCCNATNATCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORNATURALNUMBERNATGENERATEDBYZERO,SUCCAXIOMSAXIOMSX,YNATZEROSUCCXSUCCXSUCCYXYENDAXIOMS2、整数（INTEGER）规约设计INTSIGNATURESORTSORTINTCONSTRUCTORSFUNCTZEROINTSUCCINTINTPREDINTINTCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORINTEGERINTGENERATEDBYZERO,SUCC,PREDAXIOMSAXIOMSXINTSUCCPREDXXPREDSUCCXXENDAXIOMS3、真值（TRUTHVALUE）规约设计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、结合率（ASSOCIATION）规约设计ASSOCSORTSORTDATAFUNCTIONSYMBOLFUNCTDATADATADATAAXIOMSAXIOMSX,Y,ZDATAXYZXYZENDAXIOMS5、堆栈（STACK）规约设计STACKSORTDATA,STACKFUNCTEMPTYSTACKPUSHDATASTACKSTACKTOPSTACKDATAPOPSTACKSTACKCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORSTACKSTACKGENERATEDBYEMPTY,PUSHAXIOMSAXIOMSDDATA,SSTACKTOPPUSHD,SDPOPPUSHD,SSPOPEMPTYEMPTYENDAXIOMS6、带ERROR堆栈（STACKWITHERRORELEMENT）规约设计ESTACKSORTEDATA,ESTACKFUNCTERRORDEDATAEMPTY,ERRORSTESTACKPUSHEDATAESTACKESTACKTOPESTACKEDATAPOPESTACKESTACKCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORSTACKWITHERRORELEMENTESTACKGENERATEDBYERRORST,EMPTY,PUSHAXIOMSAXIOMSDEDATA,SESTACKDERRORDSERRORSTTOPPUSHD,SDPOPPUSHD,SSTOPERRORSTERRORDPOPERRORSTERRORSTTOPEMPTYERRORDPOPEMPTYERRORSTPUSHD,ERRORSTERRORSTPUSHERRORD,SERRORSTENDAXIOMS7、带结点标识符的二叉树（BINARYTREEWITHNODEIDENTIFICATION）规约设计BTREESORTDATA,BTREEFUNCTEMPTYBTREENODEBTREEDATABTREEBTREELEFTBTREEBTREERIGHTBTREEBTREELABELBTREEDATACONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORBINARYTREEBTREEGENERATEDBYEMPTY,NODEAXIOMSAXIOMST1,T2BTREE,DDATALEFTNODET1,D,T2T1LABELNODET1,D,T2DRIGHTNODET1,D,T2T2LEFTEMPTYEMPTYRIGHTEMPTYEMPTYENDAXIOMS8、方位（ORIENTATION）规约设计ORIENTATIONSORTORIENTATIONFUNCTNORTH,EAST,SOUTH,WESTORIENTATIONTURNLEFT,TURNRIGHT,OPPOSITEORIENTATIONORIENTATIONCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORORIENTATIONORIENTATIONGENERATEDBYNORTH,EAST,SOUTH,WESTAXIOMSTURNLEFTNORTHWESTTURNLEFTWESTSOUTHTURNLEFTSOUTHEASTTURNLEFTEASTNORTHTURNRIGHTNORTHEASTTURNRIGHTEASTSOUTHTURNRIGHTSOUTHWESTTURNRIGHTWESTNORTHOPPOSITENORTHSOUTHOPPOSITEEASTWESTOPPOSITESOUTHNORTHOPPOSITEWESTEASTENDAXIOMS9、方位（ORIENTATION）规约设计ORIENTATION1SORTORIENTATIONFUNCTNORTH,EAST,SOUTH,WESTORIENTATIONTURNLEFT,TURNRIGHT,OPPOSITEORIENTATIONORIENTATIONCONSTRUCTORAXIOMINDUCTIONPRINCIPLEFORORIENTATIONORIENTATIONGENERATEDBYNORTH,EAST,SOUTH,WESTAXIOMSORORIENTATIONTURNLEFTNORTHWESTTURNLEFTWESTSOUTHTURNLEFTSOUTHEASTTURNLEFTEASTNORTHTURNRIGHTTURNLEFTOROROPPOSITEORTURNLEFTTURNLEFTORENDAXIOMS可以证明ORIENTATIONORIENTATION1即证明SIGORIENTATIONSIGORIENTATION1MODORIENTATIONMODORIENTATION1证明方法1证明SIGORIENTATIONSIGORIENTATION1根据以上给出的2个规约,显然2证明MODORIENTATIONMODORIENTATION1需证明EAXIOMSORIENTATION1EAXIOMSORIENTATIONEAXIOMSORIENTATIONEAXIOMSORIENTATION133大型规约设计331规约操作符及语义1规约组合（COMBINATION）操作（1）定义（COMBINATION）SP1，SP2是两个规约，其组合操作SP1SP2是一个规约且定义如下SIG（SP1SP2）DEFSIG（SP1）SIG（SP2）SP1SP2DEFAASIG（SPI）SPI，I1，2AASIG（SP1）SP1AASIG（SP2）SP2说明组合操作SP1SP2实际上是将规约SP1的标记和公理，分别与SP2的标记和公理进行“合并”（）操作。SP表示规约SP包含的模型集合