Подвернулся примерчик из реальности.

Понадобилась процедурка:

## Код:
```
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].

Несколько угловато, но достаточно уверенно вывелось, вроде бы.

Интересно по общему инварианту порассуждать, но я не любитель это использовать при работе со строками... Видимо, опыта реально сложных доказательств мало.