Рубрика «для чайников»

На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров.

Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.

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

Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.

Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.

Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.

Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.

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

А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.

Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.

Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.

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

Задача о 8 ферзях (Взята из англоязычного мануала).

Формальная верификация на примере задачи о волке, козе и капусте - 1
Читать полностью »

Вступление

На конференции YOW! 2013 один из разработчиков языка Haskell, проф. Филип Вадлер, показал, как монады позволяют чистым функциональным языкам осуществлять императивные по сути операции, такие, как ввод-вывод и обработку исключений. Неудивительно, что интерес аудитории к этой теме породил взрывной рост публикаций о монадах в Интернет. К сожалению, бо́льшая часть этих публикаций использует примеры, написанные на функциональных языках, подразумевая, что о монадах хотят узнать новички в функциональном программировании. Но монады не специфичны для Haskell или функциональных языков, и вполне могут быть проиллюстрированы примерами на императивных языках программирования. Это и является целью данного руководства.

Чем это руководство отличается от остальных? Мы попытаемся не более чем за 15 минут «открыть» монады, используя лишь интуицию и несколько элементарных примеров кода на Python. Мы поэтому не станем теоретизировать и углубляться в философию, рассуждая о буррито, космических скафандрах, письменных столах и эндофункторах.
Читать полностью »

На столбе висят три глаза, или сказ о том, что пяти ног ATtiny13 вполне достаточно - 1
КДПВ «Ой, всё».

Мало шансов, что сей лонгрид станет живительным источником мудрости интеллектуалам, искушенным в тайнах гадания на картах Карно и познавшим потаенный смысл Третьей Нормальной Формы. Но если вы зачем-то трогали руками arduino, в кладовке пылится паяльник, понимаете, почему у батарейки один плюс, а у С++ два, то вас не смогут оставить равнодушными поистине волшебные и удивительные чудеса. Итак, имею удовольствие рекомендовать вам номера сегодняшнего представления бродячего цирка «Саман с Самшитом»:

  • Добавление RAM и ROM в ATtiny13!
  • Искусственный интеллект в микропроцессор — про и контра, или спящая красавица — ну она не дура ли?
  • Или все таки dura lex sed lex?
  • Как добавить ножек в ATtiny13?
  • Пару слов о пятом измерении: как впихнуть невпихуемое?
  • Распиливание напополам не-девствениц с перемешиванием содержимых половин (с гарантией восстановления).
  • Номер «Кормление страждущих» (см. более ранний случай насыщения пяти тысяч человек пятью ячменными хлебами и двумя рыбами).

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

Читать полностью »

Вы понимаете, — втолковывал редактор, — это должно быть занимательно, свежо, полно интересных приключений… Так, чтобы читатель не мог оторваться.
И.Ильф, Е.Петров "Как создавался Робинзон".

Начинать работу с Arduino, как и с любой другой платформой программной или аппаратной, всегда интереснее с какого-нибудь реального проекта. Программисты при этом пишут код выводящий «Hello, world», ардуинисты моргают светодиодом. И все радуются как дети.

Я же решил начать с продвинутого проекта, в том числе с тайной надеждой оторвать молодое поколение от Counter-Strike (не получилось).

Как можно догадаться из названия RoboCar4W, первым проектом стал робот-машина о четырех колесах. Начиная работу я уже имел опыт программирования, умел когда-то давно паять, но совершенно не знал даже распиновки Arduino и документацию совершенно не читал. Все премудрости изучал по ходу пьесы и Гугл в помощь.

Читать полностью »

Добрый день, уважаемые читатели Хабра. Данный пост представляет из себя гайд по созданию динамической библиотеки .dll, которая содержит в себе сообщения, необходимые для отображения в кастомном логере, располагающимся в Windows Event ViewerApplication and Services Logsуууу (в качестве примера).

MC.exe (Message compiler), rc.exe, link.exe для формирования .dll для EventMessageFile - 1
Читать полностью »

Приветствую уважаемое сообщество!

Повторение — мать учения, а разбираться в синтаксическом анализе — очень полезный навык для любого программиста, поэтому хочу еще раз поднять эту тему и поговорить в этот раз про анализ методом рекурсивного спуска (LL), обойдясь без лишних формализмов (к ним потом всегда можно будет вернуться).

