OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Воскресенье, 26 Октябрь, 2025 08:28

Сообщения без ответов | Активные темы


Список форумов » Проект Информатика-21 » Программирование "под доказательство"

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




Начать новую тему Ответить на тему  Страница 1 из 1
  [ Сообщений: 3 ] 
  Версия для печати Пред. тема | След. тема 
Автор Сообщение
Rifat
 Заголовок сообщения: Аксиоматизация цикла LOOP
СообщениеДобавлено: Понедельник, 19 Апрель, 2010 10:03 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 989
Откуда: Казань
В книге Вирта "Систематическое программирование" правила верификации для циклических конструкций записываются следующим образом:

Посылка: {P and B} S {P}
Следствие: {P} while B do S {P and not B}

Посылка: {P} S {Q}
{Q and not B} S {Q}
Следствие: {P} repeat S until B {Q}

Можно ли аналогичные правила верификации записать для цикла LOOP из языка Oberon?
Вернуться к началу
 Профиль  
 
Валерий Лаптев
 Заголовок сообщения: Re: Аксиоматизация цикла LOOP
СообщениеДобавлено: Понедельник, 19 Апрель, 2010 10:58 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 3261
Откуда: Астрахань
Rifat писал(а):
В книге Вирта "Систематическое программирование" правила верификации для циклических конструкций записываются следующим образом:

Посылка: {P and B} S {P}
Следствие: {P} while B do S {P and not B}

Посылка: {P} S {Q}
{Q and not B} S {Q}
Следствие: {P} repeat S until B {Q}

Можно ли аналогичные правила верификации записать для цикла LOOP из языка Oberon?

В общем виде, как представляется, нельзя. Поскольку нет явного условия окончания цикла.
Вернуться к началу
 Профиль  
 
Владислав Жаринов
 Заголовок сообщения: Re: Аксиоматизация цикла LOOP
СообщениеДобавлено: Вторник, 20 Апрель, 2010 05:18 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2045
Rifat писал(а):
В книге Вирта "Систематическое программирование" правила верификации для циклических конструкций записываются следующим образом:

Посылка: {P and B} S {P}
Следствие: {P} while B do S {P and not B}

Посылка: {P} S {Q}
{Q and not B} S {Q}
Следствие: {P} repeat S until B {Q}

Можно ли аналогичные правила верификации записать для цикла LOOP из языка Oberon?


Ежели разве что рассматривать LOOP как обычный цикл с "риторическим" вопросом условия... :wink:
Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  Страница 1 из 1
  [ Сообщений: 3 ] 

Список форумов » Проект Информатика-21 » Программирование "под доказательство"

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


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

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

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

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