OO第三次单元总结

一、规格化设计发展历史

　　软件规格化方法，最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究，当时出现了各种语法分析程序自动生成器以及语法制导的编译方法，使编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。规格化设计的研究高潮始于20世纪60年代后期，针对当时所谓的“软件危机”，人们提出种种解决方法，如采用工程方法来组织、管理开发过程和通过钻研规律建立严密的理论以指导开发实践。

　　经过30多年的研究和应用，如今人们在规格化设计取得了大量、重要的成果，从早期最简单的一阶谓词演算到现在应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程、代数等众多规格形式化方法，它的发展趋势是逐渐融入设计开发的各个阶段，从需求分析、功能描述、算法设计、编程、测试直到维护。

　　规格化设计对代码的创作者和使用者都有重要的作用。对于编程者，规范的设计有助于架构的建立和调整，有助于完善修正细节，有助于未来的维护和扩展；对于使用者，规格化的呈现有助于理解剖析，避免不必要的误解和分歧，同时也利于高效的阅读和学习。

二、bug分析

　　

　　三次作业总共被报了四个规格bug，很遗憾的是其中有三个都是“忘记写了”……emm反思一下第十次可能和赶时间有关，但是第十一次在时间蛮充裕的情况下就真的是粗心没检查的锅。另外一个关于repOK的bug，我觉得测试者说的很有道理。因为在原来的repOK方法中，只要出现了对象型的变量我一律用“！=null”来处理，但是想想每个对象的类中也有它自己的repOK，理应传承下来，只有满足了所有的repOK才能说明科学合理性。

　　

　　虽然从表格上看，功能bug与规格bug确实没有重合的地方，但是这并不意味着两者就毫无关联。两次作业中功能出现的问题集中在input、run、randomdrive这些代码规模较大，逻辑较复杂的方法中，本身规格就很难概括，只能借助自然语言的帮助，加上关键步骤的布尔表达式来描述。由于规格无法涵盖细小逻辑，很难体现出错误疏漏，或者换一种说法，书写规格没有起到应有的作用，所以从报告bug的角度，就看不出联系了。

三、规格改进示例

  • 前置条件　　
/**
     * @REQUIRES:
     *         0<=index<=6399;
     * @MODIFIES:None;
     * @EFFECTS:
     *         normal_behavior:
     *            !(\exist int next;map.reachlist[index].contains(next)) ==> \result==index;
     *             在index的可达节点中随机选取一个两点之间边流量最小的节点next.
     *             \result==next;
     *         exception_behavior(Exception e):
     *             \result==index;
　　*/

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:
     *         0<=index<=6399;
     *         0<=oldindex<=6399;
     * @MODIFIES:None;
     * @EFFECTS:
     *         normal_behavior:
     *            !(\exist int next;map.reachlist[index].contains(next)) ==> \result==index;
     *             在index的可达节点中随机选取一个两点之间边流量最小的节点next.
     *             \result==next;
     *         exception_behavior(Exception e):
     *             \result==index;
　　*/

······································································································································

/**
     * @REQUIRES:
     *         0<=start<=6399;
     *         0<=end<=6399;
     *         0<=flow<=100;
     * @MODIFIES:
     *         \this.flow;
     * @EFFECTS:
     *         \this.flow[start][end]==flow;
     *         \this.flow[end][start]==flow;
　　*/

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:
     *         0<=start<=6399;
     *         0<=end<=6399;
     *         distance from start to end is 1.
     *         0<=flow<=100;
     * @MODIFIES:
     *         \this.flow;
     * @EFFECTS:
     *         \this.flow[start][end]==flow;
     *         \this.flow[end][start]==flow;
　　*/

······································································································································

/**
     * @REQUIRES:
     *         0<=index<=6399;
     *         0<=next<\this.reachlist[index].size();
     * @MODIFIES:None;
     * @EFFECTS:
     *         type==0 ==> \result==\this.reachlist[index].get(next);
     *         type==1 ==> \result==\this.initreachlist[index].get(next);
　　*/

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:
     *         0<=index<=6399;
     *         0<=next<\this.reachlist[index].size();
     *         type==0 || type==1;
     * @MODIFIES:None;
     * @EFFECTS:
     *         type==0 ==> \result==\this.reachlist[index].get(next);
     *         type==1 ==> \result==\this.initreachlist[index].get(next);
　　*/

······································································································································

/**
     * @REQUIRES:None;
     * @MODIFIES:None;
     * @EFFECTS:
     *         (r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==true;
     *         !(r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==false;
　　*/

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:
     *         r!=null;
     * @MODIFIES:None;
     * @EFFECTS:
     *         (r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==true;
     *         !(r‘s time,start_x,start_y,end_x,end_y are equal to this‘s) ==> \result==false;
　　*/

······································································································································

/**
     * @REQUIRES:None;
     * @MODIFIES:None;
     * @EFFECTS:
     *         \result==\this.inputs.get(i).start_x;
　　*/

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:
     *         0<=i<\this.inputs.size();
     * @MODIFIES:None;
     * @EFFECTS:
     *         \result==\this.inputs.get(i).start_x;
　　*/

······································································································································

  • 后置条件　　
/**
     * @REQUIRES:None;
     * @MODIFIES:
     *         \this.credit;
     * @EFFECTS:
     *         \this.credit==\this.credit+1;
　　*/

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:None;
     * @MODIFIES:
     *         \this.credit;
     * @EFFECTS:
     *         \this.credit==\old(\this.credit)+1;
     */

······································································································································

/**
     * @REQUIRES:
     *         req!=null;
     * @MODIFIES:None;
     * @EFFECTS:
     *         \result == request in inputs that equals req ;
     */

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:
     *         req!=null;
     * @MODIFIES:None;
     * @EFFECTS:
     *         \result == (\exist Request r; inputs.contains(r);r.equals(req));
     * @THREAD_REQUIRES:
     *         \locked(\this);
     * @THREAD_EFFECTS:
     *         \locked();
     */

······································································································································

/**
     * @REQUIRES:
     *         req!=null;
     * @MODIFIES:
     *         \this.inputs;
     * @EFFECTS:
     *         \this.inputs.contains(req) ;
     * @THREAD_REQUIRES:
     *         \locked(\this);
     * @THREAD_EFFECTS:
     *         \locked();
     */

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:
     *         req!=null;
     * @MODIFIES:
     *         \this.inputs;
     * @EFFECTS:
     *         \this.inputs.contains(req) && \this.inputs.size()=\old(\this.inputs).size()+1;
     * @THREAD_REQUIRES:
     *         \locked(\this);
     * @THREAD_EFFECTS:
     *         \locked();
     */

······································································································································

/**
     * @REQUIRES:None;
     * @MODIFIES:
     *         \this.reachlist;
     *         \this.initreachlist;
     * @EFFECTS:
     *         \this.reachlist == new Vector<Integer>();
     *         (\all Vector x;reachlist.contains(x);x!=null);
     *         \this.initreachlist == new Vector<Integer>();
     *         (\all Vector x;initreachlist.contains(x);x!=null);
     */

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:None;
     * @MODIFIES:
     *         \this.reachlist;
     *         \this.initreachlist;
     * @EFFECTS:
     *         \this.reachlist!=null;
     *         (\all Vector x;reachlist.contains(x);x!=null);
     *         \this.initreachlist!=null;
     *         (\all Vector x;initreachlist.contains(x);x!=null);
     */

······································································································································

/**
     * @REQUIRES:None;
     * @MODIFIES:None;
     * @EFFECTS:
     *         \result==queue!=null && inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null;
     */

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↓

/**
     * @REQUIRES:None;
     * @MODIFIES:None;
     * @EFFECTS:
     *         \result==queue!=null &&  inputs!=null && taxigui!=null && outFile!=null && taxis!=null && taxiInfo!=null && map!=null && queue.repOK() && inputs.repOK() && (\all Taxi t;taxis.contains(t);t.repOK()) && map.repOK();
     */

······································································································································

四、思路与体会

　　由于出租车的框架是在第七次作业时搭建好的，后面基本没有做出大的变动，所以大部分的规格是看着方法补充。前置条件就从传入的参数入手，基本类型需要判断在指定范围内，对象类型则要求不为空。中间条件抓住本类的类变量，逐一检查是否在此方法中被改变。后置条件比较复杂，需要兼顾条件判断、数组遍历、返回值、类变量前后改变等，如果是逻辑太多的方法就只能挑出关键步骤，借助自然语言描述。

　　不同的遭遇，不同的体会。在三次作业的互测过程中，测试者并没有死抠我的规格细节，扣的分主要是因为自己的粗心大意，所以在承受范围之内。至于书写规格的体会，由于没有做到像老师在课堂上说的 “先写规格后写代码”，整个过程可以说是“重温方法思路，再按规定格式翻译一遍”。虽然体验效果有些欠佳，但依然不能否认规格化设计的重要性。在真正的工程化编程中，规格的确有提高效率，减少出错的作用。同时我也认为，“规格化”不仅仅是贯彻体现在方法前的几行JSF注释中，更重要的是从构想到实施的过程，真正具有 “规格化”的思想。

原文地址：https://www.cnblogs.com/wjy21/p/9103151.html

时间： 2024-07-30 12:14:43

OO第三次单元总结的相关文章

规格化设计——OO第三单元总结

规格化设计--OO第三单元总结 一.JML语言理论基础.应用工具链 1.1 JML语言 ? JML(java modeling language)是一种描述代码行为的语言,包括前置条件.副作用等等.JML是一种行为接口规格语言 (Behavior Interface Speci?cation Language,BISL),基于Larch方法构建. ? 通过使用JML,我们可以忽略一个类.一个方法内部的具体实现,专注于描述方法的预期功能,从而把过程性的思考延迟到方法设计中,扩展了面向对象设计的原则

OO第三单元总结 JML

OO第三单元总结 JML JML语言的理论基础.应用工具链情况 JML是一种形式化的,面向JAVA的行为接口规格语言,它结合了Eiffel的契约方法和Larch方法,以及细化演算的一些元素,有着坚实的理论基础. JML最主要的语法有前置条件,后置条件,不变式,通过这些语法对输入和输出进行约束,也就是达成了一种契约.当模块实现后,只要输入输出满足这些约束表达式就满足了规格的要求.JML主要使用java的语法,除此之外还有自己的一些语法,比如/forall,/exist等等,来实现对输入输出的约束.

OO第三单元总结（规格设计）

OO第三单元总结 一.关于JML Java Modeling Language,即JML是一种规格化表示语言,主要用于对Java程序的各种方法功能的规范描述.这样做既可以给程序设计人员明确清晰的功能要求,又可以充分全面地验证已有的代码实现保证其满足规格描述的要求. 1.语法梳理 JML的语法清晰直观地描述了一个Java的各种特征.它的语法主要由以下三个部分组成. (1)表达式: 诸如 \result \old等有具体确定意义的固定关键词称为表达式.通过不同的搭配组合可以表示不同的含义,比如(\f

OO第三次课程总结分析

OO第三次课程总结分析 规格化设计发展历史 在网上找了好久也没找到合适的信息,稍稍参考了同学的博客.大致如下:最初的的软件并没有形式化方法,随着软件工程的兴起,为了便于工程间的协调管理,人们提出采用工程方法来组织.管理软件的开发过程并深入探讨程序和程序开发过程的规律,建立严密的理论.随着时代的发展,软件的复杂度日益加大,结构化程序设计的缺点日渐暴露出来,面向对象设计由此产生,规格化设计进一步发展,这一次的规格设计可以更好地区分置换条件,以适应面向对象设计.如今,规格化设计基本完善,软件可以轻松实

OO第三单元总结

JML语言理论基础 Java建模语言(Java Modeling Language,JML)是一种进行详细设计的符号语言,他鼓励你用一种全新的方式来看待Java的类和方法.JML是一种行为接口规格语言 (Behavior Interface Speci?cation Language,BISL),基于Larch方法构建.BISL提供了对方法和类型的规格定义手段.所谓接口即一个方法或类型外部可见的内容.通过在Java代码中增加了一些符号,这些符号用来标识一个方法是干什么的,却并不关心它的实现.使用

OO第三单元总结-规格化设计

OO规格化编程体验小结 1. JML语言的理论基础.应用工具链情况 JML 理论基础: JML建立契约式编程的基础上,是一种实现契约式编程的规格化语言.顾名思义,契约式编程,是供求双方建立在一定的契约上进行软件的开发和应用.类似于在共同完成这一个工程的时候我们对于每个方法都以一个供求双方都统一并且详细知晓的合同,在这个合同上,供应方要不多不少完成合同上的所有要求,需求方的可提出的需求范围只限于合同上的明确条文.这样同时明确了双方的权利和义务.而产生契约式编程的背景是很多工程的开发过程权责混乱,导

2019年北航OO第三单元（JML规格任务）总结

一.JML简介 1.1 JML与契约式设计 说起JML,就不得不提到契约式设计(Design by Contract).这种设计模式的始祖是1986年的Eiffel语言.它是一种限定了软件中每个元素所必需的责任与义务的开发模式,程序设计中的每个元素都需要用规范的语言精准地限定其前置条件(Preconditions).后置条件(Postconditions)和不变式(Invariants).通过这三项限定,我们可以清晰地获得对一个函数功能的刻画,从而达成设计与实现的分离,便于优化.测试和生成文档.

OO第三单元总结--根据JML写代码

一. JML语言 1. 理论基础 首先,JML不是JAVA的一部分,它是一群研究者为JAVA设计的扩展部分,但还没有得到官方的支持.因此,JAVA编译器并不支持JML,所以要想JML起作用,只能采用类似openJML这样的第三方来编译,将JML 规格编译为运行时检查的语句,即RAC code(runtime assertion checking).如果代码实现与其JML规格不一致,将引发运行时JML exception. JML遵从契约式设计范式(DBC),Design by contract是

OO第三单元单元总结

目录 JML知识梳理 部署JMLUnitNG/JMLUnit 按照作业梳理自己的架构设计,并特别分析迭代中对架构的重构 按照作业分析代码实现的bug和修复情况 阐述对规格撰写和理解上的心得体会 JML知识梳理 JML理论基础 关于JML的相关介绍其实课程给出的指导书就已经足够使用了,由于指导书上都有相关知识的梳理,所以这里不花费大量篇幅去书写这部分内容,只是简单提及一些东西.首先是什么是JML,课程进行,其实阅读简单的JML已经没有多大障碍了,但是对于JML的定义这种概念已经忘记的差不多了.JM