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.