Dafny 要求字符串的前提条件不仅是空格答案

【问题标题】：Dafny precondition to require a string is not only whitespaceDafny 要求字符串的前提条件不仅是空格
【发布时间】：2019-08-21 17:53:50
【问题描述】：

我正在尝试编写一个前提条件，要求一个字符串至少包含一个非空白字符。我写了以下内容：

predicate AllWhiteSpaceChars(s: string) {
    forall i :: 0 <= i < |s| ==> s[i] in {' ', '\n', /*'\f',*/ '\r', '\t'/*, '\v'*/}
}

但我无法让我的程序对其进行验证。以下失败：

method test1(s: string)
    requires !AllWhiteSpaceChars(s)
{
    print s;
}

method test2()
{
    test1("./foo");
}

我的谓词有什么问题，如何创建一个有效的前提条件？

【问题讨论】：

标签： dafny

【解决方案1】：

似乎是触发问题。以下作品。但也许更熟悉触发器的人可以提出更好的解决方案。

predicate HasNonWhiteSpace(s: string) {
    if s == []
    then false
    else s[0] !in {' ', '\n', /*'\f',*/ '\r', '\t'/*, '\v'*/} || HasNonWhiteSpace(s[1..])
}

method test1(s: string)
    requires HasNonWhiteSpace(s)
{
    print s;
}

method test2()
{
    test1("./foo");
    test1("\t\n ");
    test1("d d");
}

顺便说一句：不确定您是否打算要求打印的字符串为非空。我目前的解决方案也需要这样做。

【讨论】：