程序设计方法学

12 04 2020 华东师大计算机科学技术系 1 第六章程序设计的形式化方法 软件新技术智能化技术扩大软件功能的关键途径自动化技术提高软件生产率的根本途径集成化技术助于提高生产率 提高质量并行化技术提高系统实效的关键技术自然化技术实现社会信息化 12 04 2020 华东师大计算机科学技术系 2 重要方向攻克的关键教技术网络体系传感器网与因特网的高效融合集成芯片从Systemonchip到Chipondemount虚拟计算资源聚合的有效性和可靠性验证软件工程基于网络环境的需求工程知识处理挖掘从消息到知识到决策的元知识高效系统在高性 效 能计算系统中系列关注信息安全信息教育 12 04 2020 华东师大计算机科学技术系 3 跨越源之识规律 创新根植辨短长 汪成为院士 12 04 2020 华东师大计算机科学技术系 4 软件自动化的三个层次 软件自动化 自动程序设计 广义 尽可能地借助计算机系统实现软件开发狭义 从形式化的软件功能规范到可执行程序代码这一过程的自动化从软件需求规范 软件功能 性能规范的转换解决从 非形式 形式 难度很大 寄希望于受限自然语言方面的突破从软件功能 性能规范 软件设计从 做什么 如何做 从软件设计规范 高级语言已有相当的进展 出现了许多工具 12 04 2020 华东师大计算机科学技术系 5 1概述 一 重要意义软件发展中的问题 整体功能不强 缺乏智能 质量欠佳 生产效率低软件自动化是提高软件生产率的根本途径软件自动化的前提是形式化因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的前提 12 04 2020 华东师大计算机科学技术系 6 二 发展状况有30多年历史Dijkstra Hoare 程序验证Scott Stratchey 程序语义形式化方法 FormalMethod 通过严格的规范化的数学理论来描述软件系统 做什么 的方法 需要形式规范语言的支持 形式规范语言 提供了一个称为语法域的记号系统 一个称为语义域的目标集合 以及一组精确定义的哪些目标系统满足那个规范的规则 12 04 2020 华东师大计算机科学技术系 7 因此 形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型的方法 形式系统是二元组 L Cn L 语言 形式规范语言 Cn 对应关系 由推理规则构成在软件规范方法方面的代表性成果有 基于异调代数的代数方法特点 用抽象代数中的公理化方法来刻画抽象数据类型中运算的性质 而不涉及数据的具体表示 基本理论 代数语义 12 04 2020 华东师大计算机科学技术系 8 抽象模型方法特点 基于某些已知的ADT来给出待定义的ADT的抽象模型 用抽象模型来刻画待定义的ADT中运算的功能 基本理论 指称语义 状态机方法特点 通过状态的转换来刻画输入与输出间的关系基本理论 操作语义 高阶软件方法 HOS 基于控制公理基本理论 公理语义 12 04 2020 华东师大计算机科学技术系 9 在软件规范语言方面的代表性成果有 一阶谓词演算组成语言80年代 Z语言 Larch语言 VDM语言90年代 面向实时及分布式的LOTOS语言 面向对象的Z Object Z VDM 等三 分类 基于模型的方法给出系统 程序 状态和状态变换与操作的显式的表示但亦是抽象的定义 不涉及并发的行为 如 Z VDM 12 04 2020 华东师大计算机科学技术系 10 代数方法通过联系不同的操作间的行为关系给出操作的隐式定义 未给出并发的显式表示 如 OBJ Larch 过程代数方法给出并发过程的一个显式模型 并通过过程间允许的可观察的通信上的限制来约束表示行为 如 CSP 通信顺序进程 和CCS 通信系统计算 基于逻辑的方法采用逻辑来描述系统的特性 包括程序行为的低级规范和系统时间的行为规范 如 时态逻辑 模态逻辑 12 04 2020 华东师大计算机科学技术系 11 基于网络的方法根据网络中的数据流显式地给出系统的并发模型 包括数据从一个结点流向另一个结点的条件 如 Petri网 谓词变换网 12 04 2020 华东师大计算机科学技术系 12 四 形式化软件开发方法采用软件生命周期的变换模型 其实质是将现实世界的需求反映成软件的模型化过程 涉及三方面模型 现实世界 模型表示和计算机系统 因此开发的过程就是从三方面对系统进行描述和转换的过程 开发过程中的任务为 模型获取 从现实世界向模型表示的过程 涉及如何提取 表示模型 对应需求分析 设计等活动 模型验证 对得到的模型表示进行检验 判断是否捕获了所有的需求 该模型是否具有所期望的特性 模型变换 是向计算机系统变换的过程 关键的任务是一致性检测 对应实现和测试 12 04 2020 华东师大计算机科学技术系 13 三项任务分别对应三方面的活动 1 形式化规范 规格 软件规范是指对软件系统对象及用来对系统对象进行操作的方法的集合 以及对所开发系统中的各对象在生命周期间的集体行为的描述 对应与软件生命周期的各个阶段 规范应该理解为是一个多阶段的行为 见例图规范可以采用非 半形式化的方法来描述 形式化规范精确地描述了用户的需求 软件系统的功能及各种性质 其描述的是 做什么 而不考虑 如何做 因此 在理解 掌握形式规范语言和方法的基础上对所描述的系统的全面 深入的了解 给出恰如其分的描述上至关重要的 12 04 2020 华东师大计算机科学技术系 14 包含各规格阶段的生命周期模型例 需求分析 BS SRD 系统设计1 DS 系统设计2 PS 软件开发 代码实现 软件测试 运行 SRD 软件需求文档BS 行为规范DS 设计规范PS 程序规范 12 04 2020 华东师大计算机科学技术系 15 软件系统规范的形式化方法 从形式化规范到目标软件系统的可实现和可执行角度 可分为三类 操作类 此类方法基于状态和转移 通过可执行模型来描述系统 模型本身能够采用静态分析和模型执行而得到验证 如 有限状态机 Statecharts Petri网等 描述类 此类方法基于数学公理和概念 通过逻辑或代数给出系统状态空间 具有高度抽象的特点 便于通过自动工具进行验证 如 基于代数的Z VDM Larch等 基于逻辑的命题线性时态逻辑 一阶线性时态逻辑 计算树逻辑等 双重类 此类方法兼具二者的特点 如 扩展状态机 实时时态逻辑等 12 04 2020 华东师大计算机科学技术系 16 形式化规范的成功案例 IBM商用信息系统 牛津大学和Hursley实验室使用Z语言 总体成本降低9 获皇家技术成就奖 Praxis公司使用VDM开发的伦敦机场信息显示系统 软件质量大为提高 故障率0 75 2 20 每K行代码 其他领域 数据库 HP医用仪器实时数据库系统电子仪器 Tektronix系列谐波发生器硬件 INMOS浮点处理器 INMOS中T9000系列虚拟信道处理器运输系统 巴黎地铁自动火车保护系统 以色列机载航空电子软件等等 12 04 2020 华东师大计算机科学技术系 17 形式化验证软件开发中错误发现的越晚修改的代价越大 与传统方法不同的是形式化方法要求在完成形式规范后就进行形式验证 形式验证主要技术包括模型检验和定理证明 模型验证是一种基于有限状态机模型并检验该模型的期望特性的技术 即对模型的状态空间进行搜索 以确认该系统具有某些性质 终止性依赖于模型的有限性 优点是 完全自动化 速度快 可用于系统的部分规范 缺点是 状态爆炸问题 因而极大地限制其实际使用范围 有序二叉决策图 OrderedBinaryDecisionDiagrams 是一种表述状态转移系统的高效率的方法 目前可以处理100 200个状态变量 状态数达10120的系统 12 04 2020 华东师大计算机科学技术系 18 模型检验需要工具的支持 已有的工具有 时态逻辑模型检验工具 如 EMC CESAR SMV Nurphi SPIN UV等 行为一致检验工具 如 FRD Cospan FormalCheck等复合检验工具 如 HSIS VIS STcP等贝尔实验室用FormalCheck对其高级数据链路控制器进行验证 从6个性能的规范中发现一个失败 进而发现一个影响信道流量的Bug 基于SMV输入语言建立了IEEEFuturebus 896 1 1991标准下cache一致协议精确模型 通过SMV的验证 发现了原先未找到和潜在的错误 此工作是第一次从IEEE标准中发现错误 12 04 2020 华东师大计算机科学技术系 19 定理证明采用逻辑公式来规范系统及其性质 这儿的逻辑由一个具有公理或推理规则的形式系统给出 进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质 定理证明可以处理无限状态空间问题 粗略地分为自动和交互两种类型 自动定理证明系统是通用搜索过程 在解决各种组合问题中比较成功 交互式定理证明系统需要与用户进行交互 要求用户能提供验证中创造性最强的部分 如断言等 因此效率较低 较难用于大系统的验证 12 04 2020 华东师大计算机科学技术系 20 现有的定理证明器有 用户导引自动推理工具 如 ACL2 Eves LP Nqthn和RRL等它们由引理或定义序列导引 每一个定理采用已建立的推演 引理驱动重写和简化启发式来自动证明 证明检验器 如 Coq HOL LEGO等 复合证明器 如 Analytica中将定理证明和符号代数系统Mathematica复合 PVS和Step将决策过程 模型检验和交互式证明复合在一起 基于符号代数运算的自动证明用于证明Pentium中SRT算法的正确性 查出了一个由故障商数字选择表引起的错误 12 04 2020 华东师大计算机科学技术系 21 程序求精 又称程序变换 是将自动推理和形式化方法相结合而形成的一门新技术 研究从抽象的形式规范推演出具体的面向计算机的程序代码的全过程 基本思想是 用一个抽象程度低 过程性强的程序去替代一个抽象程度高 过程性弱的程序 并保持二者功能的一致性 这儿的 程序 是广义的 程序 是对规范 设计文档 程序代码的统称 按这种观点 程序开发的过程就是从最高层的程序开始 通过一系列的求精变换 每一次都降低一些抽象程度或增加一些可执行性 最终得到能指导计算机明确执行的程序代码 12 04 2020 华东师大计算机科学技术系 22 在进行求精的过程中必须要保证程序的正确性 即保证程序是满足最初的形式规范的 程序的这种正确性可以通过求精过程中所遵循的一系列规则来保证 也可以采用验证工具来证明 程序求精技术是形式化方法研究的一个热点 尽管目前真正用于实际软件开发过程中并不多 但是这是一个很重要的方向 典型的方法有 IBMHursley公司和牛津大学PRG程序设计研究组提出的针对Z规范的求精方法 CarrollMorgan的规则求精方案 见ProgrammingfromSpecifications一书 12 04 2020 华东师大计算机科学技术系 23 五 认识形式化方法成长至今争议声不断 应正确地认识形式化方法 在结合到具体的软件开发过程时应考虑 应用的类型 考虑问题领域的特点和模型的复杂性规模和结构 较适应中等规模的系统 大型系统应考虑具有良好的结构类型的选择 应从所确定的目标出发考虑采用的形式化方法的类型形式化的级别 应先确定应用的关键程度 项目规模 可用资源等确定采用非 半或高度形式化的描述 12 04 2020 华东师大计算机科学技术系 24 使用范围 尽管形式化可以适应所有的开发阶段 但通常应有选择的使用 对那些安全性 可信性要求高的构件应用高度的形式化工具 工具的支持在形式化方法中具有重要的位置 应根据具体项目 综合上述因素选择合适的工具 12 04 2020 华东师大计算机科学技术系 25 12 04 2020 华东师大计算机科学技术系 26 结论 形式化的方法不是灵丹妙药 而是一种改进系统可靠性的方法 12 04 2020 华东师大计算机科学技术系 27 2 基于代数方法的规范语言 OBJ 该方法的理论工作由Guttage提出基本格式 语法定义 语义定义 限制说明 语法定义 指出类型的语法信息和检查信息作用 定义了类型与函数语义定义 指出了类型和操作间的公理作用 定义了类型的语义限制说明 给出各种限制 防止二义性作用 和语义定义一起给出重写规则基础抽象是整数集 函数定义了它们之间的相互关系 这样规范的值与函数形成一个抽象代数 12 04 2020 华东师大计算机科学技术系 28 形式定义 代数规范是三元组 S E 其中 S 是标记 S是类集 是操作集 E是有限个方程的集合 形式为L R 其中L R S 称为项 项的定义 S中的变元是项 常量是项 项经过操作集 中的操作后也是项有工具支持的二个代数规范语言是 AFFIRM OBJ 12 04 2020 华东师大计算机科学技术系 29 一 OBJ简介 一种代数形式规范语言 最基本的概念是ADT 抽象数据类型 每个ADT描述一个客体 具有很强的独立定义和数据抽象的机制 支持层次化设计 即在定义高层ADT时可以使用下层已定义的ADT 用OBJ书写形式规范的过程就是用代数等式 方程 定义ADT的过程 是一种基于代数方程逻辑的代数形式语义 又具有一种基于把代数方程解释为重写规则的操作语义 可利用这种语义证明程序的正确性 12 04 2020 华东师大计算机科学技术系 30 二 基本形式 一个OBJ的形式规范说明是诸多ADT定义的集合 每个ADT具有如下形式 其中obj与jbo是必须的 其余部分任选 12 04 2020 华东师大计算机科学技术系 31 例1 定义ADTNATURALobjNATURALsortsnatops0 nat 0无定义域 常量 succ nat nat nat上的一目运算 表示运算对象 jbo在定义ADT时若需要用到低层已定义ADTL中的运算 可在obj处用 L指出 多个时用空格分隔 例子 12 04 2020 华东师大计算机科学技术系 32 例2 在NATURAL的基础上定义ADDobjADD NATURALops natnat natvarsx y nateqns 0 x x succ x y succ x y jbo下面将给出一个较大的形式规范定义 对整数序列进行分类 在规范中自底向上的顺序分别定义了多个ADT 如 Boolean Integer seq INT sort seq INT等 12 04 2020 华东师大计算机科学技术系 33 例3 对一个整型数列分类的形式规范1 objBoolean TRUTH TRUTH是OBJ内部已varsa Boolean 定义的ADT 它具有eqns not T F T和F两个常量 not F T not not a a Tanda a aandF F Tora T Fora a jbo 12 04 2020 华东师大计算机科学技术系 34 2 整型ADT 对下述十个运算的规则容易给出 故省略了objInteger BooleansortsINTops INT INT INTINT INT INTINT INT INTINT INT div INTINT INT mod INTINT INT INTINT Boolean INTINT Booleanjbo 12 04 2020 华东师大计算机科学技术系 35 3 定义整型字符串ADTobjseq INT Integersortsseq INTops seq INT 空 seq INT 常量 seq INTseq INT seq INT 链接hd seq INT INT 头元素tl seq INT seq INT 尾串len seq INT INT 长度varsi INTs seq INT 12 04 2020 华东师大计算机科学技术系 36 eqns s s s s hd 0 hd i i hd i s i tl tl i tl i s s len 0 lens succ len tls ifs jbo 12 04 2020 华东师大计算机科学技术系 37 4 定义比较ADTobjsort seq split seq INTIntegerops seq INT INT seq INTvarss seq INTi x INTeqns x i x i s x i x ifi x i s x ifi x jbo 12 04 2020 华东师大计算机科学技术系 38 5 定义分类ADT的规范objsort seq INT sort seg splitseq INTIntegerBooleanopssort seq INT seq INTis sorted seq INT Booleanvarss s1 s2 seq INTi j x INTeqns is sorted T is sorted i T is sorted i j i j is sorted i j s i jandis sorted j s sorts sifis sorteds 12 04 2020 华东师大计算机科学技术系 39 sort i j sort j i ifi j sort i j s sort j i s ifi j sort s i j sort s j i ifi j sort s1 i j s2 sort s1 j i s2ifi j sort tls hds sortsifs s x tls x ifs andhds x hds tls x ifs andhds x s x s x hds tls x ifs andhds x jbo 12 04 2020 华东师大计算机科学技术系 40 三 运算的性质 从功能上可以将运算分为四类 初始化运算不以任何别的类型客体作为它的输入 其结果是具有自身类型的值 如 seq INT 2 构造运算以自身类型客体和别的类型客体为输入 产生具有自身类型的结果 如 3 修改运算修改自身类型客体的变量如 tl 4 观察运算以自身类型客体为输入 得出具有别的类型客体的结果 如 len 12 04 2020 华东师大计算机科学技术系 41 四 抽象的计算程序 例4 定义自然数类型的栈运算的ADTobjStack IntegerBooleansortsstackopscreate stack 空栈 push stackINT stackpop stack stacktop stack INT ERR empty stack Boolean 12 04 2020 华东师大计算机科学技术系 42 varss stackn INTeqns empty create T empty pushs n F pop create create pop push s n s top create ERR top push s n n jbo 12 04 2020 华东师大计算机科学技术系 43 抽象计算程序的计算可以归结为代数系统中的重写规则的应用 而得到计算的结果 例5 设抽象计算程序为 create push s 5 push s 3 pop s top s 则top s top pop s top pop push s 3 top pop push push s 5 3 top push s 5 5由此可知 这种方法可以机械执行 12 04 2020 华东师大计算机科学技术系 44 正确性证明 依赖相应的ADT中定义的运算规范 可以证明程序的正确性 方法为 将代数等式视为重写规则 即将等式L R视为L R L被定义为R 就可以用于程序的正确性证明 12 04 2020 华东师大计算机科学技术系 45 3 基于模型方法的规范语言VDMTheViennaDevelopmentMethod 一 概况VDM由IBM的Vienna实验室20世纪70年代提出的的一种形式化方法 最初是为了解决用形式化方法来开发编译系统 使语言的语法 语义的定义更为严格 更加系统化 如实现PL 1语言的语义规范 当时用VDL用于语言的注释 得到广泛的应用VDM在欧洲得到发展 从70年代末到90年代在欧美许多研究机构和大学得到广泛的应用 如曼彻斯特大学讲其作为必修课 以后逐渐称为一般的软件开发方法 12 04 2020 华东师大计算机科学技术系 46 1996年国际标准化组织 ISO 制定了VDM的国际化版本VDM SL VDMSpecificationLanguage 目前VDM已称为应用最为广泛的形式化规范语言 VDM是一种功能构造性规范技术 由一阶谓词逻辑和已经建立的ADT来描述每个运算或函数的功能 基本思想是ADT 数学概念和符号来规定运算或函数的功能 而且这种规定的过程是结构化的 其目的是要在系统实现之前简单而又明确地指出软件系统要完成的功能 支持程序正确性的证明 用Hoare的前 后断言描述运算的规范 12 04 2020 华东师大计算机科学技术系 47 二 VDM的形式规范的基本组成形式 VDM形式规范由三部分组成 状态 类型不变式 运算功能是一种基于抽象模型的方法 由 表示 数据 抽象 系统的状态描述和运算 操作 抽象 用前 后断言所组成 模型规范的形式定义 M 0 是M的状态集 含有不变式 0 是初始状态 是运算集合其实质是将软件系统视为基本状态的运算类型 12 04 2020 华东师大计算机科学技术系 48 1 系统状态规则 基本形式 类型ID 类型定义实体其中 ID是新定义的一个类型名实体是基本类型定义的一个新类型 基本类型 基本型 N R B 自然数 实数 Boolean 运算是常见的算术和逻辑运算 集合型 形式为 X setofQQ是已定义类型或基本类型 X是集合型ID运算有 并 交 差 元素个数 card 属于 子集 真子集 等 12 04 2020 华东师大计算机科学技术系 49 表型 有序集合 每个元素有确定位置 可重复出现 定义形式为 S seqofQS为新类型的ID Q为S的元素类型运算有 求头 hd 求尾 tl 长度 len 连接 conj 元素集 elem 索引集 inds 等 映射 有限 可列集的一个函数 通常以对偶集合形式表示 定义形式为 M MapofQM为新类型的ID Q为M的元素类型运算有 求定义域 dom 求值域 rng 限定定义域 定义域元素删除 等 12 04 2020 华东师大计算机科学技术系 50 复合型 P ComposePofe1 Q1 e2 Q2endP为新类型的ID ei Qi i 1 分别为P的分量名和分量类型运算 求复合类型值 mk P 改变分量值 求分量的值 12 04 2020 华东师大计算机科学技术系 51 例 一个教师职称提升系统的ADT定义 Studentdata ComposeStudentdataofName StringT score list SeqofChoiceendResearchdata ComposeResearchdataofName1 StringR Score List SeqofNendTeacher ComposeTeacherofT name StringT score RR score Rend 12 04 2020 华东师大计算机科学技术系 52 2 类型不变式规则 类型不变式是指对状态规则中规定的类型给出其应满足的性质 表示形式 设ST是在类型规范中所定义的一个类型ID Inv ST S P S 其中 P S 是一个一阶谓词公式 S ST 即ST中任一元素S应满足的条件例2 例1中ADTStudentdata描述了对一个教师的评价 Inv Studentdata mk Studentdata n t Studentdata n t Inv Choice t Choice lent 4 12 04 2020 华东师大计算机科学技术系 53 3 运算功能规则 运算功能规则VDM形式规范中的主要形式 其一般形式为 OP m1 Tm1 m2 Tm2 mn Tmn r1 Tr1 re TreextPV1 Tv1 PVk TvkpreC1 C1表示为 mj rk postC2 C2表示为 mj Vi rk Vi 其中 OP是运算名 mi是输入参量 ri是输出参量 ext表示Vi外部量 P wr rd 表示可读或可写 pre是前置谓词 post是后置谓词 注 Vi是执行OP前状态值 Vi是执行OP后状态值 12 04 2020 华东师大计算机科学技术系 54 例3 简单计算器规范 reg N 初始时外部变量reg 0LOAD i N extwrreg Npretruepostreg iSHOW r Nextrdreg Npretruepostr reg 12 04 2020 华东师大计算机科学技术系 55 ADD i N extwrreg Npretruepostreg reg iDIVIDE d N r Nextwrreg Npred 0postd r reg reg 0 reg d 12 04 2020 华东师大计算机科学技术系 56 为了描述方便 在前 后断言中可以出现的一些结构 let inQ含义 在let后定义一些临时变量 有效范围是Q ifethenPelseQ条件表达式 调用定义的函数 函数的规范为 显式定义 f p1 Tp1 p2 Tp2 pn Tpn Trf p1 pn functionbody 其中 pi是f的参量 类型为Tpi Tr为f的返回值 12 04 2020 华东师大计算机科学技术系 57 隐式定义 f p1 Tp1 p2 Tp2 pn Tpn r TrPre f Post 其中 Pre是f的前置谓词Post是f的后置谓词 12 04 2020 华东师大计算机科学技术系 58 例4 一个分类运算的VDM规范 Index entries seqofNSORT S Index entries r Index entriesextwroutput Index entriespres postelemr elemS is sorted r output outputconj r 其中 is sorted r 是一个函数 判断自然数表是否已经分类 12 04 2020 华东师大计算机科学技术系 59 三 VDM的程序正确性证明机制 关于函数的正确性证明f PTP Tr函数f满足规范 当且仅当 p Tp Pre f p f p Tr Post f p f p 关于运算的正确性证明设运算op的规范为 令 表示所有状态的集合 Tp Tv1 Tv2 Tr证明机制为 V pre OP V r Tr V post OP V V 其中 V exec OP r 即OP执行后的状态 12 04 2020 华东师大计算机科学技术系 60 四 一个VDM规范的例子 例5 用VDM为一个 教师职称提升系统 书写形式规范需求 该系统最终被定义为 Teacher Promotion 的运算 根据所要提升的名额 m 和全体教师的教学 科研评分表 选出总成绩最好的前m名教师 并输出教师的相关信息各运算及其函数的意义Get persons 取名额函数Teacher order 教师排序函数Score sum 教师积分计算函数Teacher list production 教师序列生成函数Teaching Research score 评分科研数据采集函数 12 04 2020 华东师大计算机科学技术系 61 类型说明 String seqofcharChoice seqofRTeacherSum ComposeTeacherSumofName2 StringTotal score REndTeacher list SeqofTeacherSumStudentdata list SeqofStudentdataReseachdata list SeqofResearchdata注 其他的说明已在例1中给出 12 04 2020 华东师大计算机科学技术系 62 类型不变式 Inv studentdata mk Studentdata n t Studentdata n t Inv Researchdata mk Researchdata n r Researchdata n r Inv choice t choice lent 4 12 04 2020 华东师大计算机科学技术系 63 函数及运算 Teacher Promotion tsl Studentdata list rsl Researchdata list m N P Teacher listextwroutput Teacher listPrelentsl lenrsl i indstsl name tsl i name1 rsl i 教学 科研二个表中名字相同 PostP Get Persons Teacher order Teacher list production ts1 rs1 m output outputconjP 12 04 2020 华东师大计算机科学技术系 64 从已排序的教师序列表td中取出总成绩最高的n位教师 从高到低次序放入tt表中 Get Persons td Teacher order list n N tt Teacher listPretd lentd n i j indstditotal score td i total score td j Postlentt n elemtt elemtd i j idnsttitotal score tt i total score tt j x elem