【形式化方法:VDM++系列】1.前言

1.前言



今天开始上课学习软件需求分析与VDM++,经过一节课的学习,我又增长了见识。

软件需求工程在软件工程中处于十分核心的地位;需求分析的好坏直接决定软件工程的成败。这一点是我之前对需求工程的理解和认识,然而今天的学习又进一步扩展了我的认识。

2.需求分析的发展阶段



说起需求分析,首先想到的是用例,然后就是各种各样的用例图,功能描述;接下来我会想到产品原型,业务流程描述等等;然而这些其实都只是需求工程的某一阶段的一小部分。实际上,需求分析大致可划分为以下3个阶段:

(1)上世纪70年代兴起的结构化需求分析技术。以传统的结构化开发方法为代表,典型工具是数据流图,数据字典,业务流程图等。我在12年写毕业论文时曾用过此技术,拜读管理信息系统的教科书,仍然能看到这种技术;

(2)上世纪80年代-90年代兴起的面向对象的需求分析技术。以OOAD为核心,典型工具是UML,上面提到的用例图就属于此类。现在UML在业内仍然非常流行,是当代软件开发的主流技术。

(3)上世纪90年代至今兴起的形式化方法。为了克服自然语言和上述分析语言主观性强的弱点,真正实现需求的精确化定义,就必须依赖于数学,形式化方法遵循严格的数学和逻辑实现软件需求的精确定义,真正实现软件开发的精确化和自动化。势必将成为未来软件业界需求分析之主流。本系列所讲述的VDM正是由IBM提出的最早的一种形式化方法。

3.什么是VDM++



VDM是上世纪60-70年代由IBM开发的第一个形式化方法语言,VDM++是1993年对VDM的扩展。作为形式化方法,VDM++基于离散数学和一阶谓词逻辑,为软件需求定义、需求检查、回归测试、软件证明等提供了可能性。

由于其形式化的特点,使它本身也成为一种编程语言。描述精确,便于与C++、Java语言转化是它的显著优势。此外,VDM++不仅支持命令式风格的开发,同时也支持函数风格的开发。闲话少说,具体等到后面就看到啦。

4.系列简介



本系列基本上会与课程进度保持同步更新,大致上每周二更新一次。下次将图文并茂地展示VDM++开发环境VDMTools的安装和使用,敬请期待。

下一篇:【形式化方法:VDM++系列】2.VDMTools环境的搭建

时间: 2024-10-05 21:54:03

【形式化方法:VDM++系列】1.前言的相关文章

【形式化方法:VDM++系列】3.基于VDM++的图书管理系统需求定义

接前文:http://www.cnblogs.com/Kassadin/p/4091040.html 1.Before We Start: 在开始图书管理系统需求定义之前,需要先进行一些说明. 1.1 输入,输出定义 输入:用户需求文字说明 输出:基于VDM++的需求规格说明文档 任何问题只有明确它的输入和输出,才会有一个明确的预期,才有可能获得预期的结果.在这里明确问题的输入输出更加重要.特别需要指出的是,VDM++作为一种形式化方法语言,它主要用于需求分析,而不是代码实现.虽然它的产出是一段

【形式化方法:VDM++系列】2.VDMTools环境的搭建

接前文:http://www.cnblogs.com/Kassadin/p/3975853.html 上次讲了软件需求分析的演化过程,本次进入正题——VDM开发环境的搭建 (自从发现能打游戏以来,居然有将近1个月没有写博客了!真是越来越颓废了..) 其实VDM++已经学习了很多,近几天应该会逐渐更新. 1.VDM开发环境介绍 需要使用的环境主要有2个:(1)VDMTools (2)Overture Tool 官方网站:[VDMTools]http://www.vdmtools.jp/en/ [O

【形式化方法:VDM++系列】4.VDM实战1——铁路费用计算

