OberonCore
https://forum.oberoncore.ru/

Этюд из книги "Построение компиляторов"
https://forum.oberoncore.ru/viewtopic.php?f=82&t=2233		 Страница 4 из 4
Автор:  Rifat [ Среда, 07 Апрель, 2010 14:53 ]
Заголовок сообщения:  Re: Этюд из книги "Построение компиляторов"
(* Предусловие: было чтение символа - Texts.Read(R, ch) (успешное или не успешное) *)
WHILE ~R.eot & (ch <= " ") DO
(* Инвариант: было чтение символа - Texts.Read(R, ch) (успешное или не успешное) *)
Texts.Read(R, ch)
END;
(* Постусловие: файл закончился или (ch > " ") *)

Правильно?
Автор:  Peter Almazov [ Среда, 07 Апрель, 2010 16:40 ]
Заголовок сообщения:  Re: Этюд из книги "Построение компиляторов"
Valery Solovey писал(а):
Ваш вариант
Извиняюсь, был занят.
Говорить тут о предусловии просто смешно. Мы можем, конечно, предположить, что перед циклом стоит Texts.Read(R, ch). Но с неменьшим успехом можем предположить, что файл вообще не открыт, а то, что содержится в сh не имеет никакого отношения к содержимому файла.

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

Постусловие, как всегда - это инвариант цикла & отрицание охраны: кусок файла от pos0 до достигнутой позиции, ислючая последний символ, состоит только из символов <= " ", а последний символ сh > " " или достигнут конец файла [и в BlackBox'е сh=0X].
Страница 4 из 4 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/