OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Вторник, 19 Март, 2024 07:08

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




Начать новую тему Ответить на тему  [ Сообщений: 26 ]  На страницу 1, 2  След.
Автор Сообщение
СообщениеДобавлено: Четверг, 08 Март, 2018 20:16 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Программирования под доказательство - это составление программы и её составных частей таким образом, чтобы её корректность по отношению к спецификации можно было доказать.

Это единственный подход, позволяющий доказывать корректность программ, потому что невозможно создать метод для доказательства или опровержения произвольного кода. Типичным ошибочным выводом из невозможности доказать произвольный код, является утверждение о невозможности доказать вообще любой код.

Рассмотрим пример.
Есть спецификация на функцию:
Код:
/*@ ensures \result == a; */
int func(int a);
Совершим невозможное:
Код:
/*@ ensures \result == a; */
int func(int a) {
     return a;
}
Что это? Это код на C и ACSL. ПО для подтверждения корректности кода на Си и больше примеров невозможного можно найти здесь https://frama-c.com/wp.html. Кстати, попробуйте угадать, что означает wp.

Следующим шагом на пути осознания доказательства корректности программ, является утверждение о том, что оно применимо только к простым случаям. Почему? Потому что в учебных материалах представлены только относительно простые примеры.

Тем не менее, не все об этом знают, и одни такие незнайки попытались доказать корректность микроядра операционной системы. Что из этого получилось, можно узнать на https://sel4.systems/.

Полное доказательство корректности программ полуавтоматическими средствами - это сложно и трудоёмко, тем не менее оно возможно и применяется в промышленности. Написание программ под доказательство без проведения полного подтверждения - это эффективный способ создания обычных программ. Но не стоит об этом спрашивать у среднестатистических профессионалов, пишущих на условном Javascript. Лучше спросите у них про пошаговый отладчик, ведь это основы.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Есть ли русификатор BlackBox 1.7 ?
СообщениеДобавлено: Четверг, 08 Март, 2018 21:10 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
budden писал(а):
Для достаточно сложной программы и спецификация будет достаточно сложной. Т.е. получится, что просто программа написана не на процедурном ЯП, а на декларативном языке спецификаций.

Типичное возражение, но неправильное. Такое можно было бы утверждать, если бы конечная программа генерировалась по спецификации. И хотя такой метод и применяется для исполняемых спецификаций, то есть программ, написанных на другом языке, но речь не о таком подходе.
Чтобы людям было понятно, я использую такую упрощенную аналогию - ошибки спецификаций не переносятся автоматически в программы так же, как ошибки тестов не переносятся в тестируемое приложение. Вы просто не сможете доказать соответствие программы некорректным спецификациям.

Цитата:
Ни те, ни другие не решают всех проблем и не могут служить основанием для полного отказа от отладки.
А вот это и есть передёргивание, в котором критика типичной работы в пошаговом отладчике как основы отладки и внедрения такого понимания со школы отождествляется с критикой отладки как таковой, что уже неоднократно опровергалось.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 08 Март, 2018 23:40 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Еще один аргумент против отладчика: отладчики (насколько я знаю) плохо справляются со случаем параллельности. Как отлаживать параллельную программу в отладчике!?!

А доказательный подход позволяет разработать правильную параллельную программу.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 08 Март, 2018 23:50 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Как утверждают создатели seL4, параллельность и для доказательного программирования - не сахар.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Есть ли русификатор BlackBox 1.7 ?
СообщениеДобавлено: Пятница, 09 Март, 2018 01:15 

