OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Четверг, 28 Март, 2024 17:09

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




Начать новую тему Ответить на тему  [ Сообщений: 62 ]  На страницу Пред.  1, 2, 3, 4
Автор Сообщение
СообщениеДобавлено: Среда, 07 Апрель, 2010 14:53 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
(* Предусловие: было чтение символа - Texts.Read(R, ch) (успешное или не успешное) *)
WHILE ~R.eot & (ch <= " ") DO
(* Инвариант: было чтение символа - Texts.Read(R, ch) (успешное или не успешное) *)
Texts.Read(R, ch)
END;
(* Постусловие: файл закончился или (ch > " ") *)

Правильно?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 07 Апрель, 2010 16:40 

Зарегистрирован: Пятница, 24 Апрель, 2009 16:28
Сообщения: 563
Откуда: Москва
Valery Solovey писал(а):
Ваш вариант
Извиняюсь, был занят.
Говорить тут о предусловии просто смешно. Мы можем, конечно, предположить, что перед циклом стоит Texts.Read(R, ch). Но с неменьшим успехом можем предположить, что файл вообще не открыт, а то, что содержится в сh не имеет никакого отношения к содержимому файла.

Предположим(!!), что имеем первый вариант.
Пусть pos0 - позиция в файле до первого чтения (которое, как предполагается стоит перед циклом).
Тогда инвариант цикла такой: кусок файла от pos0 до текущей позиции (pos), ислючая последний символ, состоит только из символов <= " ". В реальной жизни я бы этим ограничился, и не писал бы:
Aj: pos0<=j< pos: СимволФайла[j] <= " "

Постусловие, как всегда - это инвариант цикла & отрицание охраны: кусок файла от pos0 до достигнутой позиции, ислючая последний символ, состоит только из символов <= " ", а последний символ сh > " " или достигнут конец файла [и в BlackBox'е сh=0X].


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 62 ]  На страницу Пред.  1, 2, 3, 4

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


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

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


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

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