Обсуждение

> что модель, например, не начнет в какой-то момент делить на ноль где-то внутри себя, или не зациклится в самый неожиданный момент почему-то приходит на ум Гёдель...

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

В этом-то и дело, что книжек много, а текущей практики нет: одни исследования. Не идет почему-то доказательство правильности программ в программистский быт...

Как я его понял, он предлагает не столько доказательство того, что модель описывает систему, которая достигнет определенного результата, сколько доказательство правильности самой модели (что модель, например, не начнет в какой-то момент делить на ноль где-то внутри себя, или не зациклится в самый неожиданный момент). Я имел в виду и то, и другое, просто часто одни свойства можно вывести из других (простым способом). Т.е. вообще говоря, нет нужды приводить доказательства всех свойств, нужны доказательства некоторых ключевых. Тут надо пояснить, что отладка (логических) моделей отличается от отладки программ. С моделями основная проблема - что они могут оказаться невыполнимы. С точки зрения логики, это значит что из них можно вывести False, а из False - что угодно. Таким образом, теряется смысл формального обоснования. Т.е. первое требование при импорте модели, чтобы она была выполнима. В онтологиях типа OWL этот вопрос специально решался использованием дескрипционных логик, для которых есть практичные алгоритмы разрешимости. И которые позволяют отвечать на некоторые другие вопросы (типа классификации, проверки принадлежности индивидуала модели и т.д.). А в более сложном случае, дескрипционных логик не хватает. При этом этот более сложный случай не за горами, ибо после онтологий, все уже хотят использовать rules совместно с онтологиями :).

Тут вот мысли, как мне кажется, сходные с тем, что Вы говорите (если я правильно Вас понял): - Formal methods were applied in response to an existing development problem. - Formal methods were applied selectively. Only the most critical portions of the requirements were modele - In each case, formal methods offered a partial solution to the original problem. - In each case, the results of the study fed back into the development process to improve the product. Вообще это очень интересная тема. И в ЖЖ все чаще встречаются люди, которые серьезно занимаются Coq и Agda. Я и сам сделал проектик, близкий по теме, но больше все-таки к математике относящийся.

Я Coq тоже занимаюсь :)

beroal тоже, ежели не бросил еще.

Тема да, интересная. Там в статье использовали PVS, а его народ часто использует для моделирования системы перед началом разработки. По моему опыту подобное моделирование весьма полезно для понимание требований, даже если кода никакого не генерить. Естественно, надо применять селективно к критическим участкам.

У меня есть давняя, но довольно сумасшедшая идея, что все это можно сделать гораздо более простым и наглядным, если применить графические языки, используемые в теории категорий (и родственные диаграммам Фейнмана). Я даже пытался в ЖЖ изобразить нечто вроде modus ponens (но конечно это не он, по смыслу). Собственно для этого и задумывался мой "монокль", но у самого доделать не хватает чего-то... Саму дедуктивную систему можно рассматривать как моноидальную категорию. Это конечно "страшные" слова, но по сути все очень просто.

Кстати, beroal как раз смог правильно переписать мой нарисованный вывод в более привычной форме.

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

>>Тут даже много хороших частичных наработок. А ссылочек не подкинете?

Java http://www.key-project.org/ http://krakatoa.lri.fr/ http://secure.ucd.ie/products/opensource/ESCJava2/ https://mobius.ucd.ie/ http://lara.epfl.ch/dokuwiki/doku.php?id=jahob_system C# http://research.microsoft.com/en-us/projects/specsharp/

Спасибо!

вот еще интересная http://www.cl.cam.ac.uk/~mjp41/jStar/

У меня есть концепция lightweight тулзы для верификации рефакторинга. Грубо говоря, задача работать с методами без рекурсии и без циклов (либо примитивные циклы). Эта задача при вышеуказанных ограничениях достаточно легко решается - строишь contorl flow graph, поскольку циклов нет (примитивные циклы можно разворачивать), то он представляет собой дерево. По каждому пути в дереве строишь символические уравнения, они достаточно просто решаются солверами (если циклов нет или они простые). Есть конечно технические сложности с парсингом Джавы (хотя можно работать на уровне байткода) плюс с семантикой языка, но тулзу сделать в целом несложно. Самое главное это конечно знать как и где ее применять :). Но я знаю класс задач, для которых она была бы полезна в реальных проектах: рефакторинг лапшеобразного кода внутри циклов. Я с такими проблемами часто сталкивался.

>>рефакторинг лапшеобразного кода внутри циклов Возможно, это прозвучит несколько высокомерно, но я за то, чтобы лапшеобразный код просто не делать :) По поводу Вашей идеи что приходит в голову: использовать частично описанные узлы дерева, т.е. такие процедуры, которые не описаны полностью (но для которые известны пред- пост- условия и инварианты). Если бы это было возможно, применимость, как мне кажется, возросла бы. Но впрочем, не слушайте меня, я подробно в этом никогда не разбирался.

>>Есть конечно технические сложности с парсингом Джавы (хотя можно работать на уровне байткода) плюс с семантикой языка, но тулзу сделать в целом несложно. Питон подходит еще, как мне кажется. Там очень просто работать на уровне байткода, я пробовал. И на уровне синтаксиса можно, т.к. парсер встроен в стандартную библиотеку.

На счет лапши полностью с Вами согласен, но реалии таковы, что ее пишут другие, а мне часто приходилось ее сопровождать :), с целью ускорения перфоманса, например. Там широкий простор для lightweight верификации. По поводу Вашей идеи что приходит в голову: использовать частично описанные узлы дерева, т.е. такие процедуры, которые не описаны полностью (но для которые известны пред- пост- условия и инварианты). Если бы это было возможно, применимость, как мне кажется, возросла бы. Да так можно делать. Кстати, это даже реализовано в KeY тулзе, ссылку на которую я Вам дал. В плане интерфейса, на мой взгляд это лучшее, что есть, в том числе там и эта фича есть :). Но впрочем, не слушайте меня, я подробно в этом никогда не разбирался. Вы на самом деле весьма неплохо разбираетесь. Я не лучше, просто я может чуть больше времени потратил на изучение деталей, но это решаемо :)

Думаю да. Но там будут сложности с higher-order функциями. В Джаве конечно тоже просто они реже вылезают. Но я на Жабу ориентируюсь в силу специализации, я в основном на Жабе пишу. Плюс это основной научный язык сейчас - по крайней мере, один из самых часто используемых.