RIA: Design Strategies For Algebraic Specifications

抽象数据类型的代数规范中缺乏某些属性（如完整性或终止）通常是设计错误的结果，并且可能对依赖于规范的流程（如代码实现或验证）产生重大后果。为了缓解这个问题，已经投入了大量的努力来更好地理解这些属性，并实现可以保证某些属性存在或检测它们不存在的工具。到目前为止，还没有发表关于防止而不是纠正设计错误的工作。提出了两种策略，在合理的一般假设下，可以用来产生完整的、简洁的、线性的和终止的规范。这些策略的适用程度尚不清楚。如果这些策略所需要的一些簿记的困难是机械化的，那么这些策略使用起来就很简单。一个原型实现显著地提高了设计规范的生产率和规范的质量。该项目有以下目标：探索这些策略的适用性范围。在某些情况下，没有实现一个属性，但仍然不清楚是属性太强还是策略太弱。此外，在某些情况下，一种策略并不是最方便的。调查是否存在其他策略。示例表明，这些策略对于实现理想的特性是足够的，但不是必需的。可能存在具有类似目标和性能的其他策略。实现可用的策略。通过使用它们来设计一套基本的通用规范，评估和改进它们的有效性。

The lack of certain properties, such as completeness or termination, in an algebraic specification of abstract data types is often the result of design errors and can have significant consequences on processes, such as code implementation or verification, which rely on the specification. To alleviate the problem substantial efforts have been devoted to understand better these properties and to implement tools which may guarantee the presence of some properties or detect their absence. To date, no work has yet been published for preventing design errors rather than correcting them. Two strageties are suggested which, under reasonably general assumptions, can be used to produce specifications which are complete, parsimonious, linear, and terminating. The extent to which these strategies are applicable is not yet known. These strategies are simple to use if the difficulties resulting from some book-keeping they require is mechanized. A prototipical implementation improves significantly the productivity of designing specifications and the specification quality. The project has the following goals: Explore the range of applicability of these strategies. In some situations, one property is not achieved, but it is still unclear whether the property is too strong or the strategy too weak. Also, one strategy is not the most convenient one in some situations. Investigate the existence of other strategies. Examples show that these strategies are sufficient for achieving desirable properties, but are not necessary. Other strategies with similar goals and performances may exist. Implement the available stategies. Evaluate and improve their effectiveness through their use for designing a set of basic, general specifications.