Зарегистрирован: Понедельник, 11 Сентябрь, 2017 13:23
Сообщения: 1543
> А вот это и есть передёргивание,
Вы что-то домыслили, а потом и радостно опровергли. Оставляю это на вашей совести.
> Типичное возражение, но неправильное.
Код:
QWidget(QWidget *parent = Q_NULLPTR, Qt::WindowFlags f = Qt::WindowFlags())
~QWidget()
bool   acceptDrops() const
QString   accessibleDescription() const
QString   accessibleName() const
QList<QAction *>   actions() const
void   activateWindow()
void   addAction(QAction *action)
void   addActions(QList<QAction *> actions)
void   adjustSize()
bool   autoFillBackground() const
QPalette::ColorRole   backgroundRole() const
QBackingStore *   backingStore() const
QSize   baseSize() const
QWidget *   childAt(int x, int y) const
QWidget *   childAt(const QPoint &p) const
QRect   childrenRect() const
QRegion   childrenRegion() const
void   clearFocus()
void   clearMask()
QMargins   contentsMargins() const
QRect   contentsRect() const
Qt::ContextMenuPolicy   contextMenuPolicy() const
QCursor   cursor() const
WId   effectiveWinId() const
void   ensurePolished() const
Qt::FocusPolicy   focusPolicy() const
QWidget *   focusProxy() const
QWidget *   focusWidget() const
const QFont &   font() const
QFontInfo   fontInfo() const
QFontMetrics   fontMetrics() const
QPalette::ColorRole   foregroundRole() const
QRect   frameGeometry() const
QSize   frameSize() const
const QRect &   geometry() const
void   getContentsMargins(int *left, int *top, int *right, int *bottom) const
QPixmap   grab(const QRect &rectangle = QRect( QPoint( 0, 0 ), QSize( -1, -1 ) ))
void   grabGesture(Qt::GestureType gesture, Qt::GestureFlags flags = Qt::GestureFlags())
void   grabKeyboard()
void   grabMouse()
void   grabMouse(const QCursor &cursor)
int   grabShortcut(const QKeySequence &key, Qt::ShortcutContext context = Qt::WindowShortcut)
QGraphicsEffect *   graphicsEffect() const
QGraphicsProxyWidget *   graphicsProxyWidget() const
bool   hasEditFocus() const
bool   hasFocus() const
virtual bool   hasHeightForWidth() const
bool   hasMouseTracking() const
bool   hasTabletTracking() const
int   height() const
virtual int   heightForWidth(int w) const
Qt::InputMethodHints   inputMethodHints() const
virtual QVariant   inputMethodQuery(Qt::InputMethodQuery query) const
void   insertAction(QAction *before, QAction *action)
void   insertActions(QAction *before, QList<QAction *> actions)
bool   isActiveWindow() const
bool   isAncestorOf(const QWidget *child) const
bool   isEnabled() const
bool   isEnabledTo(const QWidget *ancestor) const
bool   isFullScreen() const
bool   isHidden() const
bool   isMaximized() const
bool   isMinimized() const
bool   isModal() const
bool   isVisible() const
bool   isVisibleTo(const QWidget *ancestor) const
bool   isWindow() const
bool   isWindowModified() const
QLayout *   layout() const
Qt::LayoutDirection   layoutDirection() const
QLocale   locale() const
QPoint   mapFrom(const QWidget *parent, const QPoint &pos) const
QPoint   mapFromGlobal(const QPoint &pos) const
QPoint   mapFromParent(const QPoint &pos) const
QPoint   mapTo(const QWidget *parent, const QPoint &pos) const
QPoint   mapToGlobal(const QPoint &pos) const
QPoint   mapToParent(const QPoint &pos) const
QRegion   mask() const
int   maximumHeight() const
QSize   maximumSize() const
int   maximumWidth() const
int   minimumHeight() const
QSize   minimumSize() const
virtual QSize   minimumSizeHint() const
int   minimumWidth() const
void   move(const QPoint &)
void   move(int x, int y)
QWidget *   nativeParentWidget() const
QWidget *   nextInFocusChain() const
QRect   normalGeometry() const
void   overrideWindowFlags(Qt::WindowFlags flags)
const QPalette &   palette() const
QWidget *   parentWidget() const
QPoint   pos() const
QWidget *   previousInFocusChain() const
QRect   rect() const
void   releaseKeyboard()
void   releaseMouse()
void   releaseShortcut(int id)
void   removeAction(QAction *action)
void   render(QPaintDevice *target, const QPoint &targetOffset = QPoint(), const QRegion &sourceRegion = QRegion(), RenderFlags renderFlags = RenderFlags( DrawWindowBackground | DrawChildren ))
void   render(QPainter *painter, const QPoint &targetOffset = QPoint(), const QRegion &sourceRegion = QRegion(), RenderFlags renderFlags = RenderFlags( DrawWindowBackground | DrawChildren ))
void   repaint(int x, int y, int w, int h)
void   repaint(const QRect &rect)
void   repaint(const QRegion &rgn)
void   resize(const QSize &)
void   resize(int w, int h)
bool   restoreGeometry(const QByteArray &geometry)
QByteArray   saveGeometry() const
void   scroll(int dx, int dy)
void   scroll(int dx, int dy, const QRect &r)
void   setAcceptDrops(bool on)
void   setAccessibleDescription(const QString &description)
void   setAccessibleName(const QString &name)
void   setAttribute(Qt::WidgetAttribute attribute, bool on = true)
void   setAutoFillBackground(bool enabled)
void   setBackgroundRole(QPalette::ColorRole role)
void   setBaseSize(const QSize &)
void   setBaseSize(int basew, int baseh)
void   setContentsMargins(int left, int top, int right, int bottom)
void   setContentsMargins(const QMargins &margins)
void   setContextMenuPolicy(Qt::ContextMenuPolicy policy)
void   setCursor(const QCursor &)
void   setEditFocus(bool enable)
void   setFixedHeight(int h)
void   setFixedSize(const QSize &s)
void   setFixedSize(int w, int h)
void   setFixedWidth(int w)
void   setFocus(Qt::FocusReason reason)
void   setFocusPolicy(Qt::FocusPolicy policy)
void   setFocusProxy(QWidget *w)
void   setFont(const QFont &)
void   setForegroundRole(QPalette::ColorRole role)
void   setGeometry(const QRect &)
void   setGeometry(int x, int y, int w, int h)
void   setGraphicsEffect(QGraphicsEffect *effect)
void   setInputMethodHints(Qt::InputMethodHints hints)
void   setLayout(QLayout *layout)
void   setLayoutDirection(Qt::LayoutDirection direction)
void   setLocale(const QLocale &locale)
void   setMask(const QBitmap &bitmap)
void   setMask(const QRegion &region)
void   setMaximumHeight(int maxh)
void   setMaximumSize(const QSize &)
void   setMaximumSize(int maxw, int maxh)
void   setMaximumWidth(int maxw)
void   setMinimumHeight(int minh)
void   setMinimumSize(const QSize &)
void   setMinimumSize(int minw, int minh)
void   setMinimumWidth(int minw)
void   setMouseTracking(bool enable)
void   setPalette(const QPalette &)
void   setParent(QWidget *parent)
void   setParent(QWidget *parent, Qt::WindowFlags f)
void   setShortcutAutoRepeat(int id, bool enable = true)
void   setShortcutEnabled(int id, bool enable = true)
void   setSizeIncrement(const QSize &)
void   setSizeIncrement(int w, int h)
void   setSizePolicy(QSizePolicy)
void   setSizePolicy(QSizePolicy::Policy horizontal, QSizePolicy::Policy vertical)
void   setStatusTip(const QString &)
void   setStyle(QStyle *style)
void   setTabletTracking(bool enable)
void   setToolTip(const QString &)
void   setToolTipDuration(int msec)
void   setUpdatesEnabled(bool enable)
void   setWhatsThis(const QString &)
void   setWindowFilePath(const QString &filePath)
void   setWindowFlag(Qt::WindowType flag, bool on = true)
void   setWindowFlags(Qt::WindowFlags type)
void   setWindowIcon(const QIcon &icon)
void   setWindowModality(Qt::WindowModality windowModality)
void   setWindowOpacity(qreal level)
void   setWindowRole(const QString &role)
void   setWindowState(Qt::WindowStates windowState)
void   setupUi(QWidget *widget)
QSize   size() const
virtual QSize   sizeHint() const
QSize   sizeIncrement() const
QSizePolicy   sizePolicy() const
void   stackUnder(QWidget *w)
QString   statusTip() const
QStyle *   style() const
QString   styleSheet() const
bool   testAttribute(Qt::WidgetAttribute attribute) const
QString   toolTip() const
int   toolTipDuration() const
bool   underMouse() const
void   ungrabGesture(Qt::GestureType gesture)
void   unsetCursor()
void   unsetLayoutDirection()
void   unsetLocale()
void   update(int x, int y, int w, int h)
void   update(const QRect &rect)
void   update(const QRegion &rgn)
void   updateGeometry()
bool   updatesEnabled() const
QRegion   visibleRegion() const
QString   whatsThis() const
int   width() const
WId   winId() const
QWidget *   window() const
QString   windowFilePath() const
Qt::WindowFlags   windowFlags() const
QWindow *   windowHandle() const
QIcon   windowIcon() const
Qt::WindowModality   windowModality() const
qreal   windowOpacity() const
QString   windowRole() const
Qt::WindowStates   windowState() const
QString   windowTitle() const
Qt::WindowType   windowType() const
int   x() const
int   y() const

