CODEWITHSUNDEEP
dafny
Jones
Jones

Reputation: 1214

Dafny precondition to require a string is not only whitespace

I am trying to write a precondition to require a string to contain at least one non-whitespace character. I wrote the following:

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

But I can't get my program to verify with it. The following fails:

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

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

What is wrong with my predicate, and how can I create a working precondition?

Upvotes: 0

Views: 207

Answers (1)

Matthias Schlaipfer
Matthias Schlaipfer

Reputation: 520

Seems to be a trigger issue. The following works. But maybe someone more familiar with triggers can suggest a better fix.

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");
}

BTW: not sure if you meant to require the string being printed to be non-empty. My current solution also requires that.

Upvotes: 1

Related Questions