OberonCore https://forum.oberoncore.ru/ |
|
Определение и мифы о программировании под доказательство https://forum.oberoncore.ru/viewtopic.php?f=82&t=6231 |
Страница 1 из 2 |
Автор: | Comdiv [ Четверг, 08 Март, 2018 20:16 ] |
Заголовок сообщения: | Определение и мифы о программировании под доказательство |
Программирования под доказательство - это составление программы и её составных частей таким образом, чтобы её корректность по отношению к спецификации можно было доказать. Это единственный подход, позволяющий доказывать корректность программ, потому что невозможно создать метод для доказательства или опровержения произвольного кода. Типичным ошибочным выводом из невозможности доказать произвольный код, является утверждение о невозможности доказать вообще любой код. Рассмотрим пример. Есть спецификация на функцию: Код: /*@ ensures \result == a; */ Совершим невозможное:int func(int a); Код: /*@ ensures \result == a; */ Что это? Это код на C и ACSL. ПО для подтверждения корректности кода на Си и больше примеров невозможного можно найти здесь https://frama-c.com/wp.html. Кстати, попробуйте угадать, что означает wp.int func(int a) { return a; } Следующим шагом на пути осознания доказательства корректности программ, является утверждение о том, что оно применимо только к простым случаям. Почему? Потому что в учебных материалах представлены только относительно простые примеры. Тем не менее, не все об этом знают, и одни такие незнайки попытались доказать корректность микроядра операционной системы. Что из этого получилось, можно узнать на https://sel4.systems/. Полное доказательство корректности программ полуавтоматическими средствами - это сложно и трудоёмко, тем не менее оно возможно и применяется в промышленности. Написание программ под доказательство без проведения полного подтверждения - это эффективный способ создания обычных программ. Но не стоит об этом спрашивать у среднестатистических профессионалов, пишущих на условном Javascript. Лучше спросите у них про пошаговый отладчик, ведь это основы. |
Автор: | Comdiv [ Четверг, 08 Март, 2018 21:10 ] |
Заголовок сообщения: | Re: Есть ли русификатор BlackBox 1.7 ? |
budden писал(а): Для достаточно сложной программы и спецификация будет достаточно сложной. Т.е. получится, что просто программа написана не на процедурном ЯП, а на декларативном языке спецификаций. Типичное возражение, но неправильное. Такое можно было бы утверждать, если бы конечная программа генерировалась по спецификации. И хотя такой метод и применяется для исполняемых спецификаций, то есть программ, написанных на другом языке, но речь не о таком подходе. Чтобы людям было понятно, я использую такую упрощенную аналогию - ошибки спецификаций не переносятся автоматически в программы так же, как ошибки тестов не переносятся в тестируемое приложение. Вы просто не сможете доказать соответствие программы некорректным спецификациям. Цитата: Ни те, ни другие не решают всех проблем и не могут служить основанием для полного отказа от отладки. А вот это и есть передёргивание, в котором критика типичной работы в пошаговом отладчике как основы отладки и внедрения такого понимания со школы отождествляется с критикой отладки как таковой, что уже неоднократно опровергалось.
|
Автор: | Rifat [ Четверг, 08 Март, 2018 23:40 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Еще один аргумент против отладчика: отладчики (насколько я знаю) плохо справляются со случаем параллельности. Как отлаживать параллельную программу в отладчике!?! А доказательный подход позволяет разработать правильную параллельную программу. |
Автор: | Comdiv [ Четверг, 08 Март, 2018 23:50 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Как утверждают создатели seL4, параллельность и для доказательного программирования - не сахар. |
Автор: | budden [ Пятница, 09 Март, 2018 01:15 ] |
Заголовок сообщения: | Re: Есть ли русификатор BlackBox 1.7 ? |
> А вот это и есть передёргивание, Вы что-то домыслили, а потом и радостно опровергли. Оставляю это на вашей совести. > Типичное возражение, но неправильное. Код: 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 ®ion) 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. Набросайте, если не затруднит, спецификацию, которую нужно доказать. |
Автор: | budden [ Пятница, 09 Март, 2018 01:20 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
> https://github.com/seL4 А при чём здесь Оберон и, особенно, его уникальные преимущества над таким богомерзким мейнстримом, как Си? Да по вам, батенька, застенки святой Инквизиции плачут. |
Автор: | budden [ Пятница, 09 Март, 2018 01:24 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Rifat писал(а): Еще один аргумент против отладчика: отладчики (насколько я знаю) плохо справляются со случаем параллельности. Как отлаживать параллельную программу в отладчике!?! А доказательный подход позволяет разработать правильную параллельную программу. В gdb (с которым я работал очень мало) можно по выбору останавливать один тред или все. MSVS останавливает все (правда, не обязательно сразу). CL останавливает только один. Думается, что проблемы gdb с отладкой параллельных программ связаны либо с ограниченными возможностями коммуникации (трудно остановить тред достаточно быстро без готовности со стороны самого треда), или с ошибками в самом gdb. Но конечно, да, семантика пошаговой отладки может разрушиться в многонитевой программе. Хотя если речь идёт о параллельности в разных процессах, я запускал одновременную отладку клиента JS и сервера на node.js - двумя отладчиками. Если поставить достаточно брекпойнтов, можно увидеть то, что нужно. |
Автор: | Comdiv [ Пятница, 09 Март, 2018 02:45 ] |
Заголовок сообщения: | Re: Есть ли русификатор BlackBox 1.7 ? |
budden писал(а): > А вот это и есть передёргивание, Что именно я домыслил? Что никто здесь не отвергает отладку, но Вы составили своё сообщение так, как будто отвергают? Вы что-то домыслили, а потом и радостно опровергли. Оставляю это на вашей совести. А мы всего лишь не отождествляем отладку с работой в пошаговом отладчике. Отладчик-то в Blackbox, вообще, идёт по умолчанию и в школьной версии он тоже есть. |
Автор: | Comdiv [ Пятница, 09 Март, 2018 02:56 ] |
Заголовок сообщения: | Re: Есть ли русификатор BlackBox 1.7 ? |
budden писал(а): Это - декларации публичных методов QWidget. Набросайте, если не затруднит, спецификацию, которую нужно доказать. Зачем? Это задача для тех кто всё это использует, пишет и тестирует. Но я понимаю, почему Вы ответили так. Я зацепил лишнего текста в цитате. Я отвечал на это budden писал(а): Т.е. получится, что просто программа написана не на процедурном ЯП, а на декларативном языке спецификаций. Это можно понять из текста моего ответа, но для этого нужно подумать.
|
Автор: | Comdiv [ Пятница, 09 Март, 2018 03:07 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
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 можно использовать как библиотеку, но лицензия Вам, наверное, не понравится И это viewtopic.php?f=3&t=5809&start=20#p103704... Оберон можно собирать быстрей, чем Си в силу дизайна языков, тем не менее tcc обеспечивает приличную скорость. Comdiv писал(а): Для поиска повреждения памяти используются специальные средства, и это не пошаговая отладка, что было бы крайне накладным. Даже в Си это делается достаточно неплохо. У Вас есть хорошая возможность поржать и над этим.Всё, что сказано про программирование под доказательство и про пошаговый отладчик верно для большинства языков. Сожалею, что Вы так и не поняли этого. |
Автор: | Info21 [ Пятница, 09 Март, 2018 06:01 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Comdiv писал(а): Программирования под доказательство - это составление программы и её составных частей таким образом, чтобы её корректность по отношению к спецификации можно было доказать. Беспокоит, что картинки рисуются чёрно-белые.На самом деле речь о непрерывном спектре. Корректность доказать в точном смысле может оказать и невозможным, но качество дизайна может быть на порядок выше при на порядок меньших усилиях. |
Автор: | Trurl [ Пятница, 09 Март, 2018 08:41 ] |
Заголовок сообщения: | Re: Есть ли русификатор BlackBox 1.7 ? |
budden писал(а): Это - декларации публичных методов QWidget. Набросайте, если не затруднит, спецификацию, которую нужно доказать. Если нет спецификации, то и отлаживать нечего. Любая программа будет безошибочной. |
Автор: | Comdiv [ Пятница, 09 Март, 2018 16:23 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Info21 писал(а): Беспокоит, что картинки рисуются чёрно-белые. Ну этим все страдают в той или иной степени. Нет?Двоичные модели проще для восприятия, и если за собой мой оставляем право иметь комплексное мнение, то на модель оппонента, зачастую, уже не хватает скромных возможностей мозга. |
Автор: | budden [ Пятница, 09 Март, 2018 16:33 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Comdiv писал(а): А где я здесь писал про уникальные преимущества Оберона? Возможно, не вы, возможно, не здесь, но в целом я услышал нечто типа: "отладчик в Обероне не нужен, т.к. Оберон - другой язык". В т.ч., из-за программирования под доказательство. Так вот, я перебрал всё, что мне предлагали как основание ненужности отладчика, кроме п-п-д, и не нашёл ничего уникального. Не увидел, как из указанных особенностей оберона следует вредность или ненужность отладчика, который есть в других аналогичных языках и применяется с пользой. П-п-д осталось моей последней надеждой, но оказывается, что инструментов для п-п-д для Оберона нет, уникальной для Оберона эта возможность не является, в крупных проектах П-п-д не опробовано, выводы из опробования не сделаны, в школе ему явно не учат. Микроядро - оно на то и микро, килобайта на 4, наверное. Недостаточно репрезентативно. А значит, отказаться от отладчика предлагается авансом, в надежде на то, что п-п-д подвезут в светлом будущем и оно заработает. Извините, я это не куплю. |
Автор: | budden [ Пятница, 09 Март, 2018 16:37 ] |
Заголовок сообщения: | Re: Есть ли русификатор BlackBox 1.7 ? |
Comdiv писал(а): Отладчик-то в Blackbox, вообще, идёт по умолчанию и в школьной версии он тоже есть. Правильно было бы сказать, что вы заврались. Более дипломатично можно сказать, что мы все не договорились о том, что такое "отладчик". В т.ч. вы с Info21. Т.к. он сказал, что отладчика в школьной версии нет и не будет, а вы говорите, что он есть. Противоречие налицо. Я понял, что понятие отладчика не определено, поэтому см. тему в форуме по Info21. Здесь я исхожу из традиционного определения отладчика и из возможностей конкретно RemDebug.
|
Автор: | Comdiv [ Пятница, 09 Март, 2018 16:55 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
budden писал(а): Возможно, не вы, возможно, не здесь, но в целом я услышал нечто типа: "отладчик в Обероне не нужен, т.к. Оберон - другой язык". Я не виноват в том, что Вы слышите.
|
Автор: | Comdiv [ Пятница, 09 Март, 2018 16:59 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
budden писал(а): П-п-д осталось моей последней надеждой, но оказывается, что инструментов для п-п-д для Оберона нет. Увы, Вы так и не поняли, что такое программирование под доказательство. Я не знаю, что можно ещё сказать, чтобы объяснить. Впрочем, в этой теме я отвечал не Вам, а Владимиру Ситникову - viewtopic.php?f=3&t=5809&start=140#p103822 |
Автор: | Владимир Ситников [ Пятница, 09 Март, 2018 17:26 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Comdiv писал(а): Написание программ под доказательство без проведения полного подтверждения - это эффективный способ создания обычных программ. Спасибо за пояснение, вас понял, не вижу смысла продолжать дискуссию. |
Автор: | Comdiv [ Пятница, 09 Март, 2018 17:32 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
Владимир Ситников писал(а): Спасибо за пояснение, вас понял, не вижу смысла продолжать дискуссию. Похоже, что не поняли. Я объяснил как мог, если есть уточняющие вопросы, их можно задать, для этого и создана тема. Ну или заявить, что "не вижу смысла продолжать дискуссию" - тоже вариант. |
Автор: | Владимир Ситников [ Пятница, 09 Март, 2018 18:33 ] |
Заголовок сообщения: | Re: Определение и мифы о программировании под доказательство |
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 декабря) для рядовых тестировщиков/разработчиков? Конференция по вопросам тестирования, и доклад на подобную тему наверняка был бы интересен. Понимаю, что подготовка доклада это время, но вдруг интересно? Если что, я там в программном комитете. Приём заявок на зиму ещё не открыт, и, если есть желание, можно и раньше списаться. |
Страница 1 из 2 | Часовой пояс: UTC + 3 часа |
Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |