如何在Dafny中定义这种常规语言？

问题描述

“自动机理论与应用”一书中有一个关于语言的问题

如何在Dafny中定义这种语言？

解决方法

这是L的定义到达夫尼的直接表达。

predicate ContainsOnlyAsAndBs(s: string)
{
  forall c | c in s :: c == 'a' || c == 'b'
}

predicate L(w: string)
  requires ContainsOnlyAsAndBs(w)
{
  exists x | ContainsOnlyAsAndBs(x) && x != [] :: w == ['a'] + x + ['a']
}

请注意，在Dafny中，类型string被定义为seq<char>。因此，我们可以使用通常的内置方法来处理字符串上的序列。