OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Среда, 11 Декабрь, 2019 22:59

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 10 ] 
Автор Сообщение
 Заголовок сообщения: Пример: сравнение URI с образцом
СообщениеДобавлено: Пятница, 22 Январь, 2010 01:39 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9164
Откуда: Россия, Орёл
Подвернулся примерчик из реальности.

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

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 02:17 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9164
Откуда: Россия, Орёл
Что-то намудрил ночью...

Проще можно - ищем первое несовпадение или конец URI, а потом разбираемся с этим местом и его соответствием шаблону.

Код:
PROCEDURE CompareUri (IN pattern, uri: ARRAY OF SHORTCHAR; OUT ok: BOOLEAN; OUT generic: BOOLEAN);
   VAR eqLen: INTEGER;
BEGIN
   eqLen := 0;
   WHILE (uri[eqLen] # 0X) & (pattern[eqLen] = uri[eqLen]) DO
      INC(eqLen)
   END;
   ok := (uri[eqLen] = 0X) & (pattern[eqLen] = 0X) OR (pattern[eqLen] = "*") & (pattern[eqLen+1] = 0X)
END CompareUri;


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 10:04 

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 531
Откуда: Москва
Илья Ермаков писал(а):
Подвернулся примерчик из реальности.
Несколько соображений.
1. Если у pattern "*" в конце, то зачем проверять, идет ли дальше 0Х? Это и есть в конце. Или что-то опущено в условиях.
2. Вот это все
Илья Ермаков писал(а):
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) )
не нужно, его сложность превышает сложность программы. Допустить здесь ошибку часто легче, чем в самой программе. В реальной жизни это все мгновенно отмирает (if any). Честно, говоря мне даже влом в это вникать.
3. А вот инвариант, наоборот, очень важен. Он очень простой: куски сравниваемых строк от начала до текущей позиции (< i) совпадают. Даже не требуется более строгая запись.
4. Слова "линейный поиск" поиск лишние, забудьте про них. Гораздо важнее пункт 3.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 10:30 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9164
Откуда: Россия, Орёл
"Линейный поиск" я привык использовать в смысле отображения в программе квантора E.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 11:57 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9164
Откуда: Россия, Орёл
И вообще, что такого "эзотеричного" в ЛП?

Есть циклы на последовательностях, которые не изменяют в теле ничего, кроме одного "бегунка" (вообще отсутствует фаза нарушения инварианта). А инвариант вообще тривиален - всё пройденные элементы соответствуют условию цикла (см. у Вас же: "Он очень простой: куски сравниваемых строк от начала до текущей позиции (< i) совпадают" - такой он и всюду).

"Поисковость" в том, что окончание может быть по нескольким ситуациям, которые нужно распознавать после цикла; таким образом, постусловие состоит из двух или более дизъюнктов (а постусловие - обратных конъюнктов).

Паттерн ЛП навязывает следующую дисциплину проектирования:
1. Сначала выделяем классы состояний, которые нужно распознавать после цикла. Формулируем постусловие как дизъюнктивную форму, 1-к-1 соответствующую этим классам. Уже внутри каждого дизъюнкта формулируем сколь угодно сложное условие на каждый отдельный класс.
2. Упорядочиваем дизъюнкты по области определения (используем сокращённую семантики вычислений cor-cand в качестве охраны правых дизъюнктов).
3. Отображаем их в условие цикла точным обращением в конъюнктивную форму. Если условия внутри каждого конъюнкта сложны, то вносить отрицание внутрь конъюнкта нежелательно, т.к. семантику задачи выражает именно изначальное условие, его инверсия непонятна при чтении программы.
Кроме того, вот это 1-к-1 соответствие (без упрощения выражений) важно потому, что проверки каждой ситуации выполняются после цикла. Т.е. лучше иметь полное совпадение и в условии цикла, и в IF-е после цикла.

Никакой конкуренции с методом инварианта тут нет. Если шаг по последовательности в цикле сложный (а не просто "бегунок"), то выводим его строго по инварианту.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 13:04 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8215
Откуда: Троицк, Москва
Peter Almazov писал(а):
... Честно, говоря мне даже влом в это вникать.

... инвариант ... очень простой: куски сравниваемых строк от начала до текущей позиции (< i) совпадают. Даже не требуется более строгая запись. ...
Всё правильно.

Но чел должен четко понимать, как словесные формулировки отображаются в формулы.
Для достижения такого состояния нужен тренаж.
Просто некоторым нужно, чтобы их заставили его проделать, а Илья Евгеньевич -- сознательный человек 8)


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 13:11 

Зарегистрирован: Понедельник, 30 Июль, 2007 10:53
Сообщения: 1538
Откуда: Беларусь, Минск
Илья Ермаков писал(а):
Никакой конкуренции с методом инварианта тут нет.
А точнее, это и есть "метод инварианта".


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 14:03 

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 531
Откуда: Москва
Info21 писал(а):
Peter Almazov писал(а):
Но чел должен четко понимать, как словесные формулировки отображаются в формулы.
Для достижения такого состояния нужен тренаж.
Просто некоторым нужно, чтобы их заставили его проделать, а Илья Евгеньевич -- сознательный человек 8)
Я бы охотно с этим согласился, если бы Илья действительно расписал инвариант. Но тот мусор не имеет к инварианту никакого отношения.
Вот инвариант цикла:
A j: 0<=j<i: uri[j] = pattern[j]


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 14:18 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9164
Откуда: Россия, Орёл
Так извиняйте, прежде чем писать что-то по самому циклу (инвариант), надо же спецификацию сформулировать (что вычисляем). Что и попытался сделать, для себя.

Вариант-то рабочий получился быстро (там задачка была срочная), кстати, и надёжно. Правда, когда через два часа подумал, как надо проще, заменять в работающей службе не стал :)


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Январь, 2010 14:37 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8215
Откуда: Троицк, Москва
Peter Almazov писал(а):
Вот инвариант цикла:
A j: 0<=j<i: uri[j] = pattern[j]
Вот видите, какое хорошее групповое упражнение получилось 8)


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 10 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 0


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
cron
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2019, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB