浅析形式化描述方法的应用(2)

　　4Z语言与形式化应用实例
　　4.1Z语言
　　Z语言是由英国Oxford大学程序研究组设计的一种基于一阶谓词逻辑和集合论的形式规格说明语言，它采用了严格的数学理论，可以产生简明、精确、无歧义且可证明的规格说明。它支持形式化方法中的两种类型的抽象，并分别称之为表示抽象和操作抽象。在表示抽象中，数据从数据结构的表示细节抽象出来，使用关系、函数、集合、序列、包等抽象的数据类型，这些类型构成Z语言的类型系统；而操作抽象则描述了在数据抽象中所引入的数据上的抽象算法与操作。在Z语言中，表示抽象通过类型定义、全局变量或常量以及状态空间声明来进行表述；操作抽象通过函数和基于一阶谓词逻辑的操作来表述。
　　模式(schema)是Z语言的基本描述单位，它从软件系统的状态和状态之间的转化两个方面来进行软件系统的描述。模式分为状态模式和操作模式，状态模式定义了软件系统某一部分的状态空间及其约束特性，它通过相应抽象数据类型的变量以及在它们上面所定义的一些约束关系来进行描述；操作模式则描述系统某部分的行为特征，通过描述在操作之前的该部分的状态值与操作之后的该部分的状态值之间的关系，来定义该部分的某种操作的特性。
　　4.2问题简介
　　实现一个多用户共享使用一台计算机的机制，每一个用户必须登录并且必须要有一
个口令(password)。使用Z语言规格说明一个系统的登录与验证，必须保持注册过的用户(RegisteredUsers)和他们的口令信息，而且必须跟踪当前系统中登录的活动的用户。具体来说就是描述系统的状态、注册一个新的用户和口令、已经注册过的用户的登录、注销一个用户和它的口令，注意为该系统定义的许多操作都将检查给定的用户是否已经注册。
　　4.3给定类型
　　[User]：用户的集合
　　[Word]：用户口令的集合
　　[regd]：已经注册的用户的集合
　　[active]：已经登录的活动用户的集合

　　论文榜（www.zglwb.com），是一个专门从事期刊推广、投稿辅导的网站。
本站提供如何投稿辅导，寻求投稿辅导代理，快速投稿辅导，投稿辅导格式指导等解决方案：省级投稿辅导/国家级投稿辅导/核心期刊投稿辅导//职称投稿辅导。


期刊鉴别	论文检测	免费论文	特惠期刊	学术答疑	发表流程

搜索

浅析形式化描述方法的应用(2)