首页> 外文期刊>e-Informatica: software engineering journal >An introduction to Z and formal specifications
【24h】

An introduction to Z and formal specifications

机译:Z 和正式规范简介

获取原文
获取外文期刊封面目录资料

摘要

This paper provides an introduction to the description of information systems using formal, mathematical specifications written in the Z notation, and to the refinement of these specifications into rigorously checked designs. The first part introduces the idea of a formal specification using a simple example: that of a ‘birthday book’ in which people's birthdays can be recorded, and which is able to issue reminders on the appropriate day. The behaviour of this system for correct input is specified first; then the schema calculus is used to strengthen the specification into one requiring error reports for incorrect input. The second part of the paper introduces the idea of data refinement as the primary means of constructing designs which achieve a formal specification. Refinement is presented through the medium of two examples: the first is a direct implementation of the birthday book from part one; and the second is a simple checkpoint facility, which allows the current state of a database to be saved and later restored. A Pascal-like programming language is used to show the code for some of the operations in the examples.
机译:本文介绍了使用以 Z 符号编写的形式数学规范来描述信息系统,并将这些规范细化为经过严格检查的设计。第一部分通过一个简单的例子介绍了正式规范的概念:一个“生日书”,其中可以记录人们的生日,并且能够在适当的日子发出提醒。首先指定该系统正确输入的行为;然后,使用模式演算将规范加强为需要错误报告错误输入的规范。本文的第二部分介绍了数据细化的概念,作为构建实现正式规范的设计的主要手段。通过两个例子来呈现改进:第一个是直接实现第一部分的生日书;第二个是一个简单的检查点工具,它允许保存数据库的当前状态并在以后恢复。类似 Pascal 的编程语言用于显示示例中某些操作的代码。

著录项

获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号