Это - декларации публичных методов QWidget. Набросайте, если не затруднит, спецификацию, которую нужно доказать.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 01:20 

Зарегистрирован: Понедельник, 11 Сентябрь, 2017 13:23
Сообщения: 1543
> https://github.com/seL4
А при чём здесь Оберон и, особенно, его уникальные преимущества над таким богомерзким мейнстримом, как Си? Да по вам, батенька, застенки святой Инквизиции плачут.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 01:24 

Зарегистрирован: Понедельник, 11 Сентябрь, 2017 13:23
Сообщения: 1543
Rifat писал(а):
Еще один аргумент против отладчика: отладчики (насколько я знаю) плохо справляются со случаем параллельности. Как отлаживать параллельную программу в отладчике!?!

А доказательный подход позволяет разработать правильную параллельную программу.

В gdb (с которым я работал очень мало) можно по выбору останавливать один тред или все. MSVS останавливает все (правда, не обязательно сразу). CL останавливает только один. Думается, что проблемы gdb с отладкой параллельных программ связаны либо с ограниченными возможностями коммуникации (трудно остановить тред достаточно быстро без готовности со стороны самого треда), или с ошибками в самом gdb. Но конечно, да, семантика пошаговой отладки может разрушиться в многонитевой программе. Хотя если речь идёт о параллельности в разных процессах, я запускал одновременную отладку клиента JS и сервера на node.js - двумя отладчиками. Если поставить достаточно брекпойнтов, можно увидеть то, что нужно.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Есть ли русификатор BlackBox 1.7 ?
СообщениеДобавлено: Пятница, 09 Март, 2018 02:45 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
budden писал(а):
> А вот это и есть передёргивание,
Вы что-то домыслили, а потом и радостно опровергли. Оставляю это на вашей совести.
Что именно я домыслил? Что никто здесь не отвергает отладку, но Вы составили своё сообщение так, как будто отвергают?

А мы всего лишь не отождествляем отладку с работой в пошаговом отладчике. Отладчик-то в Blackbox, вообще, идёт по умолчанию и в школьной версии он тоже есть.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Есть ли русификатор BlackBox 1.7 ?
СообщениеДобавлено: Пятница, 09 Март, 2018 02:56 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
budden писал(а):
Это - декларации публичных методов QWidget. Набросайте, если не затруднит, спецификацию, которую нужно доказать.
Зачем? Это задача для тех кто всё это использует, пишет и тестирует.
Но я понимаю, почему Вы ответили так. Я зацепил лишнего текста в цитате. Я отвечал на это
budden писал(а):
Т.е. получится, что просто программа написана не на процедурном ЯП, а на декларативном языке спецификаций.
Это можно понять из текста моего ответа, но для этого нужно подумать.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 03:07 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
budden писал(а):
> https://github.com/seL4
А при чём здесь Оберон и, особенно, его уникальные преимущества над таким богомерзким мейнстримом, как Си? Да по вам, батенька, застенки святой Инквизиции плачут.
А где я здесь писал про уникальные преимущества Оберона и про такой богомерзкий мейнстрим, как Си? Денис, сами придумали, сами искромётно высмеяли? Я вижу, память Ваша слаба, но вообще-то я писал Вам не так давно: https://zx.oberon2.ru/forum/viewtopic.php?f=46&t=347#p2124
Comdiv писал(а):
Если Вас интересует производительность, почему не хотите в качестве выходного языка использовать Си или LLVM? Зачем Oberon?
Это https://zx.oberon2.ru/forum/viewtopic.p ... =347#p2131
Цитата:
Си имеет то преимущество перед С++, что он относительно простой, поэтому для него есть Tiny C Compiler, который транслирует в 10 раз быстрей, чем gcc без опций оптимизации. Т.е. всё неплохо. Также, tcc можно использовать как библиотеку, но лицензия Вам, наверное, не понравится
...
Оберон можно собирать быстрей, чем Си в силу дизайна языков, тем не менее tcc обеспечивает приличную скорость.
И это viewtopic.php?f=3&t=5809&start=20#p103704
Comdiv писал(а):
Для поиска повреждения памяти используются специальные средства, и это не пошаговая отладка, что было бы крайне накладным. Даже в Си это делается достаточно неплохо.
У Вас есть хорошая возможность поржать и над этим.

