Подвернулся примерчик из реальности.
Понадобилась процедурка:
Код:
PROCEDURE CompareUri (IN pattern, uri: ARRAY OF SHORTCHAR; OUT ok: BOOLEAN; OUT generic: BOOLEAN);
Должна сравнить uri на соответствие pattern-у.
pattern - либо точный URI (тогда требуется точное равенство), либо начальная часть и * в конце.
Постусловие:
не соответствует: (ok = FALSE) & (generic = FALSE)
соответствует: (ok = TRUE) & (generic = шаблон_имеет_неточный_вид)
Алгоритм на узком месте, так что должен быть однопроходным и максимально быстрым (затея искать хвост только затем, чтобы там сначала * проверить, не катит).
Формулируем условие для ok.
ok = ( !E i: (i < LEN(uri$)) & (i < LenOf(pattern)) : uri[i] # pattern[i] )
& ( (LenOf(pattern) = LEN(uri$)) OR (pattern[LEN(uri$)] = '*') & (pattern[LEN(uri$)+1] = 0X) )
(где под LenOf понимаем значащую часть шаблона)
Т.е. ok, если не существует несовпадающих символов в общих частях шаблона-URI, и шаблон либо равен по длине URI, либо неточен с этого места.
Видим !E или !E, ясно, что можно строить линейный поиск, для выяснения первой части условия.
Условие окончания просмотра: или закончился uri, или найден нечёткий хвост шаблона.
Условие поиска: обнаружен несовпадающий символ.
В конце после цикла проверяется не только условие поиска, но ещё и, если шаблон не общий, его совпадение по длине с URI (что у него тоже 0X) - т.е. второй конъюнкт из спецификации выше.
Код:
PROCEDURE CompareUri (IN pattern, uri: ARRAY OF SHORTCHAR; OUT ok: BOOLEAN; OUT generic: BOOLEAN);
VAR i: INTEGER;
BEGIN
i := 0;
WHILE ~( (* end of sequence: *) (uri[i] = 0X) OR (pattern[i] = "*") & (pattern[i+1] = 0X) ) &
~((* linear search of #: *) uri[i] # pattern[i] ) DO
INC(i)
END;
generic := (pattern[i] = "*") & (pattern[i+1] = 0X);
ok := (uri[i] = 0X) & (pattern[i] = 0X) OR generic
END CompareUri;
Тонкое место - в условии цикла не фигурирует pattern[i] = 0X, но это попадает под uri[i] # pattern[i].
Несколько угловато, но достаточно уверенно вывелось, вроде бы.
Интересно по общему инварианту порассуждать, но я не любитель это использовать при работе со строками... Видимо, опыта реально сложных доказательств мало.