How to define this regular language in Dafny?

Question

There is a question in the book "Automata Theory and Applications" that talks about the language

How can I define such a language in Dafny?

Answer 1

Here is a straightforward transcription of the definition of L into Dafny.

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']
}

Note that in Dafny, the type string is defined to be seq<char>. So we can use the usual built-in methods of manipulating sequences on strings.