Всё, что сказано про программирование под доказательство и про пошаговый отладчик верно для большинства языков. Сожалею, что Вы так и не поняли этого.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 06:01 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8500
Откуда: Троицк, Москва
Comdiv писал(а):
Программирования под доказательство - это составление программы и её составных частей таким образом, чтобы её корректность по отношению к спецификации можно было доказать.
Беспокоит, что картинки рисуются чёрно-белые.

На самом деле речь о непрерывном спектре. Корректность доказать в точном смысле может оказать и невозможным, но качество дизайна может быть на порядок выше при на порядок меньших усилиях.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Есть ли русификатор BlackBox 1.7 ?
СообщениеДобавлено: Пятница, 09 Март, 2018 08:41 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1428
budden писал(а):
Это - декларации публичных методов QWidget. Набросайте, если не затруднит, спецификацию, которую нужно доказать.

Если нет спецификации, то и отлаживать нечего. Любая программа будет безошибочной.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 16:23 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Info21 писал(а):
Беспокоит, что картинки рисуются чёрно-белые.
Ну этим все страдают в той или иной степени. Нет?
Двоичные модели проще для восприятия, и если за собой мой оставляем право иметь комплексное мнение, то на модель оппонента, зачастую, уже не хватает скромных возможностей мозга.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 16:33 

Зарегистрирован: Понедельник, 11 Сентябрь, 2017 13:23
Сообщения: 1543
Comdiv писал(а):
А где я здесь писал про уникальные преимущества Оберона?

Возможно, не вы, возможно, не здесь, но в целом я услышал нечто типа: "отладчик в Обероне не нужен, т.к. Оберон - другой язык". В т.ч., из-за программирования под доказательство.

Так вот, я перебрал всё, что мне предлагали как основание ненужности отладчика, кроме п-п-д, и не нашёл ничего уникального. Не увидел, как из указанных особенностей оберона следует вредность или ненужность отладчика, который есть в других аналогичных языках и применяется с пользой. П-п-д осталось моей последней надеждой, но оказывается, что инструментов для п-п-д для Оберона нет, уникальной для Оберона эта возможность не является, в крупных проектах П-п-д не опробовано, выводы из опробования не сделаны, в школе ему явно не учат. Микроядро - оно на то и микро, килобайта на 4, наверное. Недостаточно репрезентативно. А значит, отказаться от отладчика предлагается авансом, в надежде на то, что п-п-д подвезут в светлом будущем и оно заработает. Извините, я это не куплю.


