如何将正则表达式集成到合金分析仪中?

问题描述 投票:0回答:1

我目前正在使用 Alloy 为容器编排器建模。事实证明,我需要写的很多事实都涉及到正则表达式(regex)。由于 Alloy 默认不支持正则表达式,我想知道如何添加此支持。 有谁知道要遵循的步骤?例如要修改哪部分代码?

我查看了文档和 Java 存储库,但无法确定要修改的代码部分。

alloy formal-verification
1个回答
0
投票

我是老一代 Alloy 用户,当时 Alloy 曾经是一种非常简单但富有表现力的半正式建模语言。 我知道自 4.2 版本以来,对该语言进行了很多修改,可能是为了扩展该语言的可用性而进一步牺牲了该语言原有的优雅。

话虽这么说,我确实觉得 Alloy 本质上不适合推理正则表达式。更广泛地说,它不适合推理字符串运算、算术或任何其他具有潜在无限值的非抽象域。

当然,您可以制作一个在某种程度上处理这些事情的玩具示例,但任何真正有价值的用例都会因 Alloy 的可扩展性问题而受到损害。

事实上,进行详尽的正则表达式验证将需要您确实拥有非常大的字符串池可供使用,这本身就违背了小范围假设。

它完全违背了 Alloy 过去所代表的理念,即对复杂系统进行抽象以揭示最微妙的缺陷。

再说一遍,我是恐龙。很可能我都错了,Alloy 7 也可以做咖啡。

© www.soinside.com 2019 - 2024. All rights reserved.