Предварительное условие Dafny для требования строки - это не только пробел

Я пытаюсь написать предварительное условие, чтобы строка содержала хотя бы один непробельный символ. Я написал следующее:

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
person Jones    schedule 21.08.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Кажется, проблема с триггером. Следующие работы. Но, возможно, кто-то, более знакомый с триггерами, может предложить лучшее решение.

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

Кстати: не уверен, что вы хотели, чтобы печатаемая строка была непустой. Мое текущее решение также требует этого.

person Matthias Schlaipfer    schedule 22.08.2019