Последний раз редактировалось budden Пятница, 09 Март, 2018 16:42, всего редактировалось 2 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Есть ли русификатор BlackBox 1.7 ?
СообщениеДобавлено: Пятница, 09 Март, 2018 16:37 

Зарегистрирован: Понедельник, 11 Сентябрь, 2017 13:23
Сообщения: 1543
Comdiv писал(а):
Отладчик-то в Blackbox, вообще, идёт по умолчанию и в школьной версии он тоже есть.
Правильно было бы сказать, что вы заврались. Более дипломатично можно сказать, что мы все не договорились о том, что такое "отладчик". В т.ч. вы с Info21. Т.к. он сказал, что отладчика в школьной версии нет и не будет, а вы говорите, что он есть. Противоречие налицо. Я понял, что понятие отладчика не определено, поэтому см. тему в форуме по Info21. Здесь я исхожу из традиционного определения отладчика и из возможностей конкретно RemDebug.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 16:55 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
budden писал(а):
Возможно, не вы, возможно, не здесь, но в целом я услышал нечто типа: "отладчик в Обероне не нужен, т.к. Оберон - другой язык".
Я не виноват в том, что Вы слышите.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 16:59 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
budden писал(а):
П-п-д осталось моей последней надеждой, но оказывается, что инструментов для п-п-д для Оберона нет.
Увы, Вы так и не поняли, что такое программирование под доказательство. Я не знаю, что можно ещё сказать, чтобы объяснить.
Впрочем, в этой теме я отвечал не Вам, а Владимиру Ситникову - viewtopic.php?f=3&t=5809&start=140#p103822


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 17:26 

Зарегистрирован: Вторник, 27 Февраль, 2018 09:18
Сообщения: 73
Comdiv писал(а):
Написание программ под доказательство без проведения полного подтверждения - это эффективный способ создания обычных программ.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 17:32 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Владимир Ситников писал(а):
Спасибо за пояснение, вас понял, не вижу смысла продолжать дискуссию.
Похоже, что не поняли.
Я объяснил как мог, если есть уточняющие вопросы, их можно задать, для этого и создана тема. Ну или заявить, что "не вижу смысла продолжать дискуссию" - тоже вариант.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 09 Март, 2018 18:33 

Зарегистрирован: Вторник, 27 Февраль, 2018 09:18
Сообщения: 73
Comdiv писал(а):
Владимир Ситников писал(а):
Спасибо за пояснение, вас понял, не вижу смысла продолжать дискуссию.
Похоже, что не поняли.
Я объяснил как мог, если есть уточняющие вопросы, их можно задать, для этого и создана тема. Ну или заявить, что "не вижу смысла продолжать дискуссию" - тоже вариант.


Возможно, стоит созвониться (например, в Goolge Hangouts) -- меньше времени потратим, чем текст набивать.

Я вас понял, что seL4 это, якобы, промышленная штука с некими доказательствами.
Я понял, что farma-c позволяет указывать спецификации для языка C.

И?
1) В репозитории "доказательств" seL4 код вообще на Haskell. Круто. Чего ж. Ну, ясное дело, что синхронизация межу C и Haskell кодом идеальная и без ошибок
2) Те же seL4 говорят, что они предполагают идеальную работу железа. Ну, да, конечно, FDIV всегда работало верно. Иными словами, если возникает глюк железа, то всё их хвалёное доказательство трещит по швам
3) В seL4 английским по белому написано, что их "доказательство" не доказывает отсутствие timing атак. Иными словами, Spectre, Meltdown их доказательство никак не обнаруживает.
4) Нужно понимать, что seL4 используют свой "доказанный" (ну или как там) компилятор. Понятно дело, что когда формальной верификацией покрыто 100% кода (в том числе микрокод процессоров), то это хорошо. И? Хотя бы 5% проектов находятся в таком состоянии? Море проектов, которые просто берут GCC и/или LLVM/Clang и радуются.

