期刊文献+
共找到11篇文章
< 1 >
每页显示 20 50 100
Refinement and Transformation from Z Specification to C+ +
1
作者 Zhang Xiaoying(张晓莺) +1 位作者 Chen Jiaxun(陈家训) 《Journal of Donghua University(English Edition)》 EI CAS 2001年第4期97-102,共6页
As a kind of formal specification language, Z has gained a position in the field of software development, but there is still no standard way of transforming Z specification into executable code that is promising in in... As a kind of formal specification language, Z has gained a position in the field of software development, but there is still no standard way of transforming Z specification into executable code that is promising in increasing the quality, reusability and maintainability of software.With the automatic programming model of software engineering, through the analysis for Z specification language, a feasible semi-automatic way of refinement and transformation is proposed, and the correctness of the procedure is also discussed. 展开更多
关键词 z specification refiinement transformation C + + Class template FUNCTION TEMPLATE
下载PDF
一种基于Z和精化演算的形式化开发方法 被引量:2
2
作者 阮幼林 李传湘 《小型微型计算机系统》 CSCD 北大核心 2001年第5期592-595,共4页
通过分析 Z和精化演算各自的特点 ,本文提出了一种使两者无缝集成的形式化开发方法 .该方法利用 Z良好的描述特性和扩充的类机制 ,将系统规约直接定义成精化演算中的抽象程序 ,然后用精化规则对抽象程序逐步精化 ,直到可执行程序 .
关键词 精化演算 软件开发 形式化开发方法 z语言 软件工程
下载PDF
Z规格说明构造方法 被引量:1
3
作者 刘玲 缪淮扣 《计算机工程》 CAS CSCD 北大核心 2000年第2期39-41,共3页
比较完整地描述了Z规格说明的结构和写规格说明的步骤,并通过一个所设计的Z规格说明的实例演示了用Z编写规格说明的过程。
关键词 规格说明 z模式 初始化定理证明 前置条件简化
下载PDF
Z规格说明求精的正确性判定 被引量:1
4
作者 李刚 朱关铭 童頫 《计算机科学》 CSCD 北大核心 1997年第1期68-72,共5页
软件求精是自动推理和形式化开发方法相结合而形成的一门新技术,它研究从抽象的形式格说明推演出具体的面向计算机的程序代码的全过程.其基本思想是用·个抽象程度低。
关键词 z规格说明 软件开发
下载PDF
现有Z的工具的比较
5
作者 庞军 王云峰 郑国梁 《计算机科学》 CSCD 北大核心 1999年第10期78-80,共3页
一引言软件开发过程需要大量的工具支撑,如编辑工具,编译工具,调试工具等。这些工具的使用不仅方便了软件的开发,而且合适的工具保证了软件开发的质量,它将使软件开发人员的注意力集中到设计工作本身,而不耗费在设计的相关工作上。形式... 一引言软件开发过程需要大量的工具支撑,如编辑工具,编译工具,调试工具等。这些工具的使用不仅方便了软件的开发,而且合适的工具保证了软件开发的质量,它将使软件开发人员的注意力集中到设计工作本身,而不耗费在设计的相关工作上。形式化方法为计算机系统的规约、实现和验证提供了合理的数学基础,首先对系统进行独立于实现的、基于一定形式化语义的抽象描述。 展开更多
关键词 软件开发 z工具 面向对象 计算机
下载PDF
一种从Z到精化演算的软件开发方法 被引量:3
6
作者 查鸣 王云峰 郑国梁 《计算机科学》 CSCD 北大核心 2000年第2期14-17,68,共5页
一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于... 一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于形式规约语言。通过语法和语义有严格数学定义的形式规约语言对系统及其各方面性能的描述,产生系统的形式规约,可以帮助开发者获得对所描述系统的深刻理解。 展开更多
关键词 软件开发方法 z语言 精化演算 形式化描述语言
下载PDF
一个Z的证明责任产生器 被引量:2
7
作者 沈毅 缪淮扣 +1 位作者 文志诚 陈怡海 《上海大学学报(自然科学版)》 CAS CSCD 北大核心 2005年第5期495-499,共5页
在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求.证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程.完成证明... 在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求.证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程.完成证明责任产生器的工作难点就在于如何生成证明责任,本文对这一工作进行了详细的介绍. 展开更多
关键词 形式规格说明 验证 z 证明责任 前置条件 不变式
下载PDF
基于Real-Time Object-Z语言的实时系统形式化描述 被引量:2
8
作者 魏艳铭 张广泉 《重庆师范大学学报(自然科学版)》 CAS 2007年第4期41-44,53,共5页
实时系统是一类需要考虑时间约束条件的反应系统,确保实时系统安全性和可靠性是至关重要的。形式化方法是建立在严密数学基础之上的开发方法,采用形式化方法对实时系统进行描述与验证,可以借助严密的数学证明提高实时系统的安全性和可... 实时系统是一类需要考虑时间约束条件的反应系统,确保实时系统安全性和可靠性是至关重要的。形式化方法是建立在严密数学基础之上的开发方法,采用形式化方法对实时系统进行描述与验证,可以借助严密的数学证明提高实时系统的安全性和可靠性。本文讨论Object-Z的一种实时扩展语言Real-Time Object-Z,它可以对实时系统进行形式化描述;文中以室温控制系统为例,详细说明了Real-Time Object-Z语言在实时系统形式化描述中的应用方法。 展开更多
关键词 实时系统 OBJECT-z REAL-TIME OBJECT-z 实时精化演算 形式化描述
下载PDF
Syntax-Tree Regular Expression Based DFA FormalConstruction
9
作者 Nazir Ahmad Zafar Fawaz Alsaade 《Intelligent Information Management》 2012年第4期138-146,共9页
Compiler is a program whose functionality is to translate a computer program written in source language into an equivalent machine code. Compiler construction is an advanced research area because of its size and compl... Compiler is a program whose functionality is to translate a computer program written in source language into an equivalent machine code. Compiler construction is an advanced research area because of its size and complexity. The source codes are in higher level languages which are usually complex and, consequently, increase the level of abstraction. Due to such reasons, design and construction of error free compiler is a challenge of the twenty first century. Verification of a source program does not guarantee about correctness of code generated because the bugs in compiler may lead to an incorrect target program. Therefore, verification of compiler is more important than verifying the source programs. Lexical analyzer is a main phase of compiler used for scanning input and grouping into sequence of tokens. In this paper, formal construction of deterministic finite automata (DFA) based on regular expression is presented as a part of lexical analyzer. At first, syntax tree is described based on the augmented regular expression. Then formal description of important operators, checking nullability and computing first and last positions of internal nodes of the tree is described. In next, the transition diagram is described from the follow positions and converted into deterministic finite automata by defining a relationship among syntax tree, transition diagram and DFA. Formal specification of the procedure is described using Z notation and model analysis is provided using Z/Eves toolset. 展开更多
关键词 AUTOMATA Theory COMPILER Verification LEXICAL ANALYzER Automated tools z specification
下载PDF
两次数据精化的形式化软件开发方法 被引量:3
10
作者 邢小英 王维维 《计算机工程》 CAS CSCD 北大核心 2006年第1期102-104,共3页
提出了一种从数据精化、过程精化、再数据精化的两次数据精化的形式化软件开发方法。传统Z规约数据精化很复杂。该文先采用过程写出初始规范,对模式进行第一次数据精化,然后把它转换为Z模式,再进行过程精化。最后再数据精化到目标代码... 提出了一种从数据精化、过程精化、再数据精化的两次数据精化的形式化软件开发方法。传统Z规约数据精化很复杂。该文先采用过程写出初始规范,对模式进行第一次数据精化,然后把它转换为Z模式,再进行过程精化。最后再数据精化到目标代码。以常见动态Web网页脚本语言PHP为例,阐述了该方法。并为此写了一套从过程到Z模式的转化规则,以及精化到PHP的精化规则。 展开更多
关键词 过程 z语言 规范 精化演算 PHP
下载PDF
Reusing Test Cases Based on the Function Point
11
作者 张娟 童维勤 +2 位作者 蔡立志 黄文彬 HWANG Jenq-Neng 《Journal of Donghua University(English Edition)》 EI CAS 2014年第4期441-446,共6页
Reusing test cases from existing test case library is quite common in the software testing field. Testing practice tells us that there is a strong relationship between the granularity of a function unit under testing ... Reusing test cases from existing test case library is quite common in the software testing field. Testing practice tells us that there is a strong relationship between the granularity of a function unit under testing and that of the test case. A function unit with small granularity usually results in the test cases with the same small granularity. Therefore a test case defined as the function point,i. e.,the smallest size function unit,was provided for the first time.Though test cases with smaller granularity usually have better reusability,the cost of accurately reusing and integrating such test cases is also higher. In order to balance the test case reusability and the cost of test case reuse,a novel test case reuse model based on the function point was proposed in this paper. In this model,a reusable test case for specification-based testing was defined and some reuse strategies and three formal reuse methods were given. Finally,the complete automatic software process was realized by a reusing generation tool. The new method has improved reuse accuracy,while greatly enhances the software productivity. 展开更多
关键词 function point function unit test case test case suite REUSE RG tool z specification language
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部