局部转换

Maude 战略语言

重写逻辑是并发系统和逻辑规范的自然且富有表现力的框架。Maude 规范语言提供了这种形式主义的实现，允许执行、验证和分析所表示的系统。这些规范通过术语和方程式声明其对象，并提供重写规则来表示状态上可能不确定的局部转换。有时需要对这些规则进行受控应用，以减少非确定性，捕捉全局、面向目标或效率问题，或选择特定的执行进行分析。这就是我们所说的策略。为了表达它们，尊重关注点分离原则，提出并开发了 Maude 策略语言。策略语言的首次实现是在 Maude 本身中使用其反射功能完成的。经过充分的实验，又添加了一些功能，为了提高效率，策略语言已在 C++ 中实现为 Maude 系统的一个组成部分。本文介绍了 Maude 策略语言及其语义、实施决策以及来自各个领域的几个应用示例。