Поймите меня правильно. Разумеется, где-то спецификация может и помочь. Но моё исходное мнение было в том, что есть много случаев, когда пошаговая отладка очень полезна. В той же теме я услышал "пошаговая отладка это разврат мозга на уровне импринтинга". Так там было?
Ну, пусть так и будет.

Я вижу, что вы пишете интересные штуки, но у меня совершенно нет желания, чтобы вы меня убеждали в том, что "пошаговая отладка мне не нужна". Даже, если по ходу я узнаю что-то интересное (типа seL4), всё равно считаю подобное обсуждение тратой времени впустую.

Я уже настолько привык к отсутствию серебряных пуль, что режет слух, когда говорят, что "пошаговый отладчик не нужен". Да, наверняка есть класс проблем, где пошаговая отладка только вредит. Но наверняка есть класс проблем, где пошаговая отладка эффективна.

И, кстати, когда я учил брата программированию, у него наблюдалась обратная ситуация: он мог подолгу "тупить в код", хотя достаточно было выполнить пошаговую отладку и понять почему ожидаемое поведение не соответствует желаемому.

Comdiv писал(а):
Совершим невозможное:

Я понял, что вы показали как спецификация связана с реальным C кодом.
Да, это, конечно, забавнее, чем писать программу отдельно, а Coq доказательство отдельно.
Но означает ли это, что код в farma-c стиле не требует пошаговой отладки?
По-моему, не означает.
1) Например, в самой спецификации может быть ошибка. Как её обнаружить? Вдумчиво глядеть на все спецификации?
Ну, подаём в программу массив, а она один из элементов "не туда" сортирует. Ответ "работает согласно спецификации", разумеется, не устраивает, и как предлагается обнаруживать ошибку?
2) Я могу всякое представить, но, как уже говорил, считаю, что многие выполняют "пошаговую отладку в уме", когда пытаются понять как именно будет работать написанный код, когда пытаются понять должно ли условие быть k<n или k<=n и т.п. Если с "запретом" пошаговой отладки в IDE одновременно идёт и запрет на пошаговую отладку "в уме", то, что ж, пусть так будет. Мне -- без разницы. Ну, я считаю это забавным, но тратить время на доводы в одну и/или другую сторону не хочу.
3) Что, если будет ошибка в компиляторе? Ну, подаём данные на вход, а выход неверный. Спецификация на месте. Как искать ошибку?
4) Что, если ошибка в памяти? Ну, записывается одно значение, а читается другое. Так вам спецификация на farma-c поможет
5) Что, если ошибка в сторонней системе? Пишете, например, клиентское приложение к PostgreSQL. Обложились спецификациями. А в реальности -- в PostgreSQL море ошибок. Как искать?

И, да, я понимаю, что отладка может быть "логированием" и/или "пошаговым выполнением" и/или много ещё чем-то. Я отладкой считаю любой процесс, который связан с осознанием того "почему же ожидания не совпали с реальностью". Не вижу чем "пошаговое выполнение в IDE" отличается от "пошагового прокручивания алгоритма в голове".
Например, "программа работает гораздо медленнее, чем ожидалось". Как понять почему? Можно, например, запрофилировать. Или залогировать времена прохождения ключевых точек. Или глазами весь код просмотреть.
И, да, я считаю, что пошаговое выполнение это несомненное добро, которое есть в мире программирования, и которого нет, например, у физиков. Мы можем провести эмуляцию пошагово. А физики -- хрен. Им гораздо сложнее понять почему как именно распадаются ядра и т.п.

---

Кстати, пользуясь случаем, предложу. У вас есть желание рассказать что-нибудь на тему тестирования, формальной верификации и т.п.
на конференции Гейзенбаг (Москва, 6-7 декабря) для рядовых тестировщиков/разработчиков? Конференция по вопросам тестирования, и доклад на подобную тему наверняка был бы интересен.
Понимаю, что подготовка доклада это время, но вдруг интересно?

Если что, я там в программном комитете. Приём заявок на зиму ещё не открыт, и, если есть желание, можно и раньше списаться.


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

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


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

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


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

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