又有将近2个月没更新博客了啊!winter holiday简直玩儿疯了的说!结果假期前学习的形式化方法已经忘了大半!面对期末作业,大脑一片空白.于是,赶快复习了一下之前学习的姿势! 这次的主要任务是完成一个费用计算程序. 1.问题 Make a model to calculate train fare from a station to another station by using functions and the following table. 使用函数计算两个车站之前的铁路费用.基

《软件工程 ——理论、方法与实践》知识概括第五章 软件工程中的形式化方法

第5章 软件工程中的形式化方法    从广义上讲,形式化方法(Formal Method)是指将离散数学的方法用于解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动.狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述.模型推理和验证的方法.将形式化方法运用于软件工程实践当中的只要目的是保证软件的正确性. 软件生命周期中的形式化转化策略:常用转化策略.直接转化策略和运用半形式化表示的中间转化策略. 进行模型化的过程中涉及到三种系统模型:现实世界.模型表示和计算机系统.

软件工程——理论、方法与实践 之 软件工程中的形式化方法

软件工程——理论.方法与实践 之 软件工程中的形式化方法 从广义上讲,形式化方法是指将离散数学的方法用于解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动.狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述.模型推理和验证的方法.形式化方法运用于软件工程实践当中主要目的是保证软件的正确性.软件开发实际上就是把现实世界的需求映射成软件额模型化过程.该过程包括:形式规约.形式证明我与检验.程序求精三方面的活动. 形式化规格说明是对软件系统对象,对象的操作方法,以及对象行为

软件工程中的形式化方法

软件的设计过程就是一个建立形式规约的过程.软件开发实际上就是把现实世界的需求映射成软件的模型化方法.软件规格说明是对软件系统对象,对象的操作方法,以及对象行为的描述.形式证明与验证技术主要包括模型检测和定理证明.程序求精是将自动推理和形式化方法相结合,从抽象的形式规约推演出具体的面向计算机的程序代码的全过程.模态(Modal)逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式.Kripke结构.1.一阶线性时态逻辑(FOLTL)是一阶谓词逻辑的扩展.2.计算树逻辑(CTL)是一种离散.分支时间.命题时态

.net工作准备系列--01前言

注:学习参考朱毅编著的进入IT名企必读200题. 内容重在自我学习与巩固. 前言: 章节划分 01应聘须知 02基础知识(重点) 03进阶知识 04重点应用(aspnet第一部分) 04重点应用(aspnet第二部分) 05.网络通讯 06.代码与算法 07 增强知识 01应聘须知-1.了解软件开发大环境.-2.准备简历:不宜超过一页,永远准备中文,模板.-3.渠道:3大网站,中华英才,前程无忧(51job最给力),智联招聘. -4.面试禁忌:不重考官,不注礼节,夸夸其谈,急问待遇. 总得来说就

软件工程中的形式化方法读后感

形式化方法是指将离散数学的方法用于解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动.狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述.模型推理和验证的方法.形式化方法运用于软件工程实践当中主要目的是保证软件的正确性.软件开发实际上就是把现实世界的需求映射成软件额模型化过程.该过程包括:形式规约.形式证明我与检验.程序求精三方面的活动. 其通过模态来对可能世界中的命题进行描述与演算,分为:Kripke结构..一阶线性时态逻辑..计算树逻辑.模型的三个主要组成部分是输

软件工程概论第五章--软件工程中的形式化方法

形式化方法指的是将离散数学的方法用于解决软件工程领域的问题,主要是建立精确的数学模型以及对模型的分析活动.在软件开发过程中运用数学模型有很多优点,例如能够解决规格说明的二义性,提高精确性,还能使软件相关问题的本质可以在不同抽象层次被展示出来.本章介绍形式化方法主要从形式化方法基本概念.时态逻辑.模型检验.Z语言.Petri网几个方面讲述. 形式化方法基本概念主要讲了形式规范.形式证明与验证.程序求精,形式规范说明是对软件系统对象,对象的操作方法,以及对象行为的描述.形式证明与验证主要包括模型检测