如何在达夫尼中定义这种常规语言？

Question

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

​

​

我怎么能用达夫尼来定义这样的语言呢？

Answer 1

以下是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>。因此，我们可以使用通常的内置方法来处理字符串上的序列。