使用 Narval 对 Maude 理论进行符号分析
计算机科学中的逻辑
2019-07-29 v1 编程语言
摘要
具备符号推理能力的并发函数式语言（如 Maude）为编程和分析复杂、高度非确定性的软件系统提供了一种高层次、优雅且高效的方法。Maude 的符号能力基于重写理论中的等式合一与窄化，并为 Maude 提供了高级逻辑编程能力，例如模用户可定义等式理论的合一，以及重写理论中的符号可达性分析。由于这些近期开发的符号能力与经典 Maude 特性（如：(i) 具有 sorts（类型）、子类型和重载的丰富类型结构；(ii) 模如结合、交换和恒等等各种公理组合的等式重写；以及 (iii) 重写理论中的经典可达性分析）的协同作用，错综的计算问题可在 Maude 中有效且自然地解决。然而，所有这些特性的组合可能阻碍缺乏经验的开发者对 Maude 符号计算的理解。本文旨在描述如何通过提供一个称为 Narval 的复杂图形化工具来支持对 Maude 符号计算的细粒度检视，从而使 Maude 重写理论的编程与分析更为容易。本文正在考虑接受发表于 TPLP。
引用
@article{arxiv.1907.10919,
title = {Symbolic Analysis of Maude Theories with Narval},
author = {María Alpuente and Demis Ballis and Santiago Escobar and Julia Sapiña},
journal= {arXiv preprint arXiv:1907.10919},
year = {2019}
}
备注
Paper presented at the 35th International Conference on Logic Programming (ICLP 2019), Las Cruces, New Mexico, USA, 20-25 September 2019, 16 pages