Towards an Evolutionary Formal Software-Development Using CASL
Towards an Evolutionary Formal Software-Development Using CASL
复制标题
使用 CASL 进行渐进式正式软件开发
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Axel Schairer
中科院分区：
文献类型：
--
作者：
S. Autexier;D. Hutter;H. Mantel;Axel Schairer
在实践中，软件的形式化开发是一个渐进的过程。失败的证明尝试引起规范的更改，并且此类更改使先前执行的证明无效。很明显，在这样的改变之后保留大部分的证明工作是非常可取的。在本文中，我们提出开发图作为模块化规范的通用框架，并定义了CASL规范到这些图的结构保留翻译。开发图的特点，这是一个渐进的过程中最重要的，是他们简化了对规范的变化，使其负面影响可以保持在最低限度的分析。
In practice, the formal development of software is an evolutionary process. Failed proof attempts give rise to changes in the specification and such changes invalidate proofs which have been previously performed. Clearly, it is very desirable to preserve much of the proof effort after such changes. In this paper, we propose development graphs as a general framework for modular specifications and define a structure preserving translation of CASL specifications into these graphs. The feature of development graphs, which is most important for an evolutionary process, is that they simplify the analysis of changes to the specification such that their negative effects can be kept to a minimum.