Рубрика «alloy»

в 13:25, , рубрики: alloy, Анализ и проектирование систем, конечные автоматы, Программирование, Формальный методы

Привет! Представляю вашему вниманию перевод статьи «FORMALLY SPECIFYING UIS» автора Hillel Wayne.

Применение формальных методов валидации моделей для UI - 1

От автора

Относительно недавно я наткнулся на статью про Инженерные методы в разработке ПО, где vasil-sd рассказал про формальную валидацию спецификаций к создаваемым программным продуктам. В качестве инструментария был использован Alloy. Одним из основных лейтмотивов в комментариях был — разобрать статью в контексте какого-нибудь современного веб проекта, потому что дорогодолгосложно использовать формальные методы там, где все делают быстродешево. Так как автор ссылался на блог Hillel Wayne, где такие примеры были, я решил перевести что-то из его статей в качестве дополнения к основному тексту vasil-sd

Предупреждение:

  • Все, что автор называет finite-state machine, я буду называть конечным автоматом или моделью конечного автомата.
  • Часть терминологии я почерпнул из статьи, ранее мною упомянутой, об инженерном подходе к разработке. Тем не менее, тема для меня относительно новая, потому обоих авторов(как зарубежного, так и не очень) мог понять не так — не ругайтесь.

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

в 8:20, , рубрики: alloy, model-driven engineering, Анализ и проектирование систем, Блог компании Яндекс, Проектирование и рефакторинг, разработка под windows, управление разработкой

Как проверить идеи, архитектуру и алгоритмы без написания кода? Как сформулировать и проверить их свойства? Что такое model-checkers и model-finders? Требования и спецификации — пережиток прошлого?

Привет. Меня зовут Васил Дядов, сейчас я работаю программистом в Яндексе, до этого работал в Intel, ещё раньше разрабатывал RTL-код (register transfer level) на Verilog/VHDL для ASIC/FPGA. Давно увлекаюсь темой надёжности софта и аппаратуры, математикой, инструментами и методами, применяемыми для разработки ПО и логики с гарантированными, заранее определёнными свойствами.

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

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

Инженерный подход к разработке ПО - 1

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

в 20:09, , рубрики: ACL2, alloy, Altran, Cleanroom, CompCert, Euclid, IronFleet, Isabelle, Praxis, smt, TLA+, z3, контрактное программирование, контракты, логика Хоара, математика, Надя Поликарпова, Программирование, решатель, типизация, формальные методы, формальные языки, языки спецификаций

На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на самом деле не используются и что мы делаем для исправления ситуации.

Прежде чем начать, нужно сформулировать некоторые условия. На самом деле существует не так много формальных методов: всего несколько крошечных групп. Это означает, что разные группы по-разному применяют термины. В широком смысле есть две группы формальных методов: формальная спецификация изучает запись точных, однозначных спецификаций, а формальная проверка — методы доказательства. Сюда входят и код, и абстрактные системы. Мало того, что мы используем разные термины для кода и систем, мы часто используем разные инструменты для их верификации. Чтобы ещё больше всё запутать, если кто-то говорит, что создаёт формальную спецификацию, обычно это означает и верификацию дизайна. А если кто-то говорит, что делает формальную верификацию, обычно это относится к верификации кода.
Читать полностью »

в 14:44, , рубрики: alloy, hyperx, Блог компании Kingston Technology, гаджеты, киберспорт, клавиатура, механика, механическая клавиатура, Настольные компьютеры, периферия

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

HyperX Alloy FPS RGB – первая игровая клавиатура HyperX с RGB-подсветкой в переключателях, киллер-фичей которой стали как раз переключатели. Вместо классики Cherry MX Speed Silver в Alloy FPS установлены превосходящие их Kailh Silver Speed. На Хабре нет места пустым заявлениям, поэтому приступаем к доказательствам.

Ни единого шанса сопернику – берём на вооружение ультраскоростную клавиатуру HyperX Alloy FPS RGB - 1
Читать полностью »

в 15:46, , рубрики: alloy, cherry mx red, hyperx, Блог компании Kingston Technology, механическая клавиатура, периферия

Есть такая поговорка: хорошего человека должно быть много. К хорошим клавиатурам это тоже относится, но далеко не всегда в прямом смысле слова.

HyperX Alloy FPS Pro: tenkeyless-дизайн классической механики для любителей качественной периферии - 1

