Бывает ли так что программа скомпилировалась с первого раза и без ошибок
Бывает ли так что программа скомпилировалась с первого раза и без ошибок
Освоить работу с встроенным отладчиком, изучить категории ошибок, способы их обнаружения и устранения.
Тестирование и отладка программы
Ошибки, которые может допустить программист, условно делятся на три группы:
Синтаксические ошибки
Подобные ошибки могут возникнуть при неправильном написании директивы или имени функции (процедуры); при попытке обратиться к переменной или константе, которую не объявляли ( рис. 27.1); при попытке вызвать функцию (процедуру, переменную, константу) из модуля, который не был подключен в разделе uses ; при других аналогичных недосмотрах программиста.
Ошибки времени выполнения
Ошибка времени выполнения может возникнуть не только при загрузке программы, но и во время её работы. Например, если бы попытка чтения несуществующего файла была сделана не при загрузке программы, а при нажатии на кнопку, то программа бы нормально запустилась и работала, пока пользователь не нажмет на эту кнопку.
Однако ошибки времени выполнения могут случиться и во время работы с объектом. Если есть такой риск, программист должен не забывать про возможность обработки исключительных ситуаций. В данном случае вышеприведенный код правильней будет оформить таким образом:
Алгоритмические ошибки
Если вы не допустили ни синтаксических ошибок, ни ошибок времени выполнения, программа скомпилировалась, запустилась и работает нормально, то это еще не означает, что в программе нет ошибок. Убедиться в этом можно только в процессе её тестирования.
Тестирование — процесс проверки работоспособности программы путем ввода в неё различных, даже намеренно ошибочных данных, и последующей контрольной проверке выводимого результата.
Работа с отладчиком
Давайте от теории перейдем к практике. Загрузите Lazarus с новым проектом, установите на форму простую кнопку и сохраните проект в папку 27-01. Имена проекта, формы, модуля и кнопки изменять не нужно, оставьте имена, данные по умолчанию.
Далее, сгенерируйте событие OnClick для кнопки, в котором напишите следующий код:
Точки останова — это строки, перед выполнением которых отладчик приостанавливает выполнение программы, и ждет ваших дальнейших действий.
Установить точку останова можно разными способами:
Последние два способа наиболее удобны, но выбирать вам. В любом случае, строка с установленной точкой останова окрасится красным цветом:
Снять точку останова удобней также последними двумя способами. Точка останова у нас есть, снова нажимаем кнопку «Запустить». Программа начинает свою работу, нажимаем кнопку «Button1».
Теперь программа не вывела ошибку, а приостановила свою работу и вывела на передний план Редактор кодов с выделенной серым цветом строкой, которая в данный момент готовится к выполнению:
Встроенный отладчик имеет и другие инструменты, с которыми вы сами сможете со временем освоиться, экспериментируя с ними.
Итак, разобрались со средой разработки, теперь можно загрузить первую прошивку. Можно загрузить пустую прошивку, чтобы просто убедиться, что все драйвера установились и платы вообще прошиваются. Рекомендуется делать это с новой платой, к которой никогда не подключались датчики и модули, чтобы исключить выход платы из строя по вине пользователя.
1. Плата подключается к компьютеру по USB, на ней должны замигать светодиоды. Если этого не произошло:
2. Компьютер издаст характерный сигнал подключения нового оборудования, а при первом подключении появится окошко “Установка нового оборудования”. Если этого не произошло:
3. В списке портов (Arduino IDE/Инструменты/Порт) появится новый порт, обычно COM3. Если этого не произошло:
4. Выбираем свою плату. Если это Arduino Nano, выбираем в Инструменты\Плата\Arduino Nano. Если другая – выбираем другую. Нажимаем стрелочку в левом верхнем углу (загрузить прошивку). Да, загружаем пустую прошивку.
Если появилась надпись “Загрузка завершена” – значит всё в порядке и можно прошивать другие скетчи. В любом случае на вашем пути встретятся другие два варианта событий, происходящих после нажатия на кнопку “Загрузка” – это ошибка компиляции и ошибка загрузки. Вот их давайте рассмотрим более подробно.
Ошибки компиляции
Возникает на этапе сборки и компиляции прошивки. Ошибки компиляции вызваны проблемами в коде прошивки, то есть проблема сугубо софтварная. Слева от кнопки “загрузить” есть кнопка с галочкой – проверка. Во время проверки производится компиляция прошивки и выявляются ошибки, если таковые имеются. Ардуино в этом случае может быть вообще не подключена к компьютеру.
Частые ошибки в коде, приводящие к ошибке компиляции
Ошибки загрузки
Возникают на этапе, когда прошивка собрана, скомпилирована, в ней нет критических ошибок, и производится загрузка в плату по кабелю. Ошибка может возникать как по причине неисправностей железа, так и из-за настроек программы и драйверов.
Предупреждения
Помимо ошибок, по причине которых проект вообще не загрузится в плату и не будет работать, есть ещё предупреждения, которые выводятся оранжевым текстом в чёрной области лога ошибок. Предупреждения могут появиться даже тогда, когда выше лога ошибок появилась надпись “Загрузка завершена“. Это означает, что в прошивке нет несовместимых с жизнью ошибок, она скомпилировалась и загрузилась в плату. Что же тогда означают предупреждения? Чаще всего можно увидеть такие:
Завершая раздел Введение в Arduino поговорим о вопросах, которые очень часто возникают у новичков:
Видео
9 сентября 2013 Мария (admin)В этом уроке мы создадим нашу первую программу на языке Java.
Создание приложения на языке Java состоит из трех следующих шагов:
Создание исходного файла
Если вы пользуетесь Notepad++ то нужно выбрать Тип файла:Java source file (*.java)
Компиляция исходного файла
Исходный файл с кодом программы создан, теперь перейдем к компиляции. Для компиляции Java предназначен компилятор javac, который входит в состав установленного нами в первом уроке пакета JDK.
Для того, чтобы скомпилировать исходный файл, открываем командную строку. Для этого в меню Windows Пуск в строке поиска вводим команду cmd и жмем Enter. После этого откроется командное окно.
Теперь в нем нужно изменить текущий каталог на тот, в котором находится наш исходный файл (например C:\studyjava\). Для этого вводим следующую команду:
После того, как директория изменилась, вводим команду компиляции
После этого, окно командной строки должно выглядеть следующим образом (рис 2.2):
То есть, мы не получим никакого подтверждения, о том, что программа скомпилировалась успешно. Однако, в папке с нашим исходным файлом, должен появиться файл HelloWorld.class. Это можно проверить с помощью команды
Эта команда выводит на экран список всех файлов, находящихся в выбранной директории (рис 2.3).
Если файл HelloWorld.class присутствует в этом списке, то это значит, что программа скомпилировалась успешно.
Если в коде программы есть ошибка, то компилятор Java при компиляции нам об этом сообщит.
Запуск программы
Вводим в командном окне:
Еще раз обратите внимание на чувствительность к регистру в Java. Если вы напишете helloworld вместо HelloWorld, то программа запущена не будет, потому что Java попросту не найдет файл с таким именем.
Категория: Уроки Java
Надоели нестабильные баги в многопоточном коде? Попробуй воспользоваться модел-чекерами! Ведь больше не надо бояться неверифицированных модел-чекеров, работающих либо за экспоненциальное время, либо неоптимально. Все это в прошлом: в Max Planck Institute for Software Systems разработали новый алгоритм под названием TruSt, который решает эти проблемы и, кроме того, верифицирован на Coq.
Меня зовут Владимир Гладштейн. Этим летом я проходил стажировку в MPI-SWS в группе, которая придумала алгоритм нового модел-чекера для поиска багов в многопоточных программах. Этот алгоритм является оптимальным и truly stateless (вследствие чего работает с линейными затратами по памяти). В этом посте я расскажу, как работают модел-чекеры, в каких случаях их можно использовать, и что за алгоритм придумали мои коллеги. А еще как я проверял доказательства его корректности на Coq.
О себе
Я учусь на 4-ом курсе программы «Математика, алгоритмы и анализ данных» факультета математики и компьютерных наук СПбГУ, а также работаю в Лаборатории языковых инструментов JetBrains Research. Я больше двух лет изучаю формальную верификацию программ и в основном пишу на языке Coq.
О стажировке
Этим летом мне посчастливилось пройти стажировку в Max Planck Institute for Software Systems. Попал я туда неслучайно. Дело в том, что Лаборатория языковых инструментов JBR тесно сотрудничает с этим институтом. В частности, руководитель моей группы Антон Подкопаев был постдоком у профессора MPI Виктора Вафеядиса. Поэтому с рекомендацией от Антона на меня быстро обратили внимание и устроили собеседование с Виктором. В итоге меня зачислили стажером на два месяца — с июля по август 2021 года. Стажировка проходила дистанционно.
О проекте, в котором я работал
В начале лета команда в MPI-SWS, к которой я присоединился, готовилась к подаче статьи на конференцию POPL. Если вкратце, они придумали алгоритм нового модел-чекера (далее МС) для поиска багов в многопоточных программах и предложили мне формально проверить доказательства его корректности на Coq. Этой задачей я и занимался.
Но давайте обо всем по порядку. Начнем с Coq.
O Coq
Coq — это функциональный язык программирования с очень мощной системой зависимых типов. С помощью нее по соответствию Карри-Говарда в Coq удается формулировать и на специальном языке записывать доказательства теорем, которые он сможет проверить. Примеры формулировок теорем в Coq у нас еще будут, а пока, чтобы представлять о чем речь, можно почитать начало мягкого введения. Главное, что тут надо понять — на этом языке можно написать доказательство теоремы, и он его проверит. Среди CS сообщества считается, что теоремы, проверенные на Coq, не содержат ошибок в доказательствах.
О багах в многопоточном коде
Давайте разберем пример такой программы. Пример довольно объемный, но он поможет понять, в каких случаях разумно использовать модел-чекеры. Если хотите пропустить пример, жмите сюда.
Представьте себе любимый банк. А теперь представьте, что вас назначили программистом в этом банке и попросили написать код для обслуживания очередей. Человек приходит в банк, берет номерок и ждет своей очереди.
Условно ваша программа должна уметь:
Хранить номер билетика, который будет выдан следующему человеку;
Хранить номер билета человека, которого сейчас обслуживают;
Выдавать новые билеты;
Менять номер обслуживающегося билета.
Давайте попробуем написать такое на C, используя многопоточность. Сначала заведем структуру, описывающую память нашего автомата по выдаче билетов:
Так как мы будем писать многопоточный код, в котором поля данной структуры будут шариться между потоками, нам необходимо сделать их не просто int, a atomic_int.
Теперь давайте опишем процедуру выдачи билета человеку с его последующим ожиданием своей очереди:
Теперь можно описать процедуру перехода очереди от одного человека к другому:
Для простоты будем считать, что обслуживание человека заключается в том, что он кладет одну денежку на некоторый счет x, а потом происходит проверка, что значение x действительно увеличилось на один:
Однако наш банк должен обслуживать много людей, поэтому, чтобы смоделировать его работу, надо запустить процедуру thread в нескольких потоках одновременно:
Как мы хотим, чтобы работала наша программа? Рассмотрим на примере двух потоков (N_THREADS = 2).
Будем придерживаться модели памяти Sequential Consistency (то есть можно считать, что при запуске программы инструкции разных потоков перемешиваются, сохраняя свой порядок внутри одного потока, и запускается однопоточный код).
Допустим в банк пришли Петя (первый поток) и Вася (второй поток). В нормальной ситуации они находятся сначала на строке:
Предположим, что сначала работает первый поток (то есть Петя первый взял билетик):
Он получает билет номер 0, и следующий билет будет уже иметь номер 1. Потом, например, сюда может встроиться Васин (второй) поток и оттуда выполнится три строчки (Вася возьмет свой билет и сядет в очередь):
Наконец встраивается первый поток: Петя спокойно перескакивает бесконечный цикл (а не садится туда ждать), потому что номер его билета совпадает с номером билета, который будут обслуживать.
Далее первый поток выходит из ticket_lock и начинается обслуживание Пети:
Это хорошее поведение программы, так как хоть потоки и исполняются параллельно, мы не можем начать обслуживать Васю, пока не закончим обслуживать Петю.
Предположим теперь, что сначала в первом потоке выполняется первая инструкция ticketlock_lock :
Потом сразу вмешивается второй поток, и там выполняются первые две инструкции:
Наконец, выполняется следующая инструкция первого потока:
События могут развиваться как-то так: сначала, первый поток продолжает
Тут сразу встроился Вася:
И в итоге в первом потоке в y находится 0, а х уже равен 2, что ведет к невыполнению assert ’a.
Ясно, что тут возникла проблема, потому что Вася получил свой билет до того, как наша программа успела до конца обработать получение билета Петей. Поэтому чтобы ее решить, надо просто сделать так, чтобы один поток не мог влезть между двумя инструкциями, отвечающими за выдачу билета, пока их исполняет другой поток. А именно:
Для этого можно их объединить в одну атомарную инструкцию:
«Плохой» способ выполнения программы происходит достаточно редко, так что тестами его отловить непросто. Именно поэтому тут нужен какой-нибудь другой путь проверки ее корректности.
О Model Checker
Чтобы ловить такие баги, можно использовать MC. Что они делают? Это специальные программы, которые на вход берут ваш многопоточный код и стараются некоторым способом обойти все возможные сцены его исполнения (может быть по модулю некоторой эквивалентности). Для того чтобы понять, как они работают, давайте обратимся к семантике многопоточных программ.
О семантике многопоточных программ
Каждой многопоточной программе можно поставить в соответствие некоторый «граф исполнения». Каждый такой граф описывает определенное множество исполнений программы, ведущих к одному и тому же результату. То есть если у вас есть на руках такой граф, вы можете «почти» сказать, как исполнилась программа, но этого «почти» хватает, чтобы например понять, нарушались ли какие-то assert’ы или нет.
Пример: рассмотрим программу на неком псевдоязыке:
Этой программе соответствует несколько «графов исполнения». Например, такой:
В этом графе есть два типа вершин, они называются событиями:
W(x,i) — запись в переменную x числа i (например, инструкции x := 0 соответствует W(x,0) );
R(x,j) — чтение из переменной x числа j (например, если мы в r := x прочитали 2, то этому будет соответствовать R(x,2)).
Серые — program order. Они соответствуют порядку инструкций (например x:=1 идет после x:=0, поэтому между ними стоит стрелка);
Зеленые — reads from. Они показывают, откуда событие чтения берет свое значение (в данном случает r := x читает из x:= 2).
Смотря на этот граф, легко понять, что assert не срабатывает.
О моделях памяти
Запуская один и тот же код на разных языках или на разных процессорах, мы можем наблюдать разные поведения. Почему так происходит? Дело в том, что над вашим кодом компилятор, а потом и сам процессор могут проявлять разного рода оптимизации. Эти оптимизации изначально были написаны для однопоточного кода, поэтому они могут привести к тому, что программа поведет себя совсем не так как вы хотите (подробнее тут). Ну и отличия в поведениях программ как раз обуславливаются тем, что при разных энвайронментах эти оптимизации разные. Модели поведения многопоточных программ называются моделями памяти (далее MM). Самая простая и известная MM — это Sequential Consistency.
Если мы хорошо изучим конкретную ММ, то сможем по графу исполнения программы говорить, допустим он или нет при данной ММ. Поэтому ММ часто моделируются просто предикатами на графах.
О проблемах model checker
Итак, задача MC заключается в переборе всех возможных графов соответствующих данной программе.
MC можно оценивать по большому количеству параметров, вот три из них:
Оптимальность: так как MC занимается обходом графов, можно говорить, что он оптимален если обходит каждый граф соответствующий программе ровно один раз
Stateless/explicit-state: MC может хранить какие-то данные о графах, которые он уже обошел. Если он вообще никакой информации не хранит, то будем называть его Stateless.
Параметричность по MM: будем говорить, что МС параметричен по MM, если он работает для различных MM. Математически это моделируется так, что MC принимает на вход некоторый предикат на графах исчисления cons и дальше исследует графы, соответствующие этому предикату.
Самые успешные существующие MC являются параметричными по модели памяти, оптимальными и почти Stateless. То есть они не посещают одни и те же графы несколько раз, однако, хранят какую-то информацию о своей предыдущей работе, что ведет к экспоненциальным затратам по памяти.
О TruSt
Наконец, новый алгоритм, который был разработан в MPI-SWS, является первым оптимальным, параметричным по модели памяти и в то же время Stateless (вследствие чего имеет линейные затраты по памяти). Поэтому он и называется TruSt (Truly Stateless).
Tут, однако, стоит отметить, что он работает не для всех моделей памяти, а лишь для тех, которые удовлетворяют некоторым условиям. Сюда подходят такие модели памяти, как Sequential consistency (SC), Total store ordering (TSO) (еще про эту модель можно почитать тут), Partial store ordering (PSO), а также фрагмент модели памяти языка С/С++ (RC11).
MC ищет ошибки в многопоточной программе, но кто гарантирует, что в самом алгоритме МС нет ошибок? Ведь если они есть, model checker может ввести пользователя в заблуждение. Поэтому важно формально верифицировать МС. Как раз этим я и занимался. Я взял псевдокод, на котором алгоритм был представлен в статье, закодировал это в Coq и формально проверил некоторые теоремы о корректности этого алгоритма.
К сожалению, сам алгоритм устроен довольно сложно, и я не смогу его здесь описать. Все подробности можно найти в статье. А сейчас я расскажу достаточно общую схему того, как он был закодирован на языке Coq.
Зафиксируем для начала некоторый предикат модели памяти на графах сons :
Примерно так этот алгоритм и реализован. Посмотрим, как его кодировать в Coq.
Будем говорить, что граф G1 связан отношением ⇒ с графом G2 (и писать G1 ⇒ G2) если Visit(P, G1) вызовет Visit(P, G2) на верхнем уровне рекурсии. Далее введем некоторые обозначения:
G1 ⇒* G2 будет значить, что существует некоторый k такой, что G1 ⇒k G2
О том, что я проверил на Coq
Эта теорема говорит о том, что если мы за какое-то количество шагов можем дойти из начального графа в граф G, то граф G является консистентным. Эта теорема доказывается тривиально, так как алгоритм явно на каждом шаге проверяет графы на консистентность.
Тут написано, что если
cons G — граф G консистентен
p _sem G — граф G кодирует некоторое исполнение нашей программы,
то мы этот граф встретим на каком-то рекурсивном вызове. То есть эта теорема гарантирует, что мы точно проверим все возможные исходы.
Из этого легко следует теорема.
В Coq ее сформулировать не очень просто, поэтому покажу схематично. Пусть
G0 ⇒ G1 ⇒ G2 ⇒ … ⇒ Gn есть последовательность шагов из пустого графа в некоторый Gn
G0 ⇒ H1 ⇒ H2 ⇒ … ⇒ Hn есть последовательность шагов из пустого графа в некоторый Hn и
Тогда и все промежуточные графы тоже будут равны. То есть мы не посетим один и тот же граф два раза.
Эта теорема тоже очень непростая и следует из того, что обратная процедура к Visit детерминирована.
Итоги
В итоге я проверил на Coq полный набор теорем про корректность представленного алгоритма. В ходе этой проверки было:
Найдена куча ошибок и неточностей в доказательствах на бумажке. Некоторые леммы не доказывались в том виде, в котором они были сформулированы, и пришлось придумывать новые формулировки.
Некоторые теоремы (например, теорема об оптимальности) были переформулированы, чтоб точнее ухватить суть вещи, которую мы хотим доказать.
Также в ходе формализации я заметил, что одно место в алгоритме является избыточным, и его убрали. Если вкратце, то в этом месте делалась проверка, которая следовала из других проверок. Так как на корректность алгоритма это не влияло, то понять, что оно лишнее, было непросто. Я заметил, что в доказательствах оно не играет роли, и предложил его убрать.
Заключение
В этом проекте мне пришлось во многом выйти из своей зоны комфорта: я писал его на новом для себя диалекте языка Coq, общался с людьми на английском, пользовался GitLab’ом и т.д. Это однозначно ценный опыт, но самое главное, что мне удалось поработать с мега крутыми специалистами в области Weak Memory. Надеюсь, что я смогу продолжить сотрудничать с ними в будущем. Это была очень крутая стажировка!
Бывает ли так что программа скомпилировалась с первого раза и без ошибок
Освоить работу с встроенным отладчиком, изучить категории ошибок, способы их обнаружения и устранения.
Тестирование и отладка программы
Ошибки, которые может допустить программист, условно делятся на три группы:
Синтаксические ошибки
Подобные ошибки могут возникнуть при неправильном написании директивы или имени функции (процедуры); при попытке обратиться к переменной или константе, которую не объявляли ( рис. 27.1); при попытке вызвать функцию (процедуру, переменную, константу) из модуля, который не был подключен в разделе uses ; при других аналогичных недосмотрах программиста.
Как уже говорилось, компилятор при нахождении подобной ошибки приостанавливает процесс компиляции, выводит сообщение о найденной ошибке и устанавливает курсор на допущенную ошибку, или после неё. Программисту остается только внести исправления в код программы и выполнить повторную компиляцию.
Ошибки времени выполнения
Ошибка времени выполнения может возникнуть не только при загрузке программы, но и во время её работы. Например, если бы попытка чтения несуществующего файла была сделана не при загрузке программы, а при нажатии на кнопку, то программа бы нормально запустилась и работала, пока пользователь не нажмет на эту кнопку.
Однако ошибки времени выполнения могут случиться и во время работы с объектом. Если есть такой риск, программист должен не забывать про возможность обработки исключительных ситуаций. В данном случае вышеприведенный код правильней будет оформить таким образом:
Алгоритмические ошибки
Если вы не допустили ни синтаксических ошибок, ни ошибок времени выполнения, программа скомпилировалась, запустилась и работает нормально, то это еще не означает, что в программе нет ошибок. Убедиться в этом можно только в процессе её тестирования.
Работа с отладчиком
Давайте от теории перейдем к практике. Загрузите Lazarus с новым проектом, установите на форму простую кнопку и сохраните проект в папку 27-01. Имена проекта, формы, модуля и кнопки изменять не нужно, оставьте имена, данные по умолчанию.
Далее, сгенерируйте событие OnClick для кнопки, в котором напишите следующий код:
Итак, программу мы написали, сохранили, пора её компилировать. Нажмите кнопку «Запустить» на Панели управления (или ). Программа нормально скомпилировалась и запустилась. Нажмем кнопку Button1. И тут же получаем ошибку:
Установить точку останова можно разными способами:
Последние два способа наиболее удобны, но выбирать вам. В любом случае, строка с установленной точкой останова окрасится красным цветом:
Снять точку останова удобней также последними двумя способами. Точка останова у нас есть, снова нажимаем кнопку «Запустить«. Программа начинает свою работу, нажимаем кнопку «Button1«.
Теперь программа не вывела ошибку, а приостановила свою работу и вывела на передний план Редактор кодов с выделенной серым цветом строкой, которая в данный момент готовится к выполнению:
Встроенный отладчик имеет и другие инструменты, с которыми вы сами сможете со временем освоиться, экспериментируя с ними.