Как пишет великий Д. Строгов, «понять — значит упростить». Поэтому, чтобы понять концепцию синтаксического разбора методом рекурсивного спуска (оно же LL-парсинг), упростим задачу насколько можно и вручную напишем синтаксический анализатор формата, похожего на JSON, но более простого (при желании можно будет потом его расширить до анализатора полноценного JSON, если захочется поупражняться). Напишем его, взяв за основу идею нарезания строки.

Читать полностью »

Приветствую уважаемое сообщество.

Последнее время я уделял некоторое внимание теме синтаксического анализа (с целью в том числе улучшить собственные знания и навыки), и у меня создалось впечатление, что почти все курсы по компиляторам начинают с математических формализмов, и требуют сравнительно высокого уровня подготовки от изучающего. Либо там используется в большом количестве формальная математическая запись, как в классической Dragon Book, в которой, например, написано:

Пузырьковый вычислитель выражений: простейший синтаксический LR-анализатор вручную - 1

Это может с непривычки напугать. Нет, с какого-то момента формальная запись становится удобной и даже необходимой, но для “человека с улицы”, который хотел бы, чтобы ему “на пальцах” объяснили, “в чем тут дело”, это может быть сложно. А вопрос “что такое LL и LR — анализ, и в чем между ними разница” программисты задают довольно часто (потому что не все программисты имеют формальное образование в области Computer Science, как и я, и не все из них проходили там курс по компиляторам).

Мне более близок подход, когда сначала мы берем задачу, пытаемся ее решить, и в процессе решения сначала вырабатываем интуитивное понимание принципа, а потом уже для этого понимания создаем математические формализмы. Поэтому я на очень простом примере в этой статье хочу показать, какая идея лежит в основе восходящего синтаксического анализа (он же bottom-up parsing, он же LR). Будем вычислять арифметическое выражение, в котором для еще большего упрощения будем поддерживать только операторы сложения, умножения и скобки (чтобы не усложнять пример отрицательными числами и поддержкой унарного минуса).

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

Недавно в институте я столкнулся с любопытной криптографической задачей, которой хотел бы поделиться с Сообществом. Так как русскоязычных примеров решения таких учебных «головоломок» встречается немного, а сама задача рекомендована для начинающих свой путь специалистов (не обладающих глубокими знаниями предмета), я считаю, что такая статья может быть интересна юному криптоаналитику. Пожалуйте под кат.Читать полностью »

часть 1
Продолжаем анализировать что происходит на нашем MS SQL сервере.
В этой части посмотрим как получить информацию о работе пользователей: кто и что делает, сколько ресурсов на это расходуется.
Думаю, вторая часть будет интересна не только админам БД, но и разработчикам (возможно даже разработчикам больше), которым необходимо разбираться, что не так с запросами на рабочем сервере, которые до этого отлично работали в тестовом.
Задачи анализа действий пользователей условно поделим на группы и рассмотрим каждую отдельноЧитать полностью »

Недавно столкнулся с проблемой — занедужил SVN на ubuntu server. Сам я программирую под windows и с linux “на Вы”… Погуглил по ошибке — безрезультатно. Ошибка оказалась самая типовая (сервер неожиданно закрыл соединение) и ни о чем конкретном не говорящая. Следовательно, надо погружаться глубже и анализировать логи/настройки/права/и т.п., а с этим, как раз, я “на Вы”.

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

Писать я буду не про линукс — проблему хоть и решил, но профессионалом вряд ли стал. Напишу про более знакомый мне MS SQL. Благо, уже приходилось много раз отвечать на вопросы и список типовых уже готов.

Для кого пишу

Если вы админ в Сбере (или в Яндексе или <другая топ-100 компания>), вы можете сохранить статью в избранное. Да, пригодится! Когда к вам, в очередной раз, с одними и теми же вопросами придут новички — Вы дадите им ссылку на нее. Это сэкономит Ваше время.

Если без шуток, эта СУБД часто используется в небольших компаниях. Часто совместно с 1С либо другим ПО. Отдельного БД-админа таким компаниям держать затратно — надо будет выкручиваться обычному ИТ-шнику. Для таких и пишу.
Читать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js