Иногда хочется, чтобы хорошей клавиатуры было как можно меньше — и вот компактная механика HyperX Alloy FPS PRO уже здесь. Tenkeyless-дизайн и возможность всегда взять любимицу с собой в комплекте.
Читать полностью »

в 17:14, , рубрики: alloy, alloy elite, cherry mx, hyperx, hyperx alloy, keyboard, mechanical keyboard, Блог компании Kingston Technology, Железо, игры, клавиатура, механика, периферия

Привет, GT! Споры о том, что есть «благо» в мире клавиатур не утихают, и правду-то не найти никакими средствами. Ладно субъективные характеристики, о вкусах не спорят и всё такое, но так и «объективщину» ухитряются зацепить так, что модераторы за табельное оружие хватаются.

HyperX Alloy Elite — железная заявка на победу - 1

Игровое подразделение HyperX уже пробовало свои силы в создании хорошей универсальной клавиатуры, настало время для второй попытки. Сегодня подробно изучаем HyperX Alloy Elite  — скелетную «механику» для работы и игр. Погнали!
Читать полностью »

в 10:19, , рубрики: alloy, alloy discovery, alloy navigator, internet of things, IoT, ITIL, itsm, Блог компании Alloy Software, будущее здесь, будущее рядом, ит-инфраструктура, мониторинг сети, Серверное администрирование, системное администрирование, метки:

У каждой компании-разработчика настаёт такой период в жизненном цикле, когда приходит понимание того, что будущее уже здесь. И нужно срочно определить, ты уже в будущем, ты безнадёжно отстал или тебе его ещё можно догнать и встроиться в него. Мы много лет занимаемся системами мониторинга сети и управления ИТ-инфраструктурой. Ну то есть ITIL, SAM, ITSM — наше всё. В последнее время на конференциях, семинарах и конгрессах мы всё чаще сталкиваемся с понятием IoT (интернет вещей). Нам интересно, что ждёт нашу компанию в контексте этих процессов, как вообще IoT влияет на бизнес и как дальше жить. Мы изучили проблему, ответили на свои же вопросы и сегодня готовы поделиться рассуждениями с вами. Всё получилось не так визионерски и фантастически, как мы это предполагали. Проза жизни, проза технологий, и немного паники.

А вот и IoT - 1
Читать полностью »

в 16:30, , рубрики: alloy, cherry mx, Cherry MX Blue, cherry mx brown, cherry mx red, hyperx, Kingston, Блог компании Kingston Technology, гаджеты, Железо, игры, клавиатура, механическая клавиатура, периферия

Продукция компании HyperX с самого начала была нацелена на тех, кому нужна была максимальная производительность и надёжность: профессионалы, игроки, оверклокеры. Первые продукты — отобранная и протестированная память, готовая работать на агрессивных таймингах и быстрые SSD с отличными показателями и расширенной гарантией легко завоевали сердца покупателей. Эксперимент с гарнитурами, построенными по тем же принципам: надёжность и эффективность — оказался удачным, и вот настало время ещё одного периферийного девайса.

HyperX Alloy FPS — надёжность превыше всего - 1

Каждый раз, как на GT появляется тема с выходом новой (игровой) клавиатуры, она порождает знатную войну в комментариях. Начинается всё с прений на тему ISO’шный «гнутый» Enter против ANSI’шного «прямого», затем идёт критика дополнительных кнопочек, подсветок, выбранных свичей, материалов корпуса… В общем, традиции в комментах вы и сами соблюдёте, а пока встречайте: механическая клавиатура Alloy FPS. Красная подсветка, модный нынче минимализм и, ставший классическим для продукции HyperX акцент на надёжность — в комплекте.
Читать полностью »

в 9:41, , рубрики: alloy, appcelerator, javascript, titanium, разработка мобильных приложений

Следующее высказывание с легкостью может прозвучать от того, кто только что начал изучать Titanium:

JavaScript?! Как Phonegap? Не, я лучше сделаю нативное приложение.

Разумеется, у меня были подобные беседы с клиентами, когда я был фриланс-разработчиком на Titanium. И уж конечно, как Developer Advocate, я частенько слышу это когда начинаю объяснять Titanium разработчикам, которые ищут кросс-платформенное решение для создания приложений.
Читать полностью »

Главная   |  Архив новостей  |   Android  |   Google  |   Apple  |   Microsoft  |   Информационная безопасность  |   Веб – разработка
Публикации RSS  |  Комментарии RSS
https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js