В своей прошлой статье я описал процесс верификации примитивной функции на Си. Параллельно привел соображения, почему верификация Си кода недостаточна для того, чтоб считать программу безошибочной. В основном эти соображения сводятся к мысли, что написать код — это только часть истории о получении работающей программы. Следующим приближением к тому, чтобы получить действительно безошибочную программу, является верификация ассемблерных кодов, их уже не нужно будет транслировать и поэтому полностью исключится обширное поле для возникновения ошибок. В данной статье я опишу процесс доказательства некоторых свойств уже для ассемблерного кода, который на порядок примитивней, чем даже простейшая функция на Си, о которой говорилось в прошлой статье.
Читать полностью »
Рубрика «математика» - 190
Верификация программ на ARM ассемблере
2012-10-29 в 4:41, admin, рубрики: верификация, верификация программ, математика, Программирование, формальная верификаци, функциональное программирование, метки: верификация, верификация программ, формальная верификациБиблиотека «всех» знаний
2012-10-26 в 17:34, admin, рубрики: бред, гигантомания, Земля, информация, Исследования и прогнозы в IT, математика, философия, числа, метки: бред, гигантомания, Земля, информация, философия, числа
Ниже Вы прочитаете некоторые размышления из области абсолютизма и оторванности от реальности. В тексте будут представлены философско-числовые измышления (бредни) о субполной и бесполезной библиотеки всего и вся. Точнее образов всего и вся. Если не испугались, то прошу в статью. Как показали вычисления, Землю придется разобрать. И не одну.
Данные мысли была навеяны постом Программы как произведения искусства, где рассказывалось о книге, в которой была цитата: «любая цивилизация рано или поздно придумает и теорему Пифагора, и атомный реактор. А вот нарисует ли она те же картины, напишет ли ту же музыку и снимет ли те же фильмы? Наверняка нет». А если это не так?Читать полностью »
Испытания протокола TCP с линейным сетевым кодированием (TCP/NC)
2012-10-24 в 13:43, admin, рубрики: tcp, Алгоритмы, линейная алгебра, математика, Сетевые технологии, метки: tcp, линейная алгебра
Инженеры из Массачусетского технологического института под руководством Муриель Медард (Muriel Médard) уже много лет ведут разработку расширения TCP/NC для протокола TCP, с помощью которого можно сохранить максимальную скорость передачи данных в сетях с потерями пакетов. В первую очередь, TCP/NC планируют применять в беспроводных сетях WiFi, где потери пакетов обычно составляют 2-5%, а временами до 10%. Наконец-то дошло дело до реальных экспериментов.
Во время первых полевых испытаний TCP/NC в локальной WiFi-сети общежития МТИ (потеря пакетов 2%) средняя скорость передачи данных по WiFi выросла с 1 Мбит/с до 16 Мбит/с. Тест в поезде на большой скорости (потеря пакетов 5%) показал увеличение скорости WiFi с 0,5 Мбит/с до 13,5 Мбит/с. Это вполне совпадает с теоретическими расчётами.
Читать полностью »
Научный журнал по математике принял статью от генератора текстов Mathgen
2012-10-19 в 22:34, admin, рубрики: генератор текстов, математика, научные статьи, метки: генератор текстов, научные статьи3 августа 2012 года вымышленный профессор Marcie Rathke из несуществующего Университета Южной Северной Дакоты отправил статью в научный журнал Advances in Pure Mathematics, один из многих журналов издательства Scientific Research Publishing.
Статья под названием «Независимые, отрицательные, канонические стрелы Тьюринга в уравнениях и задачах прикладной формальной PDE» (pdf) сопровождалась интригующей аннотацией: «Пусть ρ = A. Возможно ли расширить область изоморфизма? Мы показываем, что D′ является стохастически ортогональным и тривиально-аффинным соответствием. В [10], основным результатом стала конструкция множества Кардано, функции Эрдёша, Вейля, что может пролить важный свет на гипотезу Конвея-Д’Аламбера».
И аннотация, и весь текст, и список литературы в этой «научной статье» были сгенерированы программой Mathgen, которую написал математик Натан Элдридж (Nate Eldredge). Он с гордостью заявил, что статью в итоге приняли для публикации.
Читать полностью »
Бесплатный MATLAB для студентов онлайн курсов
2012-10-15 в 19:28, admin, рубрики: Matlab, octave, искусственный интеллект, математика, нейронные сети, образование, онлайн-курсы, Учебный процесс в IT, халява студентам, метки: Matlab, octave, нейронные сети, образование, онлайн-курсы, халява студентам
Буду краток. Компания Matlab сделала шаг навстречу удаленному обучению и предоставила свой продукт бесплатно скачать торрент без смс для студентов Courcera.
Читать полностью »
Математический подход к созданию сайтов
2012-10-10 в 12:35, admin, рубрики: Веб-разработка, дизайн, дизайн сайтов, макет интерфейса, математика, синусоида, фибоначчи, метки: дизайн, дизайн сайтов, макет интерфейса, математика, синусоида, фибоначчи«Математика прекрасна». Это может показаться абсурдным, для людей которые при одном только упоминании математики вздрагивают. Однако некоторые из самых красивых вещей в природе и нашей Вселенной — это проецирование математических свойств, от самых маленьких до крупнейших галактик. Один из древних философов, Аристотель сказал: «математическим наукам свойственно выстраивать все по порядку, в симметрии и ограничениях, они являются главными формами прекрасного».
Из-за своей природной красоты, математика является частью искусства и архитектуры. Но она практически не применяется для дизайна сайтов и приложений. Это наблюдается из-за того, что многие не сопоставляют математику с дизайном. Хотя, наоборот, математика может быть инструментом для производства, поистине волшебных конструкций. Тем не менее, вы не должны полагаться на математику для каждого своего творения. Дело в том, что вы должны рассматривать математику как вашего помощника. Для наглядности мы создали пару сайтов, которые представляют математические принципы, обсуждаемые в этой статье. Мы также создали рекомендации, которые можно использовать в дизайне.
Немного о хаосе и о том, как его сотворить
2012-10-10 в 5:36, admin, рубрики: математика, Теория Хаоса, Электроника для начинающих, метки: Теория Хаоса
Говоря «хаос», мы, обычно, подразумеваем полное отсутствие порядка, абсолютную неупорядоченность и случайность. С математической точки зрения, хаос и порядок – понятия не взаимоисключающие. Теория хаоса (есть что-то завораживающие в названиях математических теорий) – достаточно молодая математическая область, создание которой приравнивают по значимости открытий ХХ века к созданию квантовой механики. Хаос случается в нелинейных динамических системах. Иначе говоря, любой процесс, который протекает со временем, может быть хаотичным (например, высота дерева, температура тела или популяция мадагаскарских тараканов).
Читать полностью »
Почему оценкам в App Store не следует доверять
2012-10-09 в 19:25, admin, рубрики: App Store, apple, data mining, анализ, математика, ревью, метки: app store, data mining, анализ, ревью Задумывались ли вы когда-либо над тем, насколько хорошо работает пятизвездочная система оценивания мобильных приложений, скажем, в AppStore? До какой степени количество звезд, полученное тем или иным приложением, является показателем его качества? Почему представленный ниже явно отрицательный отзыв идет с оценкой «5», и насколько часто имеют место подобные случаи «неадекватного» оценивания приложений?
Мы – исследовательское подразделение компании Empatika – сделали попытку ответить на эти вопросы и пришли к неутешительному выводу: пользователи AppStore демонстрируют явно выраженную склонность к более частому выставлению положительных оценок, чем отрицательных, зачастую совершенно не заботясь о соответствии текста своего отзыва выставленному вместе с ним количеству звезд. Этот результат нашего исследования не так давно был опубликован на TechCrunch. О том, как мы пришли к этому выводу – читайте под катом.
Используем возможности Wolfram Mathematica в .NET приложениях
2012-10-09 в 10:18, admin, рубрики: .net, mathematica, Wolfram, компьютерная алгебра, математика, Программирование, метки: .net, mathematica, Wolfram, компьютерная алгебраЕсть люди, которым нравится писать .NET приложения. Есть люди, которые любят системы компьютерной алгебры. В этой статье круги Эйлера пересекутся!
Программирование в Maxima
2012-10-06 в 17:03, admin, рубрики: maple, mathcad, mathematica, Matlab, maxima, octave, open source, компьютерная алгебра, математика, математический пакет, математическое моделирование, функциональное программирование, метки: maple, mathcad, mathematica, Matlab, maxima, octave, компьютерная алгебра, Лисп, математика, математический пакет, математическое моделирование, функциональное программированиеУрок Maxima
Введение
Maxima — свободная система компьютерный алгебры (Computer algebra system — CAS), основанная на Commmon Lisp. В своих функциональных возможностях она едва уступает другим современным платным CAS, таким как Mathcad, Mathematica, Maple; может проводить аналитические (символьные) вычисления, численные расчеты, строить графики (при помощи gnuplot). Имеется возможность написания скриптов и даже трансляции их в код на Common Lisp с последующей компиляцией. В виду того, что maxima писалась из разрабатывалась программистами lisp, ее синтаксис может показаться несколько запутанным, поскольку язык является сразу и императивным и функциональным. Я попытаюсь разъяснить именно эти моменты и доступно изложить суть функционального подхода, и совсем не буду акцентировать внимания на конкретных математических функциях: их довольно легко освоить самостоятельно. В данной статье рассматривается именно особенности исчисления и синтаксических конструкций maxima